feat: continuity of primitives for parametric integrals (#11185)

From the sphere eversion project and generalised by `sgouezel`.

This is used in the sphere eversion project to show that averaging of loops is continuous (which will be PRed to mathlib at a later point).

Co-authored by: @fpvandoorn (who write this code originally, I believe)



Co-authored-by: Ruben Van de Velde <[email protected]>
Co-authored-by: sgouezel <[email protected]>

Author: 3 people

Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean

@@ -494,3 +494,29 @@ theorem exists_spanning_measurableSet_le {m : MeasurableSpace α} {f : α → 
       refine fun hif => hif.trans ?_
       exact mod_cast hij
     rw [this, norm_sets_spanning, iUnion_spanningSets μ, Set.inter_univ]
+
+variable (μ : Measure ℝ) [IsFiniteMeasureOnCompacts μ]
+
+lemma tendsto_measure_Icc_nhdsWithin_right' (b : ℝ) :
+    Tendsto (fun δ ↦ μ (Icc (b - δ) (b + δ))) (𝓝[>] (0 : ℝ)) (𝓝 (μ {b})) := by
+  rw [Real.singleton_eq_inter_Icc]
+  apply tendsto_measure_biInter_gt (fun r hr ↦ measurableSet_Icc)
+  · intro r s _rpos hrs
+    exact Icc_subset_Icc (by linarith) (by linarith)
+  · exact ⟨1, zero_lt_one, isCompact_Icc.measure_ne_top⟩
+
+lemma tendsto_measure_Icc_nhdsWithin_right (b : ℝ) :
+    Tendsto (fun δ ↦ μ (Icc (b - δ) (b + δ))) (𝓝[≥] (0 : ℝ)) (𝓝 (μ {b})) := by
+  simp only [← nhdsWithin_right_sup_nhds_singleton, nhdsWithin_singleton, tendsto_sup,
+    tendsto_measure_Icc_nhdsWithin_right' μ b, true_and, tendsto_pure_left]
+  intro s hs
+  simpa using mem_of_mem_nhds hs
+
+lemma tendsto_measure_Icc [NoAtoms μ] (b : ℝ) :
+    Tendsto (fun δ ↦ μ (Icc (b - δ) (b + δ))) (𝓝 (0 : ℝ)) (𝓝 0) := by
+  rw [← nhds_left'_sup_nhds_right, tendsto_sup]
+  constructor
+  · apply tendsto_const_nhds.congr'
+    filter_upwards [self_mem_nhdsWithin] with r (hr : r < 0)
+    rw [Icc_eq_empty (by linarith), measure_empty]
+  · simpa only [measure_singleton] using tendsto_measure_Icc_nhdsWithin_right μ b

Mathlib/MeasureTheory/Integral/DominatedConvergence.lean

@@ -28,7 +28,7 @@ for the Bochner integral.
 
 -/
 
-open MeasureTheory
+open MeasureTheory Metric
 
 /-!
 ## The Lebesgue dominated convergence theorem for the Bochner integral
@@ -41,7 +41,7 @@ open scoped Topology
 namespace MeasureTheory
 
 variable {α E G : Type*}
-  [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
+  [NormedAddCommGroup E] [NormedSpace ℝ E]
   [NormedAddCommGroup G] [NormedSpace ℝ G]
   {f g : α → E} {m : MeasurableSpace α} {μ : Measure α}
 
@@ -136,6 +136,8 @@ theorem integral_tsum {ι} [Countable ι] {f : ι → α → G} (hf : ∀ i, AES
 lemma hasSum_integral_of_summable_integral_norm {ι} [Countable ι] {F : ι → α → E}
     (hF_int : ∀ i : ι, Integrable (F i) μ) (hF_sum : Summable fun i ↦ ∫ a, ‖F i a‖ ∂μ) :
     HasSum (∫ a, F · a ∂μ) (∫ a, (∑' i, F i a) ∂μ) := by
+  by_cases hE : CompleteSpace E; swap
+  · simp [integral, hE, hasSum_zero]
   rw [integral_tsum (fun i ↦ (hF_int i).1)]
   · exact (hF_sum.of_norm_bounded _ fun i ↦ norm_integral_le_integral_norm _).hasSum
   have (i : ι) : ∫⁻ (a : α), ‖F i a‖₊ ∂μ = ‖(∫ a : α, ‖F i a‖ ∂μ)‖₊ := by
@@ -192,7 +194,7 @@ namespace intervalIntegral
 
 section DCT
 
-variable {ι 𝕜 E F : Type*} [NormedAddCommGroup E] [CompleteSpace E] [NormedSpace ℝ E]
+variable {ι 𝕜 E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
   {a b : ℝ} {f : ℝ → E} {μ : Measure ℝ}
 
 /-- Lebesgue dominated convergence theorem for filters with a countable basis -/
@@ -228,6 +230,8 @@ special case of the dominated convergence theorem). -/
 theorem hasSum_intervalIntegral_of_summable_norm [Countable ι] {f : ι → C(ℝ, E)}
     (hf_sum : Summable fun i : ι => ‖(f i).restrict (⟨uIcc a b, isCompact_uIcc⟩ : Compacts ℝ)‖) :
     HasSum (fun i : ι => ∫ x in a..b, f i x) (∫ x in a..b, ∑' i : ι, f i x) := by
+  by_cases hE : CompleteSpace E; swap
+  · simp [intervalIntegral, integral, hE, hasSum_zero]
   apply hasSum_integral_of_dominated_convergence
     (fun i (x : ℝ) => ‖(f i).restrict ↑(⟨uIcc a b, isCompact_uIcc⟩ : Compacts ℝ)‖)
     (fun i => (map_continuous <| f i).aestronglyMeasurable)
@@ -237,8 +241,7 @@ theorem hasSum_intervalIntegral_of_summable_norm [Countable ι] {f : ι → C(
   · exact ae_of_all _ fun x _ => hf_sum
   · exact intervalIntegrable_const
   · refine ae_of_all _ fun x hx => Summable.hasSum ?_
-    let x : (⟨uIcc a b, isCompact_uIcc⟩ : Compacts ℝ) := ⟨x, ?_⟩; swap
-    · exact ⟨hx.1.le, hx.2⟩
+    let x : (⟨uIcc a b, isCompact_uIcc⟩ : Compacts ℝ) := ⟨x, ⟨hx.1.le, hx.2⟩⟩
     have := hf_sum.of_norm
     simpa only [Compacts.coe_mk, ContinuousMap.restrict_apply]
       using ContinuousMap.summable_apply this x
@@ -300,7 +303,7 @@ section ContinuousPrimitive
 
 open scoped Interval
 
-variable {E : Type*} [NormedAddCommGroup E] [CompleteSpace E] [NormedSpace ℝ E]
+variable {E X : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace X]
   {a b b₀ b₁ b₂ : ℝ} {μ : Measure ℝ} {f : ℝ → E}
 
 theorem continuousWithinAt_primitive (hb₀ : μ {b₀} = 0)
@@ -368,10 +371,8 @@ theorem continuousWithinAt_primitive (hb₀ : μ {b₀} = 0)
   · apply continuousWithinAt_of_not_mem_closure
     rwa [closure_Icc]
 
-variable {X : Type*} [TopologicalSpace X] [FirstCountableTopology X]
-  {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
-
-theorem continuousAt_parametric_primitive_of_dominated {F : X → ℝ → E} (bound : ℝ → ℝ) (a b : ℝ)
+theorem continuousAt_parametric_primitive_of_dominated [FirstCountableTopology X]
+    {F : X → ℝ → E} (bound : ℝ → ℝ) (a b : ℝ)
     {a₀ b₀ : ℝ} {x₀ : X} (hF_meas : ∀ x, AEStronglyMeasurable (F x) (μ.restrict <| Ι a b))
     (h_bound : ∀ᶠ x in 𝓝 x₀, ∀ᵐ t ∂μ.restrict <| Ι a b, ‖F x t‖ ≤ bound t)
     (bound_integrable : IntervalIntegrable bound μ a b)
@@ -390,7 +391,7 @@ theorem continuousAt_parametric_primitive_of_dominated {F : X → ℝ → E} (bo
     rw [nhds_prod_eq]
     refine (h_bound.prod_mk Ioo_nhds).mono ?_
     rintro ⟨x, t⟩ ⟨hx : ∀ᵐ t : ℝ ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t, ht : t ∈ Ioo a b⟩
-    dsimp (config := { eta := false })
+    dsimp
     have hiF : ∀ {x a₀ b₀},
         (∀ᵐ t : ℝ ∂μ.restrict (Ι a b), ‖F x t‖ ≤ bound t) → a₀ ∈ Ioo a b → b₀ ∈ Ioo a b →
           IntervalIntegrable (F x) μ a₀ b₀ := fun {x a₀ b₀} hx ha₀ hb₀ ↦
@@ -498,6 +499,133 @@ nonrec theorem _root_.MeasureTheory.Integrable.continuous_primitive (h_int : Int
     (a : ℝ) : Continuous fun b => ∫ x in a..b, f x ∂μ :=
   continuous_primitive (fun _ _ => h_int.intervalIntegrable) a
 
+variable [IsLocallyFiniteMeasure μ] {f : X → ℝ → E}
+
+theorem continuous_parametric_primitive_of_continuous
+    {a₀ : ℝ} (hf : Continuous f.uncurry) :
+    Continuous fun p : X × ℝ ↦ ∫ t in a₀..p.2, f p.1 t ∂μ := by
+  -- We will prove continuity at a point `(q, b₀)`.
+  rw [continuous_iff_continuousAt]
+  rintro ⟨q, b₀⟩
+  apply Metric.continuousAt_iff'.2 (fun ε εpos ↦ ?_)
+  -- choose `a` and `b` such that `(a, b)` contains both `a₀` and `b₀`. We will use uniform
+  -- estimates on a neighborhood of the compact set `{q} × [a, b]`.
+  cases' exists_lt (min a₀ b₀) with a a_lt
+  cases' exists_gt (max a₀ b₀) with b lt_b
+  rw [lt_min_iff] at a_lt
+  rw [max_lt_iff] at lt_b
+  have : IsCompact ({q} ×ˢ (Icc a b)) := isCompact_singleton.prod isCompact_Icc
+  -- let `M` be a bound for `f` on the compact set `{q} × [a, b]`.
+  obtain ⟨M, hM⟩ := this.bddAbove_image hf.norm.continuousOn
+  -- let `δ` be small enough to satisfy several properties that will show up later.
+  obtain ⟨δ, δpos, hδ, h'δ, h''δ⟩ : ∃ (δ : ℝ), 0 < δ ∧ δ < 1 ∧ Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b ∧
+      (M + 1) * (μ (Icc (b₀ - δ) (b₀ + δ))).toReal + δ * (μ (Icc a b)).toReal < ε := by
+    have A : ∀ᶠ δ in 𝓝[>] (0 : ℝ), δ ∈ Ioo 0 1 := Ioo_mem_nhdsWithin_Ioi (by simp)
+    have B : ∀ᶠ δ in 𝓝 0, Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b := by
+      have I : Tendsto (fun δ ↦ b₀ - δ) (𝓝 0) (𝓝 (b₀ - 0)) := tendsto_const_nhds.sub tendsto_id
+      have J : Tendsto (fun δ ↦ b₀ + δ) (𝓝 0) (𝓝 (b₀ + 0)) := tendsto_const_nhds.add tendsto_id
+      simp only [sub_zero, add_zero] at I J
+      filter_upwards [(tendsto_order.1 I).1 _ a_lt.2, (tendsto_order.1 J).2 _ lt_b.2] with δ hδ h'δ
+      exact Icc_subset_Icc hδ.le h'δ.le
+    have C : ∀ᶠ δ in 𝓝 0,
+        (M + 1) * (μ (Icc (b₀ - δ) (b₀ + δ))).toReal + δ * (μ (Icc a b)).toReal < ε := by
+      suffices Tendsto
+        (fun δ ↦ (M + 1) * (μ (Icc (b₀ - δ) (b₀ + δ))).toReal + δ * (μ (Icc a b)).toReal)
+          (𝓝 0) (𝓝 ((M + 1) * (0 : ℝ≥0∞).toReal + 0 * (μ (Icc a b)).toReal)) by
+        simp only [zero_toReal, mul_zero, zero_mul, add_zero] at this
+        exact (tendsto_order.1 this).2 _ εpos
+      apply Tendsto.add (Tendsto.mul tendsto_const_nhds _)
+        (Tendsto.mul tendsto_id tendsto_const_nhds)
+      exact (tendsto_toReal zero_ne_top).comp (tendsto_measure_Icc _ _)
+    rcases (A.and ((B.and C).filter_mono nhdsWithin_le_nhds)).exists with ⟨δ, hδ, h'δ, h''δ⟩
+    exact ⟨δ, hδ.1, hδ.2, h'δ, h''δ⟩
+  -- By compactness of `[a, b]` and continuity of `f` there, if `p` is close enough to `q`
+  -- then `f p x` is `δ`-close to `f q x`, uniformly in `x ∈ [a, b]`.
+  -- (Note in particular that this implies a bound `M + δ ≤ M + 1` for `f p x`).
+  obtain ⟨v, v_mem, hv⟩ : ∃ v ∈ 𝓝[univ] q, ∀ p ∈ v, ∀ x ∈ Icc a b, dist (f p x) (f q x) < δ :=
+    IsCompact.mem_uniformity_of_prod isCompact_Icc hf.continuousOn (mem_univ _)
+      (dist_mem_uniformity δpos)
+  -- for `p` in this neighborhood and `s` which is `δ`-close to `b₀`, we will show that the
+  -- integrals are `ε`-close.
+  have : v ×ˢ (Ioo (b₀ - δ) (b₀ + δ)) ∈ 𝓝 (q, b₀) := by
+    rw [nhdsWithin_univ] at v_mem
+    simp only [prod_mem_nhds_iff, v_mem, true_and]
+    apply Ioo_mem_nhds <;> linarith
+  filter_upwards [this]
+  rintro ⟨p, s⟩ ⟨hp : p ∈ v, hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)⟩
+  simp only [dist_eq_norm] at hv ⊢
+  have J r u v : IntervalIntegrable (f r) μ u v := (hf.uncurry_left _).intervalIntegrable _ _
+  /- we compute the difference between the integrals by splitting the contribution of the change
+  from `b₀` to `s` (which gives a contribution controlled by the measure of `(b₀ - δ, b₀ + δ)`,
+  small enough thanks to our choice of `δ`) and the change from `q` to `p`, which is small as
+  `f p x` and `f q x` are uniformly close by design. -/
+  calc
+  ‖∫ t in a₀..s, f p t ∂μ - ∫ t in a₀..b₀, f q t ∂μ‖
+    = ‖(∫ t in a₀..s, f p t ∂μ - ∫ t in a₀..b₀, f p t ∂μ)
+        + (∫ t in a₀..b₀, f p t ∂μ - ∫ t in a₀..b₀, f q t ∂μ)‖ := by congr 1; abel
+  _ ≤ ‖∫ t in a₀..s, f p t ∂μ - ∫ t in a₀..b₀, f p t ∂μ‖
+        + ‖∫ t in a₀..b₀, f p t ∂μ - ∫ t in a₀..b₀, f q t ∂μ‖ := norm_add_le _ _
+  _ = ‖∫ t in b₀..s, f p t ∂μ‖ + ‖∫ t in a₀..b₀, (f p t - f q t) ∂μ‖ := by
+      congr 2
+      · rw [integral_interval_sub_left (J _ _ _) (J _ _ _)]
+      · rw [integral_sub (J _ _ _) (J _ _ _)]
+  _ ≤ ∫ t in Ι b₀ s, ‖f p t‖ ∂μ + ∫ t in Ι a₀ b₀, ‖f p t - f q t‖ ∂μ := by
+      gcongr
+      · exact norm_integral_le_integral_norm_Ioc
+      · exact norm_integral_le_integral_norm_Ioc
+  _ ≤ ∫ t in Icc (b₀ - δ) (b₀ + δ), ‖f p t‖ ∂μ + ∫ t in Icc a b, ‖f p t - f q t‖ ∂μ := by
+      gcongr
+      · apply setIntegral_mono_set
+        · exact (hf.uncurry_left _).norm.integrableOn_Icc
+        · exact eventually_of_forall (fun x ↦ norm_nonneg _)
+        · have : Ι b₀ s ⊆ Icc (b₀ - δ) (b₀ + δ) := by
+            apply uIoc_subset_uIcc.trans (uIcc_subset_Icc ?_ ⟨hs.1.le, hs.2.le⟩ )
+            simp [δpos.le]
+          exact eventually_of_forall this
+      · apply setIntegral_mono_set
+        · exact ((hf.uncurry_left _).sub (hf.uncurry_left _)).norm.integrableOn_Icc
+        · exact eventually_of_forall (fun x ↦ norm_nonneg _)
+        · have : Ι a₀ b₀ ⊆ Icc a b := uIoc_subset_uIcc.trans
+            (uIcc_subset_Icc ⟨a_lt.1.le, lt_b.1.le⟩ ⟨a_lt.2.le, lt_b.2.le⟩)
+          exact eventually_of_forall this
+  _ ≤ ∫ t in Icc (b₀ - δ) (b₀ + δ), M + 1 ∂μ + ∫ _t in Icc a b, δ ∂μ := by
+      gcongr
+      · apply setIntegral_mono_on
+        · exact (hf.uncurry_left _).norm.integrableOn_Icc
+        · exact continuous_const.integrableOn_Icc
+        · exact measurableSet_Icc
+        · intro x hx
+          calc ‖f p x‖ = ‖f q x + (f p x - f q x)‖ := by congr; abel
+          _ ≤ ‖f q x‖ + ‖f p x - f q x‖ := norm_add_le _ _
+          _ ≤ M + δ := by
+              gcongr
+              · apply hM
+                change (fun x ↦ ‖Function.uncurry f x‖) (q, x) ∈ _
+                apply mem_image_of_mem
+                simp only [singleton_prod, mem_image, Prod.mk.injEq, true_and, exists_eq_right]
+                exact h'δ hx
+              · exact le_of_lt (hv _ hp _ (h'δ hx))
+          _ ≤ M + 1 := by linarith
+      · apply setIntegral_mono_on
+        · exact ((hf.uncurry_left _).sub (hf.uncurry_left _)).norm.integrableOn_Icc
+        · exact continuous_const.integrableOn_Icc
+        · exact measurableSet_Icc
+        · intro x hx
+          exact le_of_lt (hv _ hp _ hx)
+  _ = (M + 1) * (μ (Icc (b₀ - δ) (b₀ + δ))).toReal + δ * (μ (Icc a b)).toReal := by simp [mul_comm]
+  _ < ε := h''δ
+
+@[fun_prop]
+theorem continuous_parametric_intervalIntegral_of_continuous {a₀ : ℝ}
+    (hf : Continuous f.uncurry) {s : X → ℝ} (hs : Continuous s) :
+    Continuous fun x ↦ ∫ t in a₀..s x, f x t ∂μ :=
+  show Continuous ((fun p : X × ℝ ↦ ∫ t in a₀..p.2, f p.1 t ∂μ) ∘ fun x ↦ (x, s x)) from
+    (continuous_parametric_primitive_of_continuous hf).comp₂ continuous_id hs
+
+theorem continuous_parametric_intervalIntegral_of_continuous'
+    (hf : Continuous f.uncurry) (a₀ b₀ : ℝ) :
+    Continuous fun x ↦ ∫ t in a₀..b₀, f x t ∂μ := by fun_prop
+
 end ContinuousPrimitive
 
 end intervalIntegral

Mathlib/Topology/MetricSpace/Pseudo/Lemmas.lean

@@ -38,6 +38,9 @@ instance : OrderTopology ℝ :=
   orderTopology_of_nhds_abs fun x => by
     simp only [nhds_basis_ball.eq_biInf, ball, Real.dist_eq, abs_sub_comm]
 
+lemma Real.singleton_eq_inter_Icc (b : ℝ) : {b} = ⋂ (r > 0), Icc (b - r) (b + r) := by
+  simp [Icc_eq_closedBall, biInter_basis_nhds Metric.nhds_basis_closedBall]
+
 /-- Special case of the sandwich lemma; see `tendsto_of_tendsto_of_tendsto_of_le_of_le'` for the
 general case. -/
 lemma squeeze_zero' {α} {f g : α → ℝ} {t₀ : Filter α} (hf : ∀ᶠ t in t₀, 0 ≤ f t)

Mathlib/Topology/Order/LeftRight.lean

@@ -107,6 +107,10 @@ theorem nhds_left_sup_nhds_right' (a : α) : 𝓝[≤] a ⊔ 𝓝[>] a = 𝓝 a
 theorem nhds_left'_sup_nhds_right' (a : α) : 𝓝[<] a ⊔ 𝓝[>] a = 𝓝[≠] a := by
   rw [← nhdsWithin_union, Iio_union_Ioi]
 
+lemma nhdsWithin_right_sup_nhds_singleton (a : α) :
+    𝓝[>] a ⊔ 𝓝[{a}] a = 𝓝[≥] a := by
+  simp only [union_singleton, Ioi_insert, ← nhdsWithin_union]
+
 theorem continuousAt_iff_continuous_left_right {a : α} {f : α → β} :
     ContinuousAt f a ↔ ContinuousWithinAt f (Iic a) a ∧ ContinuousWithinAt f (Ici a) a := by
   simp only [ContinuousWithinAt, ContinuousAt, ← tendsto_sup, nhds_left_sup_nhds_right]