Exact source: Mathlib/Analysis/Convex/Integral.lean
Pinned GitHub source · Raw UTF-8 source
Back to The average of contractive derivative generators lies in the body
1/-2Copyright (c) 2020 Yury Kudryashov. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Yury Kudryashov5-/6module78public import Mathlib.Analysis.Convex.Function9public import Mathlib.Analysis.Convex.StrictConvexSpace10public import Mathlib.MeasureTheory.Function.AEEqOfIntegral11public import Mathlib.MeasureTheory.Integral.Average1213/-!14# Jensen's inequality for integrals1516In this file we prove several forms of Jensen's inequality for integrals.1718- for convex sets: `Convex.average_mem`, `Convex.set_average_mem`, `Convex.integral_mem`;1920- for convex functions: `ConvexOn.average_mem_epigraph`, `ConvexOn.map_average_le`,21 `ConvexOn.set_average_mem_epigraph`, `ConvexOn.map_set_average_le`, `ConvexOn.map_integral_le`;2223- for strictly convex sets: `StrictConvex.ae_eq_const_or_average_mem_interior`;2425- for a closed ball in a strictly convex normed space:26 `ae_eq_const_or_norm_integral_lt_of_norm_le_const`;2728- for strictly convex functions: `StrictConvexOn.ae_eq_const_or_map_average_lt`.2930## TODO3132- Use a typeclass for strict convexity of a closed ball.3334## Tags3536convex, integral, center mass, average value, Jensen's inequality37-/3839public section404142open MeasureTheory MeasureTheory.Measure Metric Set Filter TopologicalSpace Function4344open scoped Topology ENNReal Convex4546variable {α E : Type*} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E]47 [CompleteSpace E] {μ : Measure α} {s : Set E} {t : Set α} {f : α → E} {g : E → ℝ} {C : ℝ}4849/-!50### Non-strict Jensen's inequality51-/525354/-- If `μ` is a probability measure on `α`, `s` is a convex closed set in `E`, and `f` is an55integrable function sending `μ`-a.e. points to `s`, then the expected value of `f` belongs to `s`:56`∫ x, f x ∂μ ∈ s`. See also `Convex.sum_mem` for a finite sum version of this lemma. -/57theorem Convex.integral_mem [IsProbabilityMeasure μ] (hs : Convex ℝ s) (hsc : IsClosed s)58 (hf : ∀ᵐ x ∂μ, f x ∈ s) (hfi : Integrable f μ) : (∫ x, f x ∂μ) ∈ s := by59 borelize E60 rcases hfi.aestronglyMeasurable with ⟨g, hgm, hfg⟩61 haveI : SeparableSpace (range g ∩ s : Set E) :=62 (hgm.isSeparable_range.mono inter_subset_left).separableSpace63 obtain ⟨y₀, h₀⟩ : (range g ∩ s).Nonempty := by64 rcases (hf.and hfg).exists with ⟨x₀, h₀⟩65 exact ⟨f x₀, by simp only [h₀.2, mem_range_self], h₀.1⟩66 rw [integral_congr_ae hfg]; rw [integrable_congr hfg] at hfi67 have hg : ∀ᵐ x ∂μ, g x ∈ closure (range g ∩ s) := by68 filter_upwards [hfg.rw (fun _ y => y ∈ s) hf] with x hx69 apply subset_closure70 exact ⟨mem_range_self _, hx⟩71 set G : ℕ → SimpleFunc α E := SimpleFunc.approxOn _ hgm.measurable (range g ∩ s) y₀ h₀72 have : Tendsto (fun n => (G n).integral μ) atTop (𝓝 <| ∫ x, g x ∂μ) :=73 tendsto_integral_approxOn_of_measurable hfi _ hg _ (integrable_const _)74 refine hsc.mem_of_tendsto this (Eventually.of_forall fun n => hs.sum_mem ?_ ?_ ?_)75 · exact fun _ _ => ENNReal.toReal_nonneg76 · simp_rw [measureReal_def]77 rw [← ENNReal.toReal_sum, (G n).sum_range_measure_preimage_singleton, measure_univ,78 ENNReal.toReal_one]79 finiteness80 · simp only [SimpleFunc.mem_range, forall_mem_range]81 intro x82 apply (range g).inter_subset_right83 exact SimpleFunc.approxOn_mem hgm.measurable h₀ _ _8485/-- If `μ` is a non-zero finite measure on `α`, `s` is a convex closed set in `E`, and `f` is an86integrable function sending `μ`-a.e. points to `s`, then the average value of `f` belongs to `s`:87`⨍ x, f x ∂μ ∈ s`. See also `Convex.centerMass_mem` for a finite sum version of this lemma. -/88theorem Convex.average_mem [IsFiniteMeasure μ] [NeZero μ] (hs : Convex ℝ s) (hsc : IsClosed s)89 (hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : Integrable f μ) : (⨍ x, f x ∂μ) ∈ s :=90 hs.integral_mem hsc (ae_mono' smul_absolutelyContinuous hfs) hfi.to_average9192/-- If `μ` is a non-zero finite measure on `α`, `s` is a convex closed set in `E`, and `f` is an93integrable function sending `μ`-a.e. points to `s`, then the average value of `f` belongs to `s`:94`⨍ x, f x ∂μ ∈ s`. See also `Convex.centerMass_mem` for a finite sum version of this lemma. -/95theorem Convex.set_average_mem (hs : Convex ℝ s) (hsc : IsClosed s) (h0 : μ t ≠ 0) (ht : μ t ≠ ∞)96 (hfs : ∀ᵐ x ∂μ.restrict t, f x ∈ s) (hfi : IntegrableOn f t μ) : (⨍ x in t, f x ∂μ) ∈ s :=97 have := Fact.mk ht.lt_top98 have := NeZero.mk h099 hs.average_mem hsc hfs hfi100101/-- If `μ` is a non-zero finite measure on `α`, `s` is a convex set in `E`, and `f` is an integrable102function sending `μ`-a.e. points to `s`, then the average value of `f` belongs to `closure s`:103`⨍ x, f x ∂μ ∈ s`. See also `Convex.centerMass_mem` for a finite sum version of this lemma. -/104theorem Convex.set_average_mem_closure (hs : Convex ℝ s) (h0 : μ t ≠ 0) (ht : μ t ≠ ∞)105 (hfs : ∀ᵐ x ∂μ.restrict t, f x ∈ s) (hfi : IntegrableOn f t μ) :106 (⨍ x in t, f x ∂μ) ∈ closure s :=107 hs.closure.set_average_mem isClosed_closure h0 ht (hfs.mono fun _ hx => subset_closure hx) hfi108109theorem ConvexOn.average_mem_epigraph [IsFiniteMeasure μ] [NeZero μ] (hg : ConvexOn ℝ s g)110 (hgc : ContinuousOn g s) (hsc : IsClosed s) (hfs : ∀ᵐ x ∂μ, f x ∈ s)111 (hfi : Integrable f μ) (hgi : Integrable (g ∘ f) μ) :112 (⨍ x, f x ∂μ, ⨍ x, g (f x) ∂μ) ∈ {p : E × ℝ | p.1 ∈ s ∧ g p.1 ≤ p.2} := by113 have ht_mem : ∀ᵐ x ∂μ, (f x, g (f x)) ∈ {p : E × ℝ | p.1 ∈ s ∧ g p.1 ≤ p.2} :=114 hfs.mono fun x hx => ⟨hx, le_rfl⟩115 exact average_pair hfi hgi ▸116 hg.convex_epigraph.average_mem (hsc.epigraph hgc) ht_mem (hfi.prodMk hgi)117118theorem ConcaveOn.average_mem_hypograph [IsFiniteMeasure μ] [NeZero μ] (hg : ConcaveOn ℝ s g)119 (hgc : ContinuousOn g s) (hsc : IsClosed s) (hfs : ∀ᵐ x ∂μ, f x ∈ s)120 (hfi : Integrable f μ) (hgi : Integrable (g ∘ f) μ) :121 (⨍ x, f x ∂μ, ⨍ x, g (f x) ∂μ) ∈ {p : E × ℝ | p.1 ∈ s ∧ p.2 ≤ g p.1} := by122 simpa only [mem_setOf_eq, Pi.neg_apply, average_neg, neg_le_neg_iff] using123 hg.neg.average_mem_epigraph hgc.neg hsc hfs hfi hgi.neg124125/-- **Jensen's inequality**: if a function `g : E → ℝ` is convex and continuous on a convex closed126set `s`, `μ` is a finite non-zero measure on `α`, and `f : α → E` is a function sending127`μ`-a.e. points to `s`, then the value of `g` at the average value of `f` is less than or equal to128the average value of `g ∘ f` provided that both `f` and `g ∘ f` are integrable. See also129`ConvexOn.map_centerMass_le` for a finite sum version of this lemma. -/130theorem ConvexOn.map_average_le [IsFiniteMeasure μ] [NeZero μ]131 (hg : ConvexOn ℝ s g) (hgc : ContinuousOn g s) (hsc : IsClosed s)132 (hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : Integrable f μ) (hgi : Integrable (g ∘ f) μ) :133 g (⨍ x, f x ∂μ) ≤ ⨍ x, g (f x) ∂μ :=134 (hg.average_mem_epigraph hgc hsc hfs hfi hgi).2135136/-- **Jensen's inequality**: if a function `g : E → ℝ` is concave and continuous on a convex closed137set `s`, `μ` is a finite non-zero measure on `α`, and `f : α → E` is a function sending138`μ`-a.e. points to `s`, then the average value of `g ∘ f` is less than or equal to the value of `g`139at the average value of `f` provided that both `f` and `g ∘ f` are integrable. See also140`ConcaveOn.le_map_centerMass` for a finite sum version of this lemma. -/141theorem ConcaveOn.le_map_average [IsFiniteMeasure μ] [NeZero μ]142 (hg : ConcaveOn ℝ s g) (hgc : ContinuousOn g s) (hsc : IsClosed s)143 (hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : Integrable f μ) (hgi : Integrable (g ∘ f) μ) :144 (⨍ x, g (f x) ∂μ) ≤ g (⨍ x, f x ∂μ) :=145 (hg.average_mem_hypograph hgc hsc hfs hfi hgi).2146147/-- **Jensen's inequality**: if a function `g : E → ℝ` is convex and continuous on a convex closed148set `s`, `μ` is a finite non-zero measure on `α`, and `f : α → E` is a function sending149`μ`-a.e. points of a set `t` to `s`, then the value of `g` at the average value of `f` over `t` is150less than or equal to the average value of `g ∘ f` over `t` provided that both `f` and `g ∘ f` are151integrable. -/152theorem ConvexOn.set_average_mem_epigraph (hg : ConvexOn ℝ s g) (hgc : ContinuousOn g s)153 (hsc : IsClosed s) (h0 : μ t ≠ 0) (ht : μ t ≠ ∞) (hfs : ∀ᵐ x ∂μ.restrict t, f x ∈ s)154 (hfi : IntegrableOn f t μ) (hgi : IntegrableOn (g ∘ f) t μ) :155 (⨍ x in t, f x ∂μ, ⨍ x in t, g (f x) ∂μ) ∈ {p : E × ℝ | p.1 ∈ s ∧ g p.1 ≤ p.2} :=156 have := Fact.mk ht.lt_top157 have := NeZero.mk h0158 hg.average_mem_epigraph hgc hsc hfs hfi hgi159160/-- **Jensen's inequality**: if a function `g : E → ℝ` is concave and continuous on a convex closed161set `s`, `μ` is a finite non-zero measure on `α`, and `f : α → E` is a function sending162`μ`-a.e. points of a set `t` to `s`, then the average value of `g ∘ f` over `t` is less than or163equal to the value of `g` at the average value of `f` over `t` provided that both `f` and `g ∘ f`164are integrable. -/165theorem ConcaveOn.set_average_mem_hypograph (hg : ConcaveOn ℝ s g) (hgc : ContinuousOn g s)166 (hsc : IsClosed s) (h0 : μ t ≠ 0) (ht : μ t ≠ ∞) (hfs : ∀ᵐ x ∂μ.restrict t, f x ∈ s)167 (hfi : IntegrableOn f t μ) (hgi : IntegrableOn (g ∘ f) t μ) :168 (⨍ x in t, f x ∂μ, ⨍ x in t, g (f x) ∂μ) ∈ {p : E × ℝ | p.1 ∈ s ∧ p.2 ≤ g p.1} := by169 simpa only [mem_setOf_eq, Pi.neg_apply, average_neg, neg_le_neg_iff] using170 hg.neg.set_average_mem_epigraph hgc.neg hsc h0 ht hfs hfi hgi.neg171172/-- **Jensen's inequality**: if a function `g : E → ℝ` is convex and continuous on a convex closed173set `s`, `μ` is a finite non-zero measure on `α`, and `f : α → E` is a function sending174`μ`-a.e. points of a set `t` to `s`, then the value of `g` at the average value of `f` over `t` is175less than or equal to the average value of `g ∘ f` over `t` provided that both `f` and `g ∘ f` are176integrable. -/177theorem ConvexOn.map_set_average_le (hg : ConvexOn ℝ s g) (hgc : ContinuousOn g s)178 (hsc : IsClosed s) (h0 : μ t ≠ 0) (ht : μ t ≠ ∞) (hfs : ∀ᵐ x ∂μ.restrict t, f x ∈ s)179 (hfi : IntegrableOn f t μ) (hgi : IntegrableOn (g ∘ f) t μ) :180 g (⨍ x in t, f x ∂μ) ≤ ⨍ x in t, g (f x) ∂μ :=181 (hg.set_average_mem_epigraph hgc hsc h0 ht hfs hfi hgi).2182183/-- **Jensen's inequality**: if a function `g : E → ℝ` is concave and continuous on a convex closed184set `s`, `μ` is a finite non-zero measure on `α`, and `f : α → E` is a function sending185`μ`-a.e. points of a set `t` to `s`, then the average value of `g ∘ f` over `t` is less than or186equal to the value of `g` at the average value of `f` over `t` provided that both `f` and `g ∘ f`187are integrable. -/188theorem ConcaveOn.le_map_set_average (hg : ConcaveOn ℝ s g) (hgc : ContinuousOn g s)189 (hsc : IsClosed s) (h0 : μ t ≠ 0) (ht : μ t ≠ ∞) (hfs : ∀ᵐ x ∂μ.restrict t, f x ∈ s)190 (hfi : IntegrableOn f t μ) (hgi : IntegrableOn (g ∘ f) t μ) :191 (⨍ x in t, g (f x) ∂μ) ≤ g (⨍ x in t, f x ∂μ) :=192 (hg.set_average_mem_hypograph hgc hsc h0 ht hfs hfi hgi).2193194/-- **Jensen's inequality**: if a function `g : E → ℝ` is convex and continuous on a convex closed195set `s`, `μ` is a probability measure on `α`, and `f : α → E` is a function sending `μ`-a.e. points196to `s`, then the value of `g` at the expected value of `f` is less than or equal to the expected197value of `g ∘ f` provided that both `f` and `g ∘ f` are integrable. See also198`ConvexOn.map_centerMass_le` for a finite sum version of this lemma. -/199theorem ConvexOn.map_integral_le [IsProbabilityMeasure μ] (hg : ConvexOn ℝ s g)200 (hgc : ContinuousOn g s) (hsc : IsClosed s) (hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : Integrable f μ)201 (hgi : Integrable (g ∘ f) μ) : g (∫ x, f x ∂μ) ≤ ∫ x, g (f x) ∂μ := by202 simpa only [average_eq_integral] using hg.map_average_le hgc hsc hfs hfi hgi203204/-- **Jensen's inequality**: if a function `g : E → ℝ` is concave and continuous on a convex closed205set `s`, `μ` is a probability measure on `α`, and `f : α → E` is a function sending `μ`-a.e. points206to `s`, then the expected value of `g ∘ f` is less than or equal to the value of `g` at the expected207value of `f` provided that both `f` and `g ∘ f` are integrable. -/208theorem ConcaveOn.le_map_integral [IsProbabilityMeasure μ] (hg : ConcaveOn ℝ s g)209 (hgc : ContinuousOn g s) (hsc : IsClosed s) (hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : Integrable f μ)210 (hgi : Integrable (g ∘ f) μ) : (∫ x, g (f x) ∂μ) ≤ g (∫ x, f x ∂μ) := by211 simpa only [average_eq_integral] using hg.le_map_average hgc hsc hfs hfi hgi212213/-!214### Strict Jensen's inequality215-/216217218/-- If `f : α → E` is an integrable function, then either it is a.e. equal to the constant219`⨍ x, f x ∂μ` or there exists a measurable set such that `μ t ≠ 0`, `μ tᶜ ≠ 0`, and the average220values of `f` over `t` and `tᶜ` are different. -/221theorem ae_eq_const_or_exists_average_ne_compl [IsFiniteMeasure μ] (hfi : Integrable f μ) :222 f =ᵐ[μ] const α (⨍ x, f x ∂μ) ∨223 ∃ t, MeasurableSet t ∧ μ t ≠ 0 ∧ μ tᶜ ≠ 0 ∧ (⨍ x in t, f x ∂μ) ≠ ⨍ x in tᶜ, f x ∂μ := by224 refine or_iff_not_imp_right.mpr fun H => ?_; push Not at H225 refine hfi.ae_eq_of_forall_setIntegral_eq _ _ (integrable_const _) fun t ht ht' => ?_; clear ht'226 simp only [const_apply, setIntegral_const]227 by_cases h₀ : μ t = 0228 · rw [restrict_eq_zero.2 h₀, integral_zero_measure, measureReal_def, h₀,229 ENNReal.toReal_zero, zero_smul]230 by_cases h₀' : μ tᶜ = 0231 · rw [← ae_eq_univ] at h₀'232 rw [restrict_congr_set h₀', restrict_univ, measureReal_congr h₀', measure_smul_average]233 have := average_mem_openSegment_compl_self ht.nullMeasurableSet h₀ h₀' hfi234 rw [← H t ht h₀ h₀', openSegment_same, mem_singleton_iff] at this235 rw [this, measure_smul_setAverage _ (by finiteness)]236237/-- If an integrable function `f : α → E` takes values in a convex set `s` and for some set `t` of238positive measure, the average value of `f` over `t` belongs to the interior of `s`, then the average239of `f` over the whole space belongs to the interior of `s`. -/240theorem Convex.average_mem_interior_of_set [IsFiniteMeasure μ] (hs : Convex ℝ s) (h0 : μ t ≠ 0)241 (hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : Integrable f μ) (ht : (⨍ x in t, f x ∂μ) ∈ interior s) :242 (⨍ x, f x ∂μ) ∈ interior s := by243 rw [← measure_toMeasurable] at h0; rw [← restrict_toMeasurable (by finiteness)] at ht244 by_cases h0' : μ (toMeasurable μ t)ᶜ = 0245 · rw [← ae_eq_univ] at h0'246 rwa [restrict_congr_set h0', restrict_univ] at ht247 exact hs.openSegment_interior_closure_subset_interior ht248 (hs.set_average_mem_closure h0' (by finiteness) (ae_restrict_of_ae hfs) hfi.integrableOn)249 (average_mem_openSegment_compl_self (measurableSet_toMeasurable μ t).nullMeasurableSet h0250 h0' hfi)251252/-- If an integrable function `f : α → E` takes values in a strictly convex closed set `s`, then253either it is a.e. equal to its average value, or its average value belongs to the interior of254`s`. -/255theorem StrictConvex.ae_eq_const_or_average_mem_interior [IsFiniteMeasure μ] (hs : StrictConvex ℝ s)256 (hsc : IsClosed s) (hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : Integrable f μ) :257 f =ᵐ[μ] const α (⨍ x, f x ∂μ) ∨ (⨍ x, f x ∂μ) ∈ interior s := by258 have : ∀ {t}, μ t ≠ 0 → (⨍ x in t, f x ∂μ) ∈ s := fun ht =>259 hs.convex.set_average_mem hsc ht (by finiteness) (ae_restrict_of_ae hfs) hfi.integrableOn260 refine (ae_eq_const_or_exists_average_ne_compl hfi).imp_right ?_261 rintro ⟨t, hm, h₀, h₀', hne⟩262 exact263 hs.openSegment_subset (this h₀) (this h₀') hne264 (average_mem_openSegment_compl_self hm.nullMeasurableSet h₀ h₀' hfi)265266/-- **Jensen's inequality**, strict version: if an integrable function `f : α → E` takes values in a267convex closed set `s`, and `g : E → ℝ` is continuous and strictly convex on `s`, then268either `f` is a.e. equal to its average value, or `g (⨍ x, f x ∂μ) < ⨍ x, g (f x) ∂μ`. -/269theorem StrictConvexOn.ae_eq_const_or_map_average_lt [IsFiniteMeasure μ] (hg : StrictConvexOn ℝ s g)270 (hgc : ContinuousOn g s) (hsc : IsClosed s) (hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : Integrable f μ)271 (hgi : Integrable (g ∘ f) μ) :272 f =ᵐ[μ] const α (⨍ x, f x ∂μ) ∨ g (⨍ x, f x ∂μ) < ⨍ x, g (f x) ∂μ := by273 have : ∀ {t}, μ t ≠ 0 → (⨍ x in t, f x ∂μ) ∈ s ∧ g (⨍ x in t, f x ∂μ) ≤ ⨍ x in t, g (f x) ∂μ :=274 fun ht =>275 hg.convexOn.set_average_mem_epigraph hgc hsc ht (by finiteness) (ae_restrict_of_ae hfs)276 hfi.integrableOn hgi.integrableOn277 refine (ae_eq_const_or_exists_average_ne_compl hfi).imp_right ?_278 rintro ⟨t, hm, h₀, h₀', hne⟩279 rcases average_mem_openSegment_compl_self hm.nullMeasurableSet h₀ h₀' (hfi.prodMk hgi) with280 ⟨a, b, ha, hb, hab, h_avg⟩281 rw [average_pair hfi hgi, average_pair hfi.integrableOn hgi.integrableOn,282 average_pair hfi.integrableOn hgi.integrableOn, Prod.smul_mk,283 Prod.smul_mk, Prod.mk_add_mk, Prod.mk_inj] at h_avg284 simp only [Function.comp] at h_avg285 rw [← h_avg.1, ← h_avg.2]286 calc287 g ((a • ⨍ x in t, f x ∂μ) + b • ⨍ x in tᶜ, f x ∂μ) <288 a * g (⨍ x in t, f x ∂μ) + b * g (⨍ x in tᶜ, f x ∂μ) :=289 hg.2 (this h₀).1 (this h₀').1 hne ha hb hab290 _ ≤ (a * ⨍ x in t, g (f x) ∂μ) + b * ⨍ x in tᶜ, g (f x) ∂μ := by291 gcongr292 exacts [(this h₀).2, (this h₀').2]293294/-- **Jensen's inequality**, strict version: if an integrable function `f : α → E` takes values in a295convex closed set `s`, and `g : E → ℝ` is continuous and strictly concave on `s`, then296either `f` is a.e. equal to its average value, or `⨍ x, g (f x) ∂μ < g (⨍ x, f x ∂μ)`. -/297theorem StrictConcaveOn.ae_eq_const_or_lt_map_average [IsFiniteMeasure μ]298 (hg : StrictConcaveOn ℝ s g) (hgc : ContinuousOn g s) (hsc : IsClosed s)299 (hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : Integrable f μ) (hgi : Integrable (g ∘ f) μ) :300 f =ᵐ[μ] const α (⨍ x, f x ∂μ) ∨ (⨍ x, g (f x) ∂μ) < g (⨍ x, f x ∂μ) := by301 simpa only [Pi.neg_apply, average_neg, neg_lt_neg_iff] using302 hg.neg.ae_eq_const_or_map_average_lt hgc.neg hsc hfs hfi hgi.neg303304/-- If `E` is a strictly convex normed space and `f : α → E` is a function such that `‖f x‖ ≤ C`305a.e., then either this function is a.e. equal to its average value, or the norm of its average value306is strictly less than `C`. -/307theorem ae_eq_const_or_norm_average_lt_of_norm_le_const [StrictConvexSpace ℝ E]308 (h_le : ∀ᵐ x ∂μ, ‖f x‖ ≤ C) : f =ᵐ[μ] const α (⨍ x, f x ∂μ) ∨ ‖⨍ x, f x ∂μ‖ < C := by309 rcases le_or_gt C 0 with hC0 | hC0310 · have : f =ᵐ[μ] 0 := h_le.mono fun x hx => norm_le_zero_iff.1 (hx.trans hC0)311 simp only [average_congr this, Pi.zero_apply, average_zero]312 exact Or.inl this313 by_cases hfi : Integrable f μ; swap314 · simp [average_eq, integral_undef hfi, hC0]315 rcases (le_top : μ univ ≤ ∞).eq_or_lt with hμt | hμt316 · simp [average_eq, measureReal_def, hμt, hC0]317 haveI : IsFiniteMeasure μ := ⟨hμt⟩318 replace h_le : ∀ᵐ x ∂μ, f x ∈ closedBall (0 : E) C := by simpa only [mem_closedBall_zero_iff]319 simpa only [interior_closedBall _ hC0.ne', mem_ball_zero_iff] using320 (strictConvex_closedBall ℝ (0 : E) C).ae_eq_const_or_average_mem_interior isClosed_closedBall321 h_le hfi322323/-- If `E` is a strictly convex normed space and `f : α → E` is a function such that `‖f x‖ ≤ C`324a.e., then either this function is a.e. equal to its average value, or the norm of its integral is325strictly less than `μ.real univ * C`. -/326theorem ae_eq_const_or_norm_integral_lt_of_norm_le_const [StrictConvexSpace ℝ E] [IsFiniteMeasure μ]327 (h_le : ∀ᵐ x ∂μ, ‖f x‖ ≤ C) :328 f =ᵐ[μ] const α (⨍ x, f x ∂μ) ∨ ‖∫ x, f x ∂μ‖ < μ.real univ * C := by329 rcases eq_or_ne μ 0 with h₀ | h₀; · simp [h₀, EventuallyEq]330 have hμ : 0 < μ.real univ := by331 simp [measureReal_def, ENNReal.toReal_pos_iff, pos_iff_ne_zero, h₀, measure_lt_top]332 refine (ae_eq_const_or_norm_average_lt_of_norm_le_const h_le).imp_right fun H => ?_333 rwa [average_eq, norm_smul, norm_inv, Real.norm_eq_abs, abs_of_pos hμ, ← div_eq_inv_mul,334 div_lt_iff₀' hμ] at H335336/-- If `E` is a strictly convex normed space and `f : α → E` is a function such that `‖f x‖ ≤ C`337a.e. on a set `t` of finite measure, then either this function is a.e. equal to its average value on338`t`, or the norm of its integral over `t` is strictly less than `μ.real t * C`. -/339theorem ae_eq_const_or_norm_setIntegral_lt_of_norm_le_const [StrictConvexSpace ℝ E] (ht : μ t ≠ ∞)340 (h_le : ∀ᵐ x ∂μ.restrict t, ‖f x‖ ≤ C) :341 f =ᵐ[μ.restrict t] const α (⨍ x in t, f x ∂μ) ∨ ‖∫ x in t, f x ∂μ‖ < μ.real t * C := by342 haveI := Fact.mk ht.lt_top343 rw [← measureReal_restrict_apply_univ]344 exact ae_eq_const_or_norm_integral_lt_of_norm_le_const h_le