Mathlib.Topology.Uniform­Convergence

Continuity helpers for function paths in topologies of uniform convergence on compact sets.

Affine 1 core · 1 supporting This file proves continuity of affine interpolation paths in the topology of uniform convergence on a nonempty compact set. ★ continuous_uniformOnFun_affine_of_compact

Affine paths in the topology of uniform convergence

This file proves continuity of affine interpolation paths in the topology of uniform convergence on a nonempty compact set.

lemma continuous_uniformOnFun_affine_of_compact reviewed
Causalean.Mathlib.Topology

For a compact set that is nonempty, the affine interpolation between two endpoint functions continuous on that set is continuous in the topology of uniform convergence on the set.

Formal statement
hypotheses
α E :
Type*
TopologicalSpace α
NormedAddCommGroup E
NormedSpace ℝ E
Set α
hK :
IsCompact K
hKne :
K.Nonempty
f g :
α → E
hf :
ContinuousOn f K
hg :
ContinuousOn g K
conclusion
Continuous (fun t : ℝ => ofFun {K} (fun x => (1 - t) • f x + t • g x))
Proof (Lean source)
lemma continuous_uniformOnFun_affine_of_compact {α E : Type*} [TopologicalSpace α] [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Set α} (hK : IsCompact K) (hKne : K.Nonempty) {f g : α → E} (hf : ContinuousOn f K) (hg : ContinuousOn g K) : Continuous (fun t : ℝ => ofFun {K} (fun x => (1 - t) • f x + t • g x)) := by rcases hK.exists_isMaxOn hKne (hg.sub hf).norm with ⟨x₀, hx₀, hmax⟩ let L : NNReal := ⟨‖g x₀ - f x₀‖, norm_nonneg _⟩ apply UniformOnFun.continuous_of_forall_lipschitzWith (fun _ => L) intro S hS x hx simp only [Set.mem_singleton_iff] at hS subst S rw [lipschitzWith_iff_dist_le_mul] intro t u rw [dist_eq_norm, Real.dist_eq] have hbound : ‖g x - f x‖ ≤ ‖g x₀ - f x₀‖ := by have hxmax := hmax hx change ‖(g - f) x‖ ≤ ‖(g - f) x₀‖ at hxmax simpa only [Pi.sub_apply] using hxmax change ‖((1 - t) • f x + t • g x) - ((1 - u) • f x + u • g x)‖ ≤ ‖g x₀ - f x₀‖ * |t - u| rw [show ((1 - t) • f x + t • g x) - ((1 - u) • f x + u • g x) = (t - u) • (g x - f x) by module, norm_smul, Real.norm_eq_abs] simpa only [mul_comm] using mul_le_mul_of_nonneg_left hbound (abs_nonneg (t - u))
Causalean.Mathlib.Topology.continuous_uniformOnFun_affine_of_compact · Causalean/Mathlib/Topology/UniformConvergence/Affine.lean:21
1 supporting declaration (lemmas, instances)
  • continuous_uniformOnFun_of_eq_affine_on_compact lemma — For a compact set that is nonempty, a path that agrees there with the affine interpolation of two endpoint functions continuous on the set is continuous in the topology of uniform convergence on the set.
    hypotheses
    α E :
    Type*
    TopologicalSpace α
    NormedAddCommGroup E
    NormedSpace ℝ E
    Set α
    hK :
    IsCompact K
    hKne :
    K.Nonempty
    f g :
    α → E
    hf :
    ContinuousOn f K
    hg :
    ContinuousOn g K
    path :
    ℝ → α → E
    hpath :
    ∀ t x
    if
    x ∈ K
    then
    path t x = (1 - t) • f x + t • g x
    conclusion
    Continuous (fun t : ℝ => ofFun {K} (path t))
    Proof (Lean source)
    lemma continuous_uniformOnFun_of_eq_affine_on_compact {α E : Type*} [TopologicalSpace α] [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Set α} (hK : IsCompact K) (hKne : K.Nonempty) {f g : α → E} (hf : ContinuousOn f K) (hg : ContinuousOn g K) (path : ℝ → α → E) (hpath : ∀ t x, x ∈ K → path t x = (1 - t) • f x + t • g x) : Continuous (fun t : ℝ => ofFun {K} (path t)) := by rcases hK.exists_isMaxOn hKne (hg.sub hf).norm with ⟨x₀, hx₀, hmax⟩ let L : NNReal := ⟨‖g x₀ - f x₀‖, norm_nonneg _⟩ apply UniformOnFun.continuous_of_forall_lipschitzWith (fun _ => L) intro S hS x hx simp only [Set.mem_singleton_iff] at hS subst S rw [lipschitzWith_iff_dist_le_mul] intro t u rw [dist_eq_norm, Real.dist_eq] change ‖path t x - path u x‖ ≤ (L : ℝ) * |t - u| rw [hpath t x hx, hpath u x hx] have hbound : ‖g x - f x‖ ≤ ‖g x₀ - f x₀‖ := by have hxmax := hmax hx change ‖(g - f) x‖ ≤ ‖(g - f) x₀‖ at hxmax simpa only [Pi.sub_apply] using hxmax change ‖((1 - t) • f x + t • g x) - ((1 - u) • f x + u • g x)‖ ≤ ‖g x₀ - f x₀‖ * |t - u| rw [show ((1 - t) • f x + t • g x) - ((1 - u) • f x + u • g x) = (t - u) • (g x - f x) by module, norm_smul, Real.norm_eq_abs] simpa only [mul_comm] using mul_le_mul_of_nonneg_left hbound (abs_nonneg (t - u))
    Causalean.Mathlib.Topology.continuous_uniformOnFun_of_eq_affine_on_compact · Causalean/Mathlib/Topology/UniformConvergence/Affine.lean:49