theorem Frourio.limsup_le_of_eventually_le_right {u : ℝ → ℝ} {c : ℝ} : (∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), u h ≤ c) → (∃ (M : ℝ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), u h ≤ M) → (∃ (m : ℝ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), m ≤ u h) → Filter.limsup u (nhdsWithin 0 (Set.Ioi 0)) ≤ c

On the right neighborhood filter nhdsWithin 0 (Ioi 0), if u ≤ c eventually and u is eventually bounded from both sides, then limsup u ≤ c (real version). This follows the pattern from DiniUpper_eq_toReal_of_finite but for general functions.

theorem Frourio.right_filter_limsup_le_of_bounded {u : ℝ → ℝ} {c : ℝ} (hub : ∃ (M : ℝ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), u h ≤ M) (hlb : ∃ (m : ℝ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), m ≤ u h) (hbound : ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), u h ≤ c) : Filter.limsup u (nhdsWithin 0 (Set.Ioi 0)) ≤ c

General right-filter bridge: if u is eventually bounded from both sides and eventually ≤ c, then its real limsup ≤ c. This generalizes the pattern from DiniUpper_eq_toReal_of_finite.

theorem Frourio.right_filter_limsup_le_simple {u : ℝ → ℝ} {c : ℝ} (hlb : ∃ (m : ℝ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), m ≤ u h) (hbound : ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), u h ≤ c) : Filter.limsup u (nhdsWithin 0 (Set.Ioi 0)) ≤ c

Simplified version when the eventual upper bound c also serves as a global upper bound

theorem Frourio.dini_upper_le_of_quotient_bounded {f : ℝ → ℝ} {t c m : ℝ} (hub : ∀ h ∈ Set.Ioo 0 1, (f (t + h) - f t) / h ≤ c) (hlb : ∀ h ∈ Set.Ioo 0 1, m ≤ (f (t + h) - f t) / h) : DiniUpper f t ≤ c

Helper lemma for DiniUpper bound: if quotients are bounded from both sides, DiniUpper is bounded

theorem Frourio.dini_upper_distance_squared {X : Type u_1} [PseudoMetricSpace X] (ρ : ℝ → X) (v : X) (t : ℝ) (hLipschitz : ∃ L > 0, ∀ (s₁ s₂ : ℝ), |s₁ - s₂| < 1 → dist (ρ s₁) (ρ s₂) ≤ L * |s₁ - s₂|) : ∃ (C : ℝ), DiniUpper (fun (τ : ℝ) => d2 (ρ τ) v) t ≤ C

Distance squared along a curve has controlled Dini derivative

theorem Frourio.young_inequality_evi (a b ε : ℝ) (hε : 0 < ε) : a * b ≤ ε * a ^ 2 / 2 + b ^ 2 / (2 * ε)

Young's inequality for the EVI proof

theorem Frourio.geodesic_interpolation_estimate {X : Type u_1} [PseudoMetricSpace X] {G : GeodesicStructure X} (F : X → ℝ) (lamEff : ℝ) (hSemiconvex : GeodesicSemiconvex G F lamEff) (x y : X) (t : ℝ) (ht : t ∈ Set.Icc 0 1) : F (G.γ x y t) ≤ (1 - t) * F x + t * F y - lamEff / 2 * t * (1 - t) * dist x y ^ 2

Geodesic interpolation estimate

def Frourio.UpperSemicontinuous (φ : ℝ → ℝ) : Prop

Upper semicontinuous function using the quotient-based formulation Compatible with the EVI framework from EVICore6Sub2

Equations

• Frourio.UpperSemicontinuous φ = ∀ (s t : ℝ), s < t → ∀ w ∈ Set.Icc 0 (t - s), ∀ y₀ ∈ Set.Icc 0 (t - s), |y₀ - w| < (t - s) / 4 → Frourio.upper_semicontinuous_at_zero φ s y₀

theorem Frourio.upperSemicontinuous_add_continuous {f g : ℝ → ℝ} (hf : UpperSemicontinuous f) (hg_lip_bound : ∀ (x ε : ℝ), ε > 0 → ∃ δ > 0, ∀ (y z : ℝ), |y - x| < δ → |z - x| < δ → |g y - g z| < ε / 2 * |y - z|) : UpperSemicontinuous (f + g)

Helper: Sum of USC function and locally Lipschitz continuous function is USC The key additional assumption is that for each ε > 0, we can find a neighborhood where the Lipschitz constant is bounded by ε/2

theorem Frourio.ereal_limsup_le_of_eventually_le {α : Type u_2} {f : α → EReal} {l : Filter α} {C : EReal} (h : ∀ᶠ (x : α) in l, f x ≤ C) : Filter.limsup f l ≤ C

EReal version: Limsup is bounded by a constant if the function is eventually bounded

theorem Frourio.ereal_limsup_const {α : Type u_2} {l : Filter α} {C : EReal} [l.NeBot] : Filter.limsup (fun (x : α) => C) l = C

EReal version: Limsup of a constant function equals the constant

theorem Frourio.DiniUpperE_lam_d2_bound_explicit {X : Type u_2} [PseudoMetricSpace X] (ρ : ℝ → X) (v : X) (t lam L : ℝ) (hL_pos : 0 < L) (hL_bound : ∀ s ∈ Set.Ioo (t - 1) (t + 1), dist (ρ s) (ρ t) ≤ L * |s - t|) : DiniUpperE (fun (τ : ℝ) => lam * d2 (ρ τ) v) t ≤ ↑(|lam| * (2 * L * dist (ρ t) v + L ^ 2))

DiniUpperE of λ times squared distance along a Lipschitz curve

theorem Frourio.DiniUpperE_lam_d2_bound {X : Type u_2} [PseudoMetricSpace X] (ρ : ℝ → X) (v : X) (t lam : ℝ) (hLip : ∃ L > 0, ∀ s ∈ Set.Ioo (t - 1) (t + 1), dist (ρ s) (ρ t) ≤ L * |s - t|) : ∃ (C : EReal), DiniUpperE (fun (τ : ℝ) => lam * d2 (ρ τ) v) t ≤ C

DiniUpperE of λ times squared distance along a Lipschitz curve