diff --git a/Mathlib.lean b/Mathlib.lean index 2ba33f02117f1e..bc38fd6eade688 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -5611,9 +5611,13 @@ public import Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub public import Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue public import Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym public import Mathlib.MeasureTheory.VectorMeasure.Integral +public import Mathlib.MeasureTheory.VectorMeasure.Prod +public import Mathlib.MeasureTheory.VectorMeasure.SetIntegral public import Mathlib.MeasureTheory.VectorMeasure.Variation.Basic public import Mathlib.MeasureTheory.VectorMeasure.Variation.Defs +public import Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation public import Mathlib.MeasureTheory.VectorMeasure.WithDensity +public import Mathlib.MeasureTheory.VectorMeasure.WithDensityVec public import Mathlib.ModelTheory.Algebra.Field.Basic public import Mathlib.ModelTheory.Algebra.Field.CharP public import Mathlib.ModelTheory.Algebra.Field.IsAlgClosed diff --git a/Mathlib/Analysis/Normed/Group/Continuity.lean b/Mathlib/Analysis/Normed/Group/Continuity.lean index 609c44b07dde86..e4e9048e9eaae7 100644 --- a/Mathlib/Analysis/Normed/Group/Continuity.lean +++ b/Mathlib/Analysis/Normed/Group/Continuity.lean @@ -7,6 +7,7 @@ module public import Mathlib.Analysis.Normed.Group.Basic public import Mathlib.Topology.Algebra.Ring.Real +public import Mathlib.Topology.Instances.ENNReal.Lemmas public import Mathlib.Topology.Metrizable.Uniformity public import Mathlib.Topology.Sequences @@ -68,6 +69,16 @@ theorem tendsto_one_iff_norm_tendsto_zero {f : α → E} {a : Filter α} : Tendsto f a (𝓝 1) ↔ Tendsto (‖f ·‖) a (𝓝 0) := tendsto_iff_norm_inv_mul_tendsto_zero.trans <| by simp +@[to_additive] +theorem tendsto_iff_enorm_inv_mul_tendsto_zero {f : α → E} {a : Filter α} {b : E} : + Tendsto f a (𝓝 b) ↔ Tendsto (fun e => ‖(f e)⁻¹ * b‖ₑ) a (𝓝 0) := by + simp only [← edist_eq_enorm_inv_mul, ← tendsto_iff_edist_tendsto_0] + +@[to_additive] +theorem tendsto_one_iff_enorm_tendsto_zero {f : α → E} {a : Filter α} : + Tendsto f a (𝓝 1) ↔ Tendsto (‖f ·‖ₑ) a (𝓝 0) := + tendsto_iff_enorm_inv_mul_tendsto_zero.trans <| by simp + @[to_additive (attr := simp 1100)] theorem comap_norm_nhds_one : comap norm (𝓝 0) = 𝓝 (1 : E) := by simpa only [dist_one_right] using nhds_comap_dist (1 : E) @@ -302,6 +313,11 @@ theorem tendsto_iff_norm_div_tendsto_zero {f : α → E} {a : Filter α} {b : E} Tendsto f a (𝓝 b) ↔ Tendsto (fun e => ‖f e / b‖) a (𝓝 0) := by simp only [← dist_eq_norm_div, ← tendsto_iff_dist_tendsto_zero] +@[to_additive] +theorem tendsto_iff_enorm_div_tendsto_zero {f : α → E} {a : Filter α} {b : E} : + Tendsto f a (𝓝 b) ↔ Tendsto (fun e => ‖f e / b‖ₑ) a (𝓝 0) := by + simp only [← edist_eq_enorm_div, ← tendsto_iff_edist_tendsto_0] + @[to_additive] theorem SeminormedCommGroup.mem_closure_iff {s : Set E} : a ∈ closure s ↔ ∀ ε, 0 < ε → ∃ b ∈ s, ‖a / b‖ < ε := by diff --git a/Mathlib/Analysis/Normed/Operator/Bilinear.lean b/Mathlib/Analysis/Normed/Operator/Bilinear.lean index 187148928cc83d..909c07e8acd2f5 100644 --- a/Mathlib/Analysis/Normed/Operator/Bilinear.lean +++ b/Mathlib/Analysis/Normed/Operator/Bilinear.lean @@ -165,6 +165,14 @@ theorem flip_flip (f : E →SL[σ₁₃] F →SL[σ₂₃] G) : f.flip.flip = f theorem opNorm_flip (f : E →SL[σ₁₃] F →SL[σ₂₃] G) : ‖f.flip‖ = ‖f‖ := le_antisymm (by simpa only [flip_flip] using le_norm_flip f.flip) (le_norm_flip f) +@[simp] +theorem opNNNorm_flip (f : E →SL[σ₁₃] F →SL[σ₂₃] G) : ‖f.flip‖₊ = ‖f‖₊ := by + simp [← NNReal.coe_inj] + +@[simp] +theorem opENorm_flip (f : E →SL[σ₁₃] F →SL[σ₂₃] G) : ‖f.flip‖ₑ = ‖f‖ₑ := by + simp [enorm_eq_nnnorm] + @[simp] lemma flip_zero : flip (0 : E →SL[σ₁₃] F →SL[σ₂₃] G) = 0 := rfl diff --git a/Mathlib/Analysis/Normed/Operator/Mul.lean b/Mathlib/Analysis/Normed/Operator/Mul.lean index 1ed482a0a80254..3cf11c69837973 100644 --- a/Mathlib/Analysis/Normed/Operator/Mul.lean +++ b/Mathlib/Analysis/Normed/Operator/Mul.lean @@ -221,6 +221,10 @@ theorem opNNNorm_lsmul_le : ‖(lsmul 𝕜 R : R →L[𝕜] E →L[𝕜] E)‖ rw [← NNReal.coe_le_coe] simpa using opNorm_lsmul_le +theorem opENorm_lsmul_le : ‖(lsmul 𝕜 R : R →L[𝕜] E →L[𝕜] E)‖ₑ ≤ 1 := by + rw [enorm_eq_nnnorm] + simpa using opNNNorm_lsmul_le + end SMulLinear end ContinuousLinearMap @@ -247,6 +251,10 @@ theorem opNorm_mul : ‖mul 𝕜 R‖ = 1 := theorem opNNNorm_mul : ‖mul 𝕜 R‖₊ = 1 := Subtype.ext <| opNorm_mul 𝕜 R +@[simp] +theorem opENorm_mul : ‖mul 𝕜 R‖ₑ = 1 := by + simp [enorm_eq_nnnorm] + end /-- The norm of `lsmul` equals 1 in any nontrivial normed group. @@ -268,6 +276,11 @@ theorem opNNNorm_lsmul [NormedDivisionRing R] [NormedAlgebra 𝕜 R] [Module R E rw [← NNReal.coe_inj] simp +@[simp] +theorem opENorm_lsmul [NormedDivisionRing R] [NormedAlgebra 𝕜 R] [Module R E] [NormSMulClass R E] + [IsScalarTower 𝕜 R E] [Nontrivial E] : ‖(lsmul 𝕜 R : R →L[𝕜] E →L[𝕜] E)‖ₑ = 1 := by + simp [enorm_eq_nnnorm] + /-- The norm of `lsmul x` equals `‖x‖` in any nontrivial normed group. This is `ContinuousLinearMap.opNorm_lsmul_apply_le` as an equality. -/ @@ -288,6 +301,12 @@ theorem opNNNorm_lsmul_apply [NormedDivisionRing R] [NormedAlgebra 𝕜 R] [Modu rw [← NNReal.coe_inj] simp +@[simp] +theorem opENorm_lsmul_apply [NormedDivisionRing R] [NormedAlgebra 𝕜 R] [Module R E] + [NormSMulClass R E] [IsScalarTower 𝕜 R E] [Nontrivial E] {a : R} : + ‖(lsmul 𝕜 R a : E →L[𝕜] E)‖ₑ = ‖a‖ₑ := by + simp [enorm_eq_nnnorm] + end ContinuousLinearMap end Normed diff --git a/Mathlib/Data/NNReal/Defs.lean b/Mathlib/Data/NNReal/Defs.lean index 612791983d60ef..41e15f10ecf1e6 100644 --- a/Mathlib/Data/NNReal/Defs.lean +++ b/Mathlib/Data/NNReal/Defs.lean @@ -127,6 +127,8 @@ noncomputable instance : LinearOrderedCommGroupWithZero ℝ≥0 where example {p q : ℝ≥0} (h1p : 0 < p) (h2p : p ≤ q) : q⁻¹ ≤ p⁻¹ := by with_reducible_and_instances exact inv_anti₀ h1p h2p +@[simp] lemma mk_coe (a : ℝ≥0) (ha : 0 ≤ (a : ℝ)) : NNReal.mk (a : ℝ) ha = a := rfl + -- Simp lemma to put back `n.val` into the normal form given by the coercion. @[simp] theorem val_eq_coe (n : ℝ≥0) : n.val = n := diff --git a/Mathlib/MeasureTheory/Constructions/Polish/StronglyMeasurable.lean b/Mathlib/MeasureTheory/Constructions/Polish/StronglyMeasurable.lean index 1676161053d094..2582708a2b5916 100644 --- a/Mathlib/MeasureTheory/Constructions/Polish/StronglyMeasurable.lean +++ b/Mathlib/MeasureTheory/Constructions/Polish/StronglyMeasurable.lean @@ -82,12 +82,22 @@ variable {X E ι : Type*} [MeasurableSpace X] [CommMonoid E] [TopologicalSpace E section -variable [IsCompletelyPseudoMetrizableSpace E] [ContinuousMul E] - [Countable ι] {L : SummationFilter ι} [L.NeBot] [L.filter.IsCountablyGenerated] +variable [ContinuousMul E] {L : SummationFilter ι} [L.NeBot] [L.filter.IsCountablyGenerated] -/-- The product of strongly measurable functions is measurable. -/ +/-- The infinite product of strongly measurable functions is measurable, `HasProd` version. -/ @[to_additive (attr := fun_prop) -/-- The sum of strongly measurable functions is measurable. -/] +/-- The infinite sum of strongly measurable functions is measurable, `HasSum` version. -/] +theorem StronglyMeasurable.hasProd [PseudoMetrizableSpace E] {f : ι → X → E} {g : X → E} + (h : ∀ i : ι, StronglyMeasurable (f i)) (h' : ∀ x, HasProd (fun i ↦ f i x) (g x) L) : + StronglyMeasurable g := by + refine stronglyMeasurable_of_tendsto L.filter ?_ (tendsto_pi_nhds.mpr h') + fun_prop + +variable [IsCompletelyPseudoMetrizableSpace E] [Countable ι] + +/-- The infinite product of strongly measurable functions is measurable. -/ +@[to_additive (attr := fun_prop) +/-- The infinite sum of strongly measurable functions is measurable. -/] theorem StronglyMeasurable.tprod {f : ι → X → E} (h : ∀ i : ι, StronglyMeasurable (f i)) : StronglyMeasurable (fun x => ∏'[L] i : ι, f i x) := by let E := { x | Multipliable (f · x) L } diff --git a/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean b/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean index 96fc1608bff08b..6ff9c1d3559d40 100644 --- a/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean +++ b/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean @@ -661,6 +661,12 @@ theorem eLpNorm_smul_measure_of_ne_zero {c : ℝ≥0∞} (hc : c ≠ 0) (f : α · simp [*] exact eLpNorm_smul_measure_of_ne_zero_of_ne_top hp0 hp_top c +theorem eLpNorm_smul_measure_le (c : ℝ≥0∞) (f : α → ε) (p : ℝ≥0∞) + (μ : Measure α) : eLpNorm f p (c • μ) ≤ c ^ (1 / p).toReal • eLpNorm f p μ := by + rcases eq_or_ne c 0 with rfl | hc + · simp + · exact (eLpNorm_smul_measure_of_ne_zero hc f p μ ).le + /-- See `eLpNorm_smul_measure_of_ne_zero` for a version with scalar multiplication by `ℝ≥0∞`. -/ lemma eLpNorm_smul_measure_of_ne_zero' {c : ℝ≥0} (hc : c ≠ 0) (f : α → ε) (p : ℝ≥0∞) (μ : Measure α) : eLpNorm f p (c • μ) = c ^ p.toReal⁻¹ • eLpNorm f p μ := @@ -684,15 +690,16 @@ theorem eLpNorm_one_smul_measure {f : α → ε} (c : ℝ≥0∞) : eLpNorm f 1 (c • μ) = c * eLpNorm f 1 μ := by rw [eLpNorm_smul_measure_of_ne_top] <;> simp +theorem eLpNorm_le_of_measure_le_smul {c : ℝ≥0∞} + {μ μ' : Measure α} (h : μ' ≤ c • μ) {f : α → ε} {p : ℝ≥0∞} : + eLpNorm f p μ' ≤ c ^ (1 / p).toReal • eLpNorm f p μ := by + grw [eLpNorm_mono_measure f h, eLpNorm_smul_measure_le] + theorem MemLp.of_measure_le_smul {μ' : Measure α} {c : ℝ≥0∞} (hc : c ≠ ∞) (hμ'_le : μ' ≤ c • μ) {f : α → ε} (hf : MemLp f p μ) : MemLp f p μ' := by refine ⟨hf.1.mono_ac (Measure.absolutelyContinuous_of_le_smul hμ'_le), ?_⟩ - refine (eLpNorm_mono_measure f hμ'_le).trans_lt ?_ - by_cases hc0 : c = 0 - · simp [hc0] - rw [eLpNorm_smul_measure_of_ne_zero hc0, smul_eq_mul] - refine ENNReal.mul_lt_top (Ne.lt_top ?_) hf.2 - simp [hc, hc0] + grw [eLpNorm_le_of_measure_le_smul hμ'_le] + exact ENNReal.mul_lt_top (Ne.lt_top (by simp [hc])) hf.2 theorem MemLp.smul_measure {f : α → ε} {c : ℝ≥0∞} (hf : MemLp f p μ) (hc : c ≠ ∞) : MemLp f p (c • μ) := diff --git a/Mathlib/MeasureTheory/Function/LpSpace/Basic.lean b/Mathlib/MeasureTheory/Function/LpSpace/Basic.lean index f66de7c766a34e..87bc16d4c4b653 100644 --- a/Mathlib/MeasureTheory/Function/LpSpace/Basic.lean +++ b/Mathlib/MeasureTheory/Function/LpSpace/Basic.lean @@ -232,7 +232,6 @@ theorem nnnorm_def (f : Lp E p μ) : ‖f‖₊ = ENNReal.toNNReal (eLpNorm f p protected theorem coe_nnnorm (f : Lp E p μ) : (‖f‖₊ : ℝ) = ‖f‖ := rfl -@[simp] theorem enorm_def (f : Lp E p μ) : ‖f‖ₑ = eLpNorm f p μ := ENNReal.coe_toNNReal <| Lp.eLpNorm_ne_top f @@ -245,6 +244,7 @@ theorem nnnorm_toLp (f : α → E) (hf : MemLp f p μ) : ‖hf.toLp f‖₊ = ENNReal.toNNReal (eLpNorm f p μ) := NNReal.eq <| norm_toLp f hf +@[simp] lemma enorm_toLp {f : α → E} (hf : MemLp f p μ) : ‖hf.toLp f‖ₑ = eLpNorm f p μ := by simp_rw [enorm, nnnorm_toLp f hf, ENNReal.coe_toNNReal hf.2.ne] @@ -869,6 +869,66 @@ end ContinuousLinearMap namespace MeasureTheory.Lp +section LpToLpOfMeasureLeSMul + +variable [NormedSpace ℝ E] {ν : Measure α} {c : ℝ≥0∞} + +/-- The canonical map from `Lᵖ ν` to `Lᵖ μ` when `μ` is bounded by a multiple of `ν`. +This is the linear map version. Use instead the continuous linear map +version `LpToLpOfMeasureLeSMul` -/ +noncomputable def LpToLpOfMeasureLeSMulₗ (hc : c ≠ ∞) (h : μ ≤ c • ν) : + Lp E p ν →ₗ[ℝ] Lp E p μ where + toFun f := ((Lp.memLp f).of_measure_le_smul hc h).toLp f + map_add' f g := by + ext + grw [MemLp.coeFn_toLp, Lp.coeFn_add, MemLp.coeFn_toLp, MemLp.coeFn_toLp] + have : μ ≪ ν := Measure.absolutelyContinuous_of_le_smul h + apply Measure.AbsolutelyContinuous.ae_eq this + grw [Lp.coeFn_add] + map_smul' c f := by + ext + grw [MemLp.coeFn_toLp, Lp.coeFn_smul, MemLp.coeFn_toLp] + have : μ ≪ ν := Measure.absolutelyContinuous_of_le_smul h + apply Measure.AbsolutelyContinuous.ae_eq this + grw [Lp.coeFn_smul] + rfl + +lemma coeFn_LpToLpOfMeasureLeSMulₗ (hc : c ≠ ∞) (h : μ ≤ c • ν) (f : Lp E p ν) : + LpToLpOfMeasureLeSMulₗ hc h f =ᵐ[μ] f := by + simp [LpToLpOfMeasureLeSMulₗ, MemLp.coeFn_toLp] + +lemma enorm_LpToLpOfMeasureLeSMulₗ_apply_le + (hc : c ≠ ∞) (h : μ ≤ c • ν) [Fact (1 ≤ p)] {f : Lp E p ν} : + ‖LpToLpOfMeasureLeSMulₗ hc h f‖ₑ ≤ c ^ (1 / p).toReal * ‖f‖ₑ := by + simp only [Lp.enorm_def] + grw [eLpNorm_congr_ae (coeFn_LpToLpOfMeasureLeSMulₗ hc h f)] + exact eLpNorm_le_of_measure_le_smul h + +lemma norm_LpToLpOfMeasureLeSMulₗ_apply_le + (hc : c ≠ ∞) (h : μ ≤ c • ν) [Fact (1 ≤ p)] {f : Lp E p ν} : + ‖LpToLpOfMeasureLeSMulₗ hc h f‖ ≤ c.toReal ^ (1 / p).toReal * ‖f‖ := by + simp only [← toReal_enorm] + rw [ENNReal.toReal_rpow, ← ENNReal.toReal_mul] + apply (ENNReal.toReal_le_toReal (by simp only [ne_eq, enorm_ne_top, not_false_eq_true]) _).2 + (enorm_LpToLpOfMeasureLeSMulₗ_apply_le hc h) + simp [ENNReal.mul_eq_top, hc] + +/-- The canonical map from `Lᵖ ν` to `Lᵖ μ` when `μ` is bounded by a multiple of `ν`. -/ +noncomputable def LpToLpOfMeasureLeSMul [Fact (1 ≤ p)] (hc : c ≠ ∞) (h : μ ≤ c • ν) : + Lp E p ν →L[ℝ] Lp E p μ := + LinearMap.mkContinuous (LpToLpOfMeasureLeSMulₗ hc h) (c.toReal ^ (1 / p).toReal) + (fun _ ↦ norm_LpToLpOfMeasureLeSMulₗ_apply_le hc h) + +lemma coeFn_LpToLpOfMeasureLeSMul [Fact (1 ≤ p)] (hc : c ≠ ∞) (h : μ ≤ c • ν) (f : Lp E p ν) : + LpToLpOfMeasureLeSMul hc h f =ᵐ[μ] f := + coeFn_LpToLpOfMeasureLeSMulₗ hc h f + +lemma norm_LpToLpOfMeasureLeSMul [Fact (1 ≤ p)] (hc : c ≠ ∞) (h : μ ≤ c • ν) : + ‖(LpToLpOfMeasureLeSMul hc h : Lp E p ν →L[ℝ] Lp E p μ)‖ ≤ c.toReal ^ (1 / p).toReal := + LinearMap.mkContinuous_norm_le _ (Real.rpow_nonneg (by simp) _) _ + +end LpToLpOfMeasureLeSMul + section PosPart theorem lipschitzWith_pos_part : LipschitzWith 1 fun x : ℝ => max x 0 := diff --git a/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean b/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean index d6a80a4a9e1495..1a9b39c030e3d8 100644 --- a/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean +++ b/Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean @@ -322,6 +322,18 @@ theorem setToSimpleFunc_eq_sum_filter [DecidablePred fun x ↦ x ≠ (0 : F)] rw [hx0] exact map_zero _ +/-- The `setToSimpleFunc` is equal to a sum over any set that includes `f.range` (except `0`). -/ +theorem setToSimpleFunc_eq_sum_of_subset [DecidablePred fun x : F => x ≠ 0] + (T : Set α → F →L[ℝ] F') (hT : T ∅ = 0) {f : α →ₛ F} {s : Finset F} + (hs : {x ∈ f.range | x ≠ 0} ⊆ s) : + setToSimpleFunc T f = ∑ x ∈ s, T (f ⁻¹' {x}) x := by + rw [setToSimpleFunc_eq_sum_filter, Finset.sum_subset hs] + rintro x - hx; rw [Finset.mem_filter, not_and_or, Ne, Classical.not_not] at hx + rcases hx.symm with (rfl | hx) + · simp + rw [SimpleFunc.mem_range] at hx + rw [preimage_eq_empty] <;> simp [Set.disjoint_singleton_left, hx, hT] + theorem map_setToSimpleFunc (T : Set α → F →L[ℝ] F') (h_add : FinMeasAdditive μ T) {f : α →ₛ G} (hf : Integrable f μ) {g : G → F} (hg : g 0 = 0) : (f.map g).setToSimpleFunc T = ∑ x ∈ f.range, T (f ⁻¹' {x}) (g x) := by diff --git a/Mathlib/MeasureTheory/Integral/Prod.lean b/Mathlib/MeasureTheory/Integral/Prod.lean index de59485ec6289f..29aa2b79574237 100644 --- a/Mathlib/MeasureTheory/Integral/Prod.lean +++ b/Mathlib/MeasureTheory/Integral/Prod.lean @@ -7,6 +7,7 @@ module public import Mathlib.MeasureTheory.Function.LpSeminorm.Prod public import Mathlib.MeasureTheory.Integral.DominatedConvergence +public import Mathlib.MeasureTheory.Integral.SetToL1 public import Mathlib.MeasureTheory.Integral.Bochner.Set public import Mathlib.MeasureTheory.Measure.Prod @@ -37,7 +38,6 @@ product measure, Fubini's theorem, Fubini-Tonelli theorem public section - noncomputable section open scoped Topology ENNReal MeasureTheory @@ -60,12 +60,6 @@ functions. We show that if `f` is a binary measurable function, then the functio along one of the variables (using either the Lebesgue or Bochner integral) is measurable. -/ - -theorem measurableSet_integrable [SFinite ν] ⦃f : α → β → E⦄ - (hf : StronglyMeasurable (uncurry f)) : MeasurableSet {x | Integrable (f x) ν} := by - simp_rw [Integrable, hf.of_uncurry_left.aestronglyMeasurable, true_and] - exact measurableSet_lt (Measurable.lintegral_prod_right hf.enorm) measurable_const - section variable [NormedSpace ℝ E] @@ -75,49 +69,10 @@ variable [NormedSpace ℝ E] This version has `f` in curried form. -/ theorem MeasureTheory.StronglyMeasurable.integral_prod_right [SFinite ν] ⦃f : α → β → E⦄ (hf : StronglyMeasurable (uncurry f)) : StronglyMeasurable fun x => ∫ y, f x y ∂ν := by - classical - by_cases hE : CompleteSpace E; swap; · simp [integral, hE, stronglyMeasurable_const] - borelize E - haveI : SeparableSpace (range (uncurry f) ∪ {0} : Set E) := - hf.separableSpace_range_union_singleton - let s : ℕ → SimpleFunc (α × β) E := - SimpleFunc.approxOn _ hf.measurable (range (uncurry f) ∪ {0}) 0 (by simp) - let s' : ℕ → α → SimpleFunc β E := fun n x => (s n).comp (Prod.mk x) measurable_prodMk_left - let f' : ℕ → α → E := fun n => {x | Integrable (f x) ν}.indicator fun x => (s' n x).integral ν - have hf' : ∀ n, StronglyMeasurable (f' n) := by - intro n; refine StronglyMeasurable.indicator ?_ (measurableSet_integrable hf) - have : ∀ x, ((s' n x).range.filter fun x => x ≠ 0) ⊆ (s n).range := by - intro x; refine Finset.Subset.trans (Finset.filter_subset _ _) ?_; intro y - simp_rw [SimpleFunc.mem_range]; rintro ⟨z, rfl⟩; exact ⟨(x, z), rfl⟩ - simp only [SimpleFunc.integral_eq_sum_of_subset (this _)] - refine Finset.stronglyMeasurable_fun_sum _ fun x _ => ?_ - refine (Measurable.ennreal_toReal ?_).stronglyMeasurable.smul_const _ - simp only [s', SimpleFunc.coe_comp, preimage_comp] - apply measurable_measure_prodMk_left - exact (s n).measurableSet_fiber x - have h2f' : Tendsto f' atTop (𝓝 fun x : α => ∫ y : β, f x y ∂ν) := by - rw [tendsto_pi_nhds]; intro x - by_cases hfx : Integrable (f x) ν - · have (n : _) : Integrable (s' n x) ν := by - apply (hfx.norm.add hfx.norm).mono' (s' n x).aestronglyMeasurable - filter_upwards with y - simp_rw [s', SimpleFunc.coe_comp]; exact SimpleFunc.norm_approxOn_zero_le _ _ (x, y) n - simp only [f', hfx, SimpleFunc.integral_eq_integral _ (this _), indicator_of_mem, - mem_setOf_eq] - refine - tendsto_integral_of_dominated_convergence (fun y => ‖f x y‖ + ‖f x y‖) - (fun n => (s' n x).aestronglyMeasurable) (hfx.norm.add hfx.norm) ?_ ?_ - · refine fun n => Eventually.of_forall fun y => - SimpleFunc.norm_approxOn_zero_le ?_ ?_ (x, y) n - · exact hf.measurable - · simp - · refine Eventually.of_forall fun y => SimpleFunc.tendsto_approxOn ?_ ?_ ?_ - · exact hf.measurable.of_uncurry_left - · simp - apply subset_closure - simp [-uncurry_apply_pair] - · simp [f', hfx, integral_undef] - exact stronglyMeasurable_of_tendsto _ hf' h2f' + simp only [integral_eq_setToFun] + apply StronglyMeasurable.setToFun_prod_right _ (fun s hs ↦ ?_) hf + refine (Measurable.ennreal_toReal ?_).stronglyMeasurable.smul_const _ + exact measurable_measure_prodMk_left hs /-- The Bochner integral is measurable. This shows that the integrand of (the right-hand-side of) Fubini's theorem is measurable. -/ @@ -380,13 +335,11 @@ end variable [NormedSpace ℝ E] theorem Integrable.integral_prod_left ⦃f : α × β → E⦄ (hf : Integrable f (μ.prod ν)) : - Integrable (fun x => ∫ y, f (x, y) ∂ν) μ := - Integrable.mono hf.integral_norm_prod_left hf.aestronglyMeasurable.integral_prod_right' <| - Eventually.of_forall fun x => - (norm_integral_le_integral_norm _).trans_eq <| - (norm_of_nonneg <| - integral_nonneg_of_ae <| - Eventually.of_forall fun y => (norm_nonneg (f (x, y)) :)).symm + Integrable (fun x => ∫ y, f (x, y) ∂ν) μ := by + apply Integrable.mono hf.integral_norm_prod_left hf.aestronglyMeasurable.integral_prod_right' + filter_upwards with x + grw [norm_integral_le_integral_norm] + exact le_abs_self _ theorem Integrable.integral_prod_right [SFinite μ] ⦃f : α × β → E⦄ (hf : Integrable f (μ.prod ν)) : Integrable (fun y => ∫ x, f (x, y) ∂μ) ν := diff --git a/Mathlib/MeasureTheory/Integral/SetToL1.lean b/Mathlib/MeasureTheory/Integral/SetToL1.lean index 1af06506765fed..bd8c0a097c415a 100644 --- a/Mathlib/MeasureTheory/Integral/SetToL1.lean +++ b/Mathlib/MeasureTheory/Integral/SetToL1.lean @@ -844,6 +844,12 @@ theorem setToFun_simpleFunc [CompleteSpace F] (hT : DominatedFinMeasAdditive μ apply (SimpleFunc.setToSimpleFunc_congr T (fun s ↦ hT.eq_zero_of_measure_zero) hT.1 hf _).symm grw [A, Lp.simpleFunc.toSimpleFunc_eq_toFun] +theorem setToFun_simpleFunc_eq_setToSimpleFunc [CompleteSpace F] + (hT : DominatedFinMeasAdditive μ T C) (f : SimpleFunc α E) (hf : Integrable f μ) : + setToFun μ T hT f = f.setToSimpleFunc T := by + rw [setToFun_simpleFunc hT f hf] + rfl + section Order variable {G' G'' : Type*} @@ -1384,6 +1390,66 @@ theorem tendsto_setToFun_filter_of_norm_le_const (hT : DominatedFinMeasAdditive exact tendsto_setToFun_filter_of_dominated_convergence hT C h_meas h_boundc (integrable_const c) h_lim +omit [NormedSpace ℝ E] in +theorem _root_.measurableSet_integrable {β : Type*} {mβ : MeasurableSpace β} [SFinite μ] + ⦃f : β → α → E⦄ (hf : StronglyMeasurable (Function.uncurry f)) : + MeasurableSet {x | Integrable (f x) μ} := by + simp_rw [Integrable, hf.of_uncurry_left.aestronglyMeasurable, true_and] + exact measurableSet_lt (Measurable.lintegral_prod_right hf.enorm) measurable_const + +/-- The `setToFun` operation is measurable. This shows that the integrand of (the right-hand-side +of) Fubini's theorem is measurable. This version has `f` in curried form. -/ +theorem StronglyMeasurable.setToFun_prod_right {β : Type*} {mβ : MeasurableSpace β} [SFinite μ] + (hT : DominatedFinMeasAdditive μ T C) + (h'T : ∀ (s : Set (β × α)), MeasurableSet s → StronglyMeasurable fun x => T (Prod.mk x ⁻¹' s)) + ⦃f : β → α → E⦄ (hf : StronglyMeasurable (Function.uncurry f)) : + StronglyMeasurable fun x => setToFun μ T hT (f x) := by + classical + by_cases hF : CompleteSpace F; swap; + · simp [setToFun, hF, stronglyMeasurable_const] + borelize E + haveI : SeparableSpace (range (Function.uncurry f) ∪ {0} : Set E) := + hf.separableSpace_range_union_singleton + let s : ℕ → SimpleFunc (β × α) E := + SimpleFunc.approxOn _ hf.measurable (range (Function.uncurry f) ∪ {0}) 0 (by simp) + let s' : ℕ → β → SimpleFunc α E := fun n x => (s n).comp (Prod.mk x) measurable_prodMk_left + let f' : ℕ → β → F := fun n => + {x | Integrable (f x) μ}.indicator fun x => (s' n x).setToSimpleFunc T + have hf' n : StronglyMeasurable (f' n) := by + refine StronglyMeasurable.indicator ?_ (measurableSet_integrable hf) + have : ∀ x, ((s' n x).range.filter fun x => x ≠ 0) ⊆ (s n).range := by + intro x; refine Finset.Subset.trans (Finset.filter_subset _ _) ?_; intro y + simp_rw [SimpleFunc.mem_range]; rintro ⟨z, rfl⟩; exact ⟨(x, z), rfl⟩ + simp_rw [SimpleFunc.setToSimpleFunc_eq_sum_of_subset T hT.1.map_empty_eq_zero (this _)] + refine Finset.stronglyMeasurable_fun_sum _ fun x _ => ?_ + simp only [s', SimpleFunc.coe_comp, preimage_comp] + apply StronglyMeasurable.apply_continuousLinearMap + apply h'T + exact (s n).measurableSet_fiber x + have h2f' : Tendsto f' atTop (𝓝 fun x : β => setToFun μ T hT (f x)) := by + apply tendsto_pi_nhds.2 fun x ↦ ?_ + by_cases hfx : Integrable (f x) μ + · have (n : _) : Integrable (s' n x) μ := by + apply (hfx.norm.add hfx.norm).mono' (s' n x).aestronglyMeasurable + filter_upwards with y + simp_rw [s', SimpleFunc.coe_comp]; exact SimpleFunc.norm_approxOn_zero_le _ _ (x, y) n + simp only [mem_setOf_eq, hfx, indicator_of_mem, this, + ← setToFun_simpleFunc_eq_setToSimpleFunc hT, f'] + refine + tendsto_setToFun_of_dominated_convergence hT (fun y => ‖f x y‖ + ‖f x y‖) + (fun n => (s' n x).aestronglyMeasurable) (hfx.norm.add hfx.norm) ?_ ?_ + · refine fun n => Eventually.of_forall fun y => + SimpleFunc.norm_approxOn_zero_le ?_ ?_ (x, y) n + · exact hf.measurable + · simp + · refine Eventually.of_forall fun y => SimpleFunc.tendsto_approxOn ?_ ?_ ?_ + · exact hf.measurable.of_uncurry_left + · simp + apply subset_closure + simp [-Function.uncurry_apply_pair] + · simp [f', hfx, setToFun_undef] + exact stronglyMeasurable_of_tendsto _ hf' h2f' + variable {X : Type*} [TopologicalSpace X] [FirstCountableTopology X] theorem continuousWithinAt_setToFun_of_dominated (hT : DominatedFinMeasAdditive μ T C) diff --git a/Mathlib/MeasureTheory/Measure/Prod.lean b/Mathlib/MeasureTheory/Measure/Prod.lean index e9f92b71955eb6..1dbfadd2cc5f2b 100644 --- a/Mathlib/MeasureTheory/Measure/Prod.lean +++ b/Mathlib/MeasureTheory/Measure/Prod.lean @@ -419,6 +419,14 @@ theorem AbsolutelyContinuous.prod [SFinite ν'] (h1 : μ ≪ μ') (h2 : ν ≪ rw [measure_prod_null hs] at h2s exact (h2s.filter_mono h1.ae_le).mono fun _ h => h2 h +omit [SFinite ν] in +@[gcongr] theorem prod_mono [SFinite ν'] (h1 : μ ≤ μ') (h2 : ν ≤ ν') : μ.prod ν ≤ μ'.prod ν' := by + apply Measure.le_iff.2 (fun s hs ↦ ?_) + calc μ.prod ν s + _ ≤ ∫⁻ x, ν (Prod.mk x ⁻¹' s) ∂μ := prod_apply_le hs + _ ≤ ∫⁻ x, ν' (Prod.mk x ⁻¹' s) ∂μ' := by gcongr + _ = (μ'.prod ν') s := (prod_apply hs).symm + /-- Note: the converse is not true. For a counterexample, see Walter Rudin *Real and Complex Analysis*, example (c) in section 8.9. It is true if the set is measurable, see `ae_prod_mem_iff_ae_ae_mem`. -/ @@ -835,7 +843,8 @@ theorem map_prod_map {δ} [MeasurableSpace δ] {f : α → β} {g : γ → δ} ( -- `prod_smul_right` needs an instance to get `SFinite (c • ν)` from `SFinite ν`, -- hence it is placed in the `WithDensity` file, where the instance is defined. -lemma prod_smul_left {μ : Measure α} (c : ℝ≥0∞) : (c • μ).prod ν = c • (μ.prod ν) := by +lemma prod_smul_left {μ : Measure α} {R : Type*} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] + (c : R) : (c • μ).prod ν = c • (μ.prod ν) := by ext s hs rw [prod_apply hs, Measure.smul_apply, prod_apply hs] simp diff --git a/Mathlib/MeasureTheory/Measure/WithDensity.lean b/Mathlib/MeasureTheory/Measure/WithDensity.lean index 404bcf0aa490ea..243df99a8a2eec 100644 --- a/Mathlib/MeasureTheory/Measure/WithDensity.lean +++ b/Mathlib/MeasureTheory/Measure/WithDensity.lean @@ -660,8 +660,10 @@ instance Measure.withDensity.instSFinite [SFinite μ] {f : α → ℝ≥0∞} : rw [key] infer_instance -instance [SFinite μ] (c : ℝ≥0∞) : SFinite (c • μ) := by - rw [← withDensity_const] +instance [SFinite μ] {R : Type*} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] (c : R) : + SFinite (c • μ) := by + have : c • μ = c • ((1 : ℝ≥0∞) • μ) := by simp + rw [this, ← smul_assoc, ← withDensity_const] infer_instance /-- If `μ ≪ ν` and `ν` is s-finite, then `μ` is s-finite. -/ @@ -724,10 +726,12 @@ theorem prod_withDensity {f : α → ℝ≥0∞} {g : β → ℝ≥0∞} (hf : M -- `prod_smul_left` is in the `Prod` file. This lemma is here because this is the file in which -- we prove the instance that gives `SFinite (c • ν)`. -lemma Measure.prod_smul_right (c : ℝ≥0∞) : μ.prod (c • ν) = c • (μ.prod ν) := by +lemma Measure.prod_smul_right {R : Type*} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] (c : R) : + μ.prod (c • ν) = c • (μ.prod ν) := by ext s hs - simp_rw [Measure.prod_apply hs, Measure.smul_apply, Measure.prod_apply hs, smul_eq_mul] - rw [lintegral_const_mul] + have A (s : Set β) : c • ν s = (c • 1) * ν s := by simp + simp_rw [Measure.prod_apply hs, Measure.smul_apply, Measure.prod_apply hs, A] + rw [lintegral_const_mul, smul_one_mul] exact measurable_measure_prodMk_left hs end Prod diff --git a/Mathlib/MeasureTheory/VectorMeasure/AddContent.lean b/Mathlib/MeasureTheory/VectorMeasure/AddContent.lean index 8394925e8a56f3..2941ff56b6cc06 100644 --- a/Mathlib/MeasureTheory/VectorMeasure/AddContent.lean +++ b/Mathlib/MeasureTheory/VectorMeasure/AddContent.lean @@ -5,10 +5,12 @@ Authors: Sébastien Gouëzel -/ module +public import Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner public import Mathlib.Analysis.Normed.Group.InfiniteSum public import Mathlib.MeasureTheory.Measure.AddContent public import Mathlib.MeasureTheory.Measure.MeasuredSets -public import Mathlib.MeasureTheory.VectorMeasure.Basic +public import Mathlib.MeasureTheory.Measure.Trim +public import Mathlib.MeasureTheory.VectorMeasure.SetIntegral /-! # Constructing a vector measure from an additive content @@ -16,7 +18,7 @@ public import Mathlib.MeasureTheory.VectorMeasure.Basic Consider a content defined on a semiring of sets. We investigate in this file whether it is possible to extend it to a (countably additive) vector measure on the whole sigma-algebra. We show that this is possible when the content is dominated by a finite -measure, see `exists_extension_of_isSetSemiring_of_le_measure_of_generateFrom`. +measure, see `exists_extension_of_isSetSemiring_of_le_measure`. -/ @[expose] public section @@ -291,10 +293,6 @@ private lemma exists_extension_of_isSetSemiring_of_le_measure_of_generateFrom_of /-- Consider an additive content `m ` on a semi-ring of sets `C`, which is dominated by a finite measure `μ`. Assume that `C` generates the sigma-algebra. Then `m` extends to a countably additive vector measure which is dominated by `μ`. -/ -/- TODO: weaken the assumption that `C` generates the sigma-algebra to measurability of all -elements of `C`, once integrals wrt vector measures is available (by composing the integral wrt `m'` -on the generated sigma-algebra, with conditional expectation of the indicator function to project -on the generated sigma-algebra). -/ theorem exists_extension_of_isSetSemiring_of_le_measure_of_generateFrom [IsFiniteMeasure μ] {C : Set (Set α)} {m : AddContent E C} (hC : IsSetSemiring C) (hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s) (h'C : hα = generateFrom C) : @@ -315,4 +313,83 @@ theorem exists_extension_of_isSetSemiring_of_le_measure_of_generateFrom exact ae_le_set_inter Filter.EventuallyLE.rfl (hD s hs) exact ⟨m', h, fun s ↦ (h' s).trans (Measure.restrict_apply_le (⋃₀ D) s)⟩ +/-- Consider an additive content `m ` on a semi-ring of measurable sets `C`, which is dominated +by a finite measure `μ`. +Then `m` extends to a countably additive vector measure which is dominated by `μ`. -/ +theorem exists_extension_of_isSetSemiring_of_le_measure [NormedSpace ℝ E] + [IsFiniteMeasure μ] {C : Set (Set α)} {m : AddContent E C} (hC : IsSetSemiring C) + (hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s) (h'C : ∀ s ∈ C, MeasurableSet s) : + ∃ m' : VectorMeasure α E, (∀ s ∈ C, m' s = m s) ∧ ∀ s, ‖m' s‖ₑ ≤ μ s := by + /- On the sigma-algebra `M` generated by `C`, the desired vector measure is provided by + `exists_extension_of_isSetSemiring_of_le_measure_of_generateFrom`. We extend it to the whole + sigma-algebra of measurable sets by integrating the conditional expectation with respect to `M`. + This extension satisfies all the desired properties. -/ + classical + let M : MeasurableSpace α := generateFrom C + have Mle : M ≤ hα := generateFrom_le h'C + set μ' := μ.trim Mle with hμ' + obtain ⟨m', m'C, hm'⟩ : + ∃ m' : @VectorMeasure α M E _ _, (∀ s ∈ C, m' s = m s) ∧ ∀ s, ‖m' s‖ₑ ≤ μ' s := by + apply exists_extension_of_isSetSemiring_of_le_measure_of_generateFrom hC (fun s hs ↦ ?_) rfl + apply (hm s hs).trans_eq + exact (MeasureTheory.trim_measurableSet_eq Mle (measurableSet_generateFrom hs)).symm + have m'_le : m'.variation ≤ μ' := by + exact variation_le_of_forall_enorm_le (fun s hs ↦ hm' _) + -- next line is to make sure that the default instance is picked below when defininig `m''`. + let : MeasurableSpace α := hα + let m'' : VectorMeasure α E := + { measureOf' s := if MeasurableSet s then ∫ᵛ x, μ[s.indicator 1 | M] x ∂• m' else 0 + empty' := by simp + not_measurable' s hs := by simp [hs] + m_iUnion' f f_meas hf := by + have : ∫ᵛ (x : α), μ[fun x ↦ ∑' (d : ℕ), (f d).indicator 1 x | M] x ∂•m' + = ∫ᵛ (x : α), ∑' d, μ[(f d).indicator 1 | M] x ∂•m' := by + apply VectorMeasure.integral_congr_ae + apply ae_mono m'_le + apply ae_eq_trim_of_measurable _ (by fun_prop) (by fun_prop) + apply condExp_tsum (fun i ↦ ?_) + · simp only [enorm_indicator_eq_indicator_enorm, Pi.one_apply, enorm_one, f_meas, + lintegral_indicator, lintegral_const, MeasurableSet.univ, Measure.restrict_apply, + Set.univ_inter, one_mul, ne_eq, ← measure_iUnion hf f_meas, measure_ne_top, + not_false_eq_true] + · exact AEStronglyMeasurable.indicator (by fun_prop) (f_meas i) + simp only [f_meas, ↓reduceIte, implies_true, MeasurableSet.iUnion, + indicator_iUnion_of_pairwise_disjoint _ hf, this] + have I : ∑' (i : ℕ), ∫⁻ (a : α), ‖μ[(f i).indicator (1 : α → ℝ) | M] a‖ₑ ∂μ < ∞ := by + have A i : ∫⁻ a, ‖μ[(f i).indicator (1 : α → ℝ) | M] a‖ₑ ∂μ = μ (f i) := + lintegral_enorm_condExp_indicator Mle (f_meas i) + simp_rw [A, ← measure_iUnion hf f_meas] + exact measure_lt_top _ _ + rw [integral_tsum (by fun_prop)]; swap + · apply ne_of_lt + grw [m'_le, hμ'] + have A i : Measurable[M] (fun x ↦ ‖μ[(f i).indicator (1 : α → ℝ) | M] x‖ₑ) := by fun_prop + simp_rw [lintegral_trim Mle (A _)] + exact I + refine Summable.hasSum (Summable.of_enorm ?_) + apply ne_of_lt (lt_of_le_of_lt ?_ I) + gcongr with i + grw [enorm_integral_le_lintegral_enorm, ContinuousLinearMap.opENorm_lsmul_le, one_mul, + lintegral_mono' m'_le le_rfl, hμ', lintegral_trim _ (by fun_prop)] } + refine ⟨m'', fun s hs ↦ ?_, fun s ↦ ?_⟩ + · simp only [h'C s hs, ↓reduceIte, m''] + have : ∫ᵛ (x : α), μ[s.indicator 1 | M] x ∂•m' = ∫ᵛ (x : α), s.indicator 1 x ∂•m' := by + apply integral_congr_ae + filter_upwards with x + rw [condExp_of_stronglyMeasurable Mle] + · exact StronglyMeasurable.indicator stronglyMeasurable_const + (measurableSet_generateFrom hs) + · exact (integrable_const 1).indicator (h'C s hs) + rw [this, integral_indicator (measurableSet_generateFrom hs)] + have : IsFiniteMeasure m'.variation := + isFiniteMeasure_of_le _ m'_le + simp only [Pi.one_apply, setIntegral_const] + simp [m'C s hs] + · by_cases hs : MeasurableSet s; swap + · simp [not_measurable _ hs] + simp only [hs, ↓reduceIte, m''] + grw [enorm_integral_le_lintegral_enorm, ContinuousLinearMap.opENorm_lsmul_le, one_mul, + lintegral_mono' m'_le le_rfl, hμ', lintegral_trim _ (by fun_prop), + lintegral_enorm_condExp_indicator Mle hs] + end MeasureTheory.VectorMeasure diff --git a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean b/Mathlib/MeasureTheory/VectorMeasure/Basic.lean index 89109bd96cf520..b4eeca1293d77c 100644 --- a/Mathlib/MeasureTheory/VectorMeasure/Basic.lean +++ b/Mathlib/MeasureTheory/VectorMeasure/Basic.lean @@ -135,12 +135,30 @@ theorem hasSum_of_disjoint_iUnion (hm : ∀ i, MeasurableSet (f i)) (hd : Pairwi · simp [Function.apply_extend MeasurableSet, Function.comp_def, hm] · exact hd.disjoint_extend_bot (he.factorsThrough _) +theorem of_if {ι : Type*} {x : ι} {B : Set ι} {A : Set α} [Decidable (x ∈ B)] : + v (if x ∈ B then A else ∅) = indicator B (fun _ => v A) x := by + split_ifs with h <;> simp [h] + variable [T2Space M] theorem of_disjoint_iUnion (hm : ∀ i, MeasurableSet (f i)) (hd : Pairwise (Disjoint on f)) : v (⋃ i, f i) = ∑' i, v (f i) := (hasSum_of_disjoint_iUnion hm hd).tsum_eq.symm +theorem of_biUnion {ι : Type*} {s : Set ι} {f : ι → Set α} (hs : s.Countable) + (hd : s.Pairwise (Disjoint on f)) (h : ∀ b ∈ s, MeasurableSet (f b)) : + v (⋃ b ∈ s, f b) = ∑' p : s, v (f p) := by + haveI := hs.toEncodable + rw [biUnion_eq_iUnion] + apply of_disjoint_iUnion + · exact fun x ↦ h x x.2 + · exact hd.on_injective Subtype.coe_injective fun x => x.2 + +theorem of_biUnion_finset {ι : Type*} {s : Finset ι} {f : ι → Set α} (hd : PairwiseDisjoint (↑s) f) + (hm : ∀ b ∈ s, MeasurableSet (f b)) : v (⋃ b ∈ s, f b) = ∑ p ∈ s, v (f p) := by + rw [← Finset.sum_attach, Finset.attach_eq_univ, ← tsum_fintype (L := .unconditional s)] + exact of_biUnion s.countable_toSet hd hm + theorem of_union {A B : Set α} (h : Disjoint A B) (hA : MeasurableSet A) (hB : MeasurableSet B) : v (A ∪ B) = v A + v B := by rw [Set.union_eq_iUnion, of_disjoint_iUnion, tsum_fintype, Fintype.sum_bool, cond, cond] @@ -208,22 +226,6 @@ theorem of_nonpos_disjoint_union_eq_zero {s : SignedMeasure α} {A B : Set α} ( rw [of_union h hA₁ hB₁] at hAB linarith -lemma of_biUnion_finset {ι : Type*} {s : Finset ι} {f : ι → Set α} (hd : PairwiseDisjoint (↑s) f) - (hm : ∀ b ∈ s, MeasurableSet (f b)) : v (⋃ b ∈ s, f b) = ∑ p ∈ s, v (f p) := by - classical - induction s using Finset.induction with - | empty => simp - | insert a s has ih => - simp only [Finset.mem_insert, iUnion_iUnion_eq_or_left, has, not_false_eq_true, - Finset.sum_insert] - rw [of_union, ih] - · exact hd.subset (by simp) - · grind - · simp only [disjoint_iUnion_right] - exact fun i hi ↦ hd (by simp) (by simp [hi]) (by grind) - · apply hm _ (by simp) - · apply Finset.measurableSet_biUnion _ (by grind) - theorem tendsto_vectorMeasure_iUnion_atTop_nat {s : ℕ → Set α} (hm : Monotone s) (hs : ∀ i, MeasurableSet (s i)) : Tendsto (fun n ↦ v (s n)) atTop (𝓝 (v (⋃ n, s n))) := by @@ -252,6 +254,23 @@ theorem tendsto_vectorMeasure_iInter_atTop_nat exact tendsto_vectorMeasure_iUnion_atTop_nat (fun i j hij ↦ by simpa using hm hij) (fun i ↦ (hs i).compl) +/-- If two vector measures give the same mass to the whole space and coincide on a +generating π-system, then they coincide. -/ +theorem ext_of_generateFrom + {M : Type*} [AddCommGroup M] [TopologicalSpace M] [T2Space M] [ContinuousSub M] + {X : Type*} {mX : MeasurableSpace X} {μ ν : VectorMeasure X M} + (C : Set (Set X)) (hμν : ∀ s ∈ C, μ s = ν s) + (hA : mX = MeasurableSpace.generateFrom C) (hC : IsPiSystem C) + (h_univ : μ Set.univ = ν Set.univ) : μ = ν := by + ext s hs + induction s, hs using MeasurableSpace.induction_on_inter hA hC with + | empty => simp + | basic t ht => exact hμν t ht + | compl t htm iht => + simp [of_compl, iht, htm, h_univ] + | iUnion f hfd hfm ihf => + simp [of_disjoint_iUnion, hfm, hfd, ihf] + end section SMul diff --git a/Mathlib/MeasureTheory/VectorMeasure/Integral.lean b/Mathlib/MeasureTheory/VectorMeasure/Integral.lean index 227c9783e8f9a8..bca065e9f14d07 100644 --- a/Mathlib/MeasureTheory/VectorMeasure/Integral.lean +++ b/Mathlib/MeasureTheory/VectorMeasure/Integral.lean @@ -58,7 +58,7 @@ We often consider integrable functions with respect to the total variation of `μ.transpose B` = `μ.mapRange B.flip.toAddMonoidHom B.flip.continuous`, which is the reference measure for the pairing integral. -When `f` is not integrable with respect to `(μ.transpose B).variation`, the value of +When `f` is not integrable with respect to `μ.variation`, the value of `μ.integral B f` is set to `0`. This is an analogous convention to the Bochner integral. However, there are cases where a natural definition of the integral as an unconditional sum exists, but `f` is not integrable in this sense: Let `μ` be the `L∞(ℕ)`-valued measure on `ℕ` defined by extending @@ -73,10 +73,11 @@ public section open Set MeasureTheory VectorMeasure ContinuousLinearMap Filter Topology open scoped ENNReal NNReal -variable {ι X Y E F G : Type*} {mX : MeasurableSpace X} [MeasurableSpace Y] +variable {ι X Y E F G H : Type*} {mX : MeasurableSpace X} [MeasurableSpace Y] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] + [NormedAddCommGroup H] [NormedSpace ℝ H] namespace MeasureTheory @@ -112,17 +113,25 @@ theorem cbmApplyMeasure_union (μ : VectorMeasure X F) (B : E →L[ℝ] F →L[ ext x simp [of_union hdisj hs ht] -theorem dominatedFinMeasAdditive_cbmApplyMeasure (μ : VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) : - DominatedFinMeasAdditive (μ.transpose B).variation (μ.transpose B) 1 := by - refine ⟨fun s t hs ht _ _ hdisj ↦ cbmApplyMeasure_union μ B hs ht hdisj, fun s hs hsf ↦ ?_⟩ - simpa using! norm_measure_le_variation hsf.ne - theorem norm_cbmApplyMeasure_le (μ : VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) (s : Set X) : ‖cbmApplyMeasure μ B s‖ ≤ ‖B‖ * ‖μ s‖ := by rw [opNorm_le_iff (by positivity)] intro x grw [cbmApplyMeasure_apply, le_opNorm₂, mul_right_comm] +theorem dominatedFinMeasAdditive_cbmApplyMeasure (μ : VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) : + DominatedFinMeasAdditive μ.variation (μ.transpose B) ‖B‖ := by + refine ⟨fun s t hs ht _ _ hdisj ↦ cbmApplyMeasure_union μ B hs ht hdisj, fun s hs hsf ↦ ?_⟩ + apply (norm_cbmApplyMeasure_le _ _ _).trans + gcongr + exact norm_measure_le_variation hsf.ne + +theorem dominatedFinMeasAdditive_transpose_cbmApplyMeasure + (μ : VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) : + DominatedFinMeasAdditive (μ.transpose B).variation (μ.transpose B) 1 := by + refine ⟨fun s t hs ht _ _ hdisj ↦ cbmApplyMeasure_union μ B hs ht hdisj, fun s hs hsf ↦ ?_⟩ + simpa using! norm_measure_le_variation hsf.ne + end cbmApplyMeasure namespace VectorMeasure @@ -221,15 +230,15 @@ function with respect to a signed measure. -/ /-- `f : X → E` is said to be integrable with respect to `μ` and `B` if it is integrable with respect to `(μ.transpose B).variation`. -/ -protected abbrev Integrable (μ : VectorMeasure X F) (f : X → E) (B : E →L[ℝ] F →L[ℝ] G) : Prop := - MeasureTheory.Integrable f (μ.transpose B).variation +protected abbrev Integrable (μ : VectorMeasure X F) (f : X → E) : Prop := + MeasureTheory.Integrable f μ.variation /-- `f : X → E` is said to be integrable with respect to `μ` and `B` on `s` if it is integrable with respect to the vector measure `μ.restrict s`. When `s` is measurable, this is equivalent to integrability with respect to `(μ.transpose B).variation.restrict s`. -/ protected abbrev IntegrableOn - (μ : VectorMeasure X F) (f : X → E) (B : E →L[ℝ] F →L[ℝ] G) (s : Set X) : Prop := - (μ.restrict s).Integrable f B + (μ : VectorMeasure X F) (f : X → E) (s : Set X) : Prop := + (μ.restrict s).Integrable f open Classical in /-- The `G`-valued integral of `E`-valued function and the `F`-valued vector measure `μ` with linear @@ -242,7 +251,7 @@ When `μ` is a signed measure, to get the integral in `G` of a `G`-valued functi `B = (ContinousLinearMap.lsmul ℝ ℝ).flip`. Notation `∫ᵛ x, f x ∂<•μ`. -/ noncomputable def integral (μ : VectorMeasure X F) (f : X → E) (B : E →L[ℝ] F →L[ℝ] G) : G := - setToFun (μ.transpose B).variation (μ.transpose B) + setToFun μ.variation (μ.transpose B) (dominatedFinMeasAdditive_cbmApplyMeasure μ B) f @[inherit_doc integral] @@ -274,9 +283,14 @@ notation3 "∫ᵛ "(...)" in "s", "r:60:(scoped f => f)" ∂<•"μ:70 => variable {μ ν B} -lemma integral_eq_setToFun : ∫ᵛ x, f x ∂[B; μ] = setToFun (μ.transpose B).variation (μ.transpose B) +lemma integral_eq_setToFun : ∫ᵛ x, f x ∂[B; μ] = setToFun μ.variation (μ.transpose B) (dominatedFinMeasAdditive_cbmApplyMeasure μ B) f := by rfl +lemma integral_eq_setToFun_transpose (hf : μ.Integrable f) : + ∫ᵛ x, f x ∂[B; μ] = setToFun (μ.transpose B).variation (μ.transpose B) + (dominatedFinMeasAdditive_transpose_cbmApplyMeasure μ B) f := + setToFun_congr_measure_of_integrable _ (by simp) (variation_transpose_le _ _) _ _ _ hf + theorem integral_of_not_completeSpace (hG : ¬CompleteSpace G) : ∫ᵛ x, f x ∂[B; μ] = 0 := by simp [integral, setToFun, hG] @@ -343,7 +357,7 @@ theorem transpose_sub_cbm (μ : VectorMeasure X F) (B C : E →L[ℝ] F →L[ℝ section Function -theorem integral_undef (h : ¬ μ.Integrable f B) : +theorem integral_undef (h : ¬ μ.Integrable f) : ∫ᵛ x, f x ∂[B; μ] = 0 := by simp [integral, setToFun_undef _ h] @@ -351,48 +365,54 @@ theorem integral_undef (h : ¬ μ.Integrable f B) : theorem integral_zero : ∫ᵛ _, 0 ∂[B; μ] = 0 := setToFun_zero _ -theorem integral_congr_ae (h : f =ᵐ[(μ.transpose B).variation] g) : +theorem integral_congr_ae (h : f =ᵐ[μ.variation] g) : ∫ᵛ x, f x ∂[B; μ] = ∫ᵛ x, g x ∂[B; μ] := setToFun_congr_ae _ h -theorem integral_eq_zero_of_ae (hf : f =ᵐ[(μ.transpose B).variation] 0) : +theorem integral_eq_zero_of_ae (hf : f =ᵐ[μ.variation] 0) : ∫ᵛ x, f x ∂[B; μ] = 0 := by simp [integral_congr_ae hf] -@[to_fun] lemma Integrable.add (hf : μ.Integrable f B) (hg : μ.Integrable g B) : - μ.Integrable (f + g) B := +omit [NormedSpace ℝ E] [NormedSpace ℝ F] in +@[to_fun] lemma Integrable.add (hf : μ.Integrable f) (hg : μ.Integrable g) : + μ.Integrable (f + g) := MeasureTheory.Integrable.add hf hg -@[to_fun] lemma Integrable.neg (hf : μ.Integrable f B) : - μ.Integrable (-f) B := +omit [NormedSpace ℝ E] [NormedSpace ℝ F] in +@[to_fun] lemma Integrable.neg (hf : μ.Integrable f) : + μ.Integrable (-f) := MeasureTheory.Integrable.neg hf -@[to_fun] lemma Integrable.sub (hf : μ.Integrable f B) (hg : μ.Integrable g B) : - μ.Integrable (f - g) B := +omit [NormedSpace ℝ E] [NormedSpace ℝ F] in +@[to_fun] lemma Integrable.sub (hf : μ.Integrable f) (hg : μ.Integrable g) : + μ.Integrable (f - g) := MeasureTheory.Integrable.sub hf hg +omit [NormedSpace ℝ E] [NormedSpace ℝ F] in @[to_fun] lemma Integrable.smul {𝕜 : Type*} [NormedAddCommGroup 𝕜] [SMulZeroClass 𝕜 E] - [IsBoundedSMul 𝕜 E] (c : 𝕜) (hf : μ.Integrable f B) : - μ.Integrable (c • f) B := + [IsBoundedSMul 𝕜 E] (c : 𝕜) (hf : μ.Integrable f) : + μ.Integrable (c • f) := MeasureTheory.Integrable.smul c hf +omit [NormedSpace ℝ E] [NormedSpace ℝ F] in theorem Integrable.finsetSum {ι : Type*} (s : Finset ι) {f : ι → X → E} - (hf : ∀ i ∈ s, μ.Integrable (f i) B) : μ.Integrable (∑ i ∈ s, f i) B := + (hf : ∀ i ∈ s, μ.Integrable (f i)) : μ.Integrable (∑ i ∈ s, f i) := integrable_finsetSum' s hf +omit [NormedSpace ℝ E] [NormedSpace ℝ F] in theorem Integrable.fun_finsetSum {ι : Type*} (s : Finset ι) {f : ι → X → E} - (hf : ∀ i ∈ s, μ.Integrable (f i) B) : μ.Integrable (fun x ↦ ∑ i ∈ s, f i x) B := + (hf : ∀ i ∈ s, μ.Integrable (f i)) : μ.Integrable (fun x ↦ ∑ i ∈ s, f i x) := integrable_finsetSum s hf -theorem integral_fun_add (hf : μ.Integrable f B) (hg : μ.Integrable g B) : +theorem integral_fun_add (hf : μ.Integrable f) (hg : μ.Integrable g) : ∫ᵛ x, f x + g x ∂[B; μ] = ∫ᵛ x, f x ∂[B; μ] + ∫ᵛ x, g x ∂[B; μ] := setToFun_add _ hf hg -theorem integral_add (hf : μ.Integrable f B) (hg : μ.Integrable g B) : +theorem integral_add (hf : μ.Integrable f) (hg : μ.Integrable g) : ∫ᵛ x, (f + g) x ∂[B; μ] = ∫ᵛ x, f x ∂[B; μ] + ∫ᵛ x, g x ∂[B; μ] := integral_fun_add hf hg theorem integral_finsetSum (s : Finset ι) {f : ι → X → E} - (hf : ∀ i ∈ s, μ.Integrable (f i) B) : + (hf : ∀ i ∈ s, μ.Integrable (f i)) : ∫ᵛ x, ∑ i ∈ s, f i x ∂[B; μ] = ∑ i ∈ s, ∫ᵛ x, f i x ∂[B; μ] := setToFun_finsetSum _ s hf @@ -407,11 +427,11 @@ variable (f μ B) in theorem integral_neg : ∫ᵛ x, (-f) x ∂[B; μ] = -∫ᵛ x, f x ∂[B; μ] := integral_fun_neg μ B f -theorem integral_fun_sub (hf : μ.Integrable f B) (hg : μ.Integrable g B) : +theorem integral_fun_sub (hf : μ.Integrable f) (hg : μ.Integrable g) : ∫ᵛ x, f x - g x ∂[B; μ] = ∫ᵛ x, f x ∂[B; μ] - ∫ᵛ x, g x ∂[B; μ] := setToFun_sub _ hf hg -theorem integral_sub (hf : μ.Integrable f B) (hg : μ.Integrable g B) : +theorem integral_sub (hf : μ.Integrable f) (hg : μ.Integrable g) : ∫ᵛ x, (f - g) x ∂[B; μ] = ∫ᵛ x, f x ∂[B; μ] - ∫ᵛ x, g x ∂[B; μ] := integral_fun_sub hf hg variable (f μ B) in @@ -426,7 +446,7 @@ theorem integral_smul (c : ℝ) : ∫ᵛ x, (c • f) x ∂[B; μ] = c • ∫ᵛ x, f x ∂[B; μ] := integral_fun_smul μ B c f @[simp] -theorem integral_const [CompleteSpace G] [IsFiniteMeasure (μ.transpose B).variation] (c : E) : +theorem integral_const [CompleteSpace G] [IsFiniteMeasure μ.variation] (c : E) : ∫ᵛ _ : X, c ∂[B; μ] = B c (μ univ) := setToFun_const _ _ @@ -434,34 +454,40 @@ end Function section VectorMeasure +omit [NormedSpace ℝ E] [NormedSpace ℝ F] in /- `simpNF` complains that this lemma can be proved by `simp`, because the `simp`-generated lemma unfolds the abbrev `VectorMeasure.Integrable`. TODO: fix `simp`. See lean4#13958. -/ @[nolint simpNF, simp] -lemma Integrable.zero_vectorMeasure : (0 : VectorMeasure X F).Integrable f B := by +lemma Integrable.zero_vectorMeasure : (0 : VectorMeasure X F).Integrable f := by simp [VectorMeasure.Integrable] -lemma Integrable.add_vectorMeasure (hμ : μ.Integrable f B) (hν : ν.Integrable f B) : - (μ + ν).Integrable f B := by +omit [NormedSpace ℝ E] [NormedSpace ℝ F] in +lemma Integrable.add_vectorMeasure (hμ : μ.Integrable f) (hν : ν.Integrable f) : + (μ + ν).Integrable f := by apply Integrable.mono_measure (integrable_add_measure.2 ⟨hμ, hν⟩) - grw [transpose_add, variation_add_le] + grw [variation_add_le] -lemma Integrable.neg_vectorMeasure (hμ : μ.Integrable f B) : - (-μ).Integrable f B := +omit [NormedSpace ℝ E] [NormedSpace ℝ F] in +lemma Integrable.neg_vectorMeasure (hμ : μ.Integrable f) : + (-μ).Integrable f := Integrable.mono_measure hμ (by simp) -lemma Integrable.sub_vectorMeasure (hμ : μ.Integrable f B) (hν : ν.Integrable f B) : - (μ - ν).Integrable f B := by +omit [NormedSpace ℝ E] [NormedSpace ℝ F] in +lemma Integrable.sub_vectorMeasure (hμ : μ.Integrable f) (hν : ν.Integrable f) : + (μ - ν).Integrable f := by convert hμ.add_vectorMeasure hν.neg_vectorMeasure using 1 exact sub_eq_add_neg μ ν -lemma Integrable.smul_vectorMeasure (hμ : μ.Integrable f B) (c : ℝ) : - (c • μ).Integrable f B := by +omit [NormedSpace ℝ E] in +lemma Integrable.smul_vectorMeasure (hμ : μ.Integrable f) (c : ℝ) : + (c • μ).Integrable f := by apply Integrable.mono_measure (Integrable.smul_measure_nnreal hμ (c := ‖c‖₊)) - simp [transpose_smul, variation_smul] + simp [variation_smul] +omit [NormedSpace ℝ E] [NormedSpace ℝ F] in lemma Integrable.finsetSum_vectorMeasure {ι : Type*} {μ : ι → VectorMeasure X F} {s : Finset ι} - (h : ∀ i ∈ s, (μ i).Integrable f B) : - (∑ i ∈ s, μ i).Integrable f B := by + (h : ∀ i ∈ s, (μ i).Integrable f) : + (∑ i ∈ s, μ i).Integrable f := by classical induction s using Finset.induction_on with | empty => simp @@ -470,8 +496,9 @@ lemma Integrable.finsetSum_vectorMeasure {ι : Type*} {μ : ι → VectorMeasure Finset.sum_insert] at h ⊢ exact h.1.add_vectorMeasure (ih h.2) -lemma Integrable.restrict (hf : μ.Integrable f B) {s : Set X} : - (μ.restrict s).Integrable f B := by +omit [NormedSpace ℝ E] [NormedSpace ℝ F] in +lemma Integrable.restrict (hf : μ.Integrable f) {s : Set X} : + (μ.restrict s).Integrable f := by by_cases hs : MeasurableSet s · simpa [VectorMeasure.Integrable, transpose_restrict, variation_restrict hs] using MeasureTheory.Integrable.restrict hf @@ -489,12 +516,12 @@ theorem integral_smul_vectorMeasure (f : X → E) (c : ℝ) : by_cases hG : CompleteSpace G; swap · simp [integral, setToFun, hG] simp_rw [integral, ← setToFun_smul_left] - have : ((c • μ).transpose B).variation = ‖c‖₊ • (μ.transpose B).variation := by - simp [transpose, mapRange_smul, variation_smul] - simp only [this, mul_one] - have : DominatedFinMeasAdditive (μ.transpose B).variation ((c • μ).transpose B) ‖c‖ := by - simp only [transpose_smul, coe_smul, Real.norm_eq_abs] - simpa using! (dominatedFinMeasAdditive_cbmApplyMeasure μ B).smul c + have : (c • μ).variation = ‖c‖₊ • μ.variation := by + simp [variation_smul] + simp only [this] + have : DominatedFinMeasAdditive μ.variation ((c • μ).transpose B) (‖c‖ * ‖B‖) := by + simp only [transpose_smul, coe_smul] + exact (dominatedFinMeasAdditive_cbmApplyMeasure μ B).smul c rw! [← setToFun_congr_smul_measure' _ this, transpose_smul] rfl @@ -503,13 +530,13 @@ theorem integral_smul_nnreal_vectorMeasure (f : X → E) (c : ℝ≥0) : ∫ᵛ x, f x ∂[B; c • μ] = c • ∫ᵛ x, f x ∂[B; μ] := integral_smul_vectorMeasure f (c : ℝ) -theorem integral_add_vectorMeasure (hμ : μ.Integrable f B) (hν : ν.Integrable f B) : +theorem integral_add_vectorMeasure (hμ : μ.Integrable f) (hν : ν.Integrable f) : ∫ᵛ x, f x ∂[B; μ + ν] = ∫ᵛ x, f x ∂[B; μ] + ∫ᵛ x, f x ∂[B; ν] := - setToFun_add_left'' (by simp [transpose]) hμ hν (by grw [transpose_add, variation_add_le]) - zero_le_one zero_le_one zero_le_one + setToFun_add_left'' (by simp [transpose]) hμ hν (by grw [variation_add_le]) + (norm_nonneg _) (norm_nonneg _) (norm_nonneg _) theorem integral_finsetSum_vectorMeasure {μ : ι → VectorMeasure X F} - {s : Finset ι} (hf : ∀ i ∈ s, (μ i).Integrable f B) : + {s : Finset ι} (hf : ∀ i ∈ s, (μ i).Integrable f) : ∫ᵛ x, f x ∂[B; ∑ i ∈ s, μ i] = ∑ i ∈ s, ∫ᵛ x, f x ∂[B; μ i] := by classical induction s using Finset.induction_on with @@ -524,7 +551,7 @@ theorem integral_neg_vectorMeasure : ∫ᵛ x, f x ∂[B; -μ] = -∫ᵛ x, f x ∂[B; μ] := by simp [integral, ← setToFun_neg'] -theorem integral_sub_vectorMeasure (hμ : μ.Integrable f B) (hν : ν.Integrable f B) : +theorem integral_sub_vectorMeasure (hμ : μ.Integrable f) (hν : ν.Integrable f) : ∫ᵛ x, f x ∂[B; μ - ν] = ∫ᵛ x, f x ∂[B; μ] - ∫ᵛ x, f x ∂[B; ν] := by rw [sub_eq_add_neg, integral_add_vectorMeasure hμ hν.neg_vectorMeasure, integral_neg_vectorMeasure, ← sub_eq_add_neg] @@ -533,76 +560,46 @@ end VectorMeasure section cbm -/- `simpNF` complains that this lemma can be proved by `simp`, because the `simp`-generated lemma -unfolds the abbrev `VectorMeasure.Integrable`. TODO: fix `simp`. See lean4#13958. -/ -@[nolint simpNF, simp] -lemma Integrable.zero_cbm : μ.Integrable f (0 : E →L[ℝ] F →L[ℝ] G) := by - simp [VectorMeasure.Integrable] - -lemma Integrable.add_cbm (hB : μ.Integrable f B) (hC : μ.Integrable f C) : - μ.Integrable f (B + C) := by - apply Integrable.mono_measure (integrable_add_measure.2 ⟨hB, hC⟩) - grw [transpose_add_cbm, variation_add_le] - -lemma Integrable.neg_cbm (hB : μ.Integrable f B) : - μ.Integrable f (-B) := by - apply Integrable.mono_measure hB - simp - -lemma Integrable.sub_cbm (hB : μ.Integrable f B) (hC : μ.Integrable f C) : - μ.Integrable f (B - C) := by - convert hB.add_cbm hC.neg_cbm using 1 - exact sub_eq_add_neg B C - -lemma Integrable.finsetSum_cbm {ι : Type*} {B : ι → E →L[ℝ] F →L[ℝ] G} {s : Finset ι} - (h : ∀ i ∈ s, μ.Integrable f (B i)) : μ.Integrable f (∑ i ∈ s, B i) := by - classical - induction s using Finset.induction_on with - | empty => simp - | insert a s ha ih => - simp only [Finset.mem_insert, forall_eq_or_imp, ha, not_false_eq_true, - Finset.sum_insert] at h ⊢ - exact h.1.add_cbm (ih h.2) - variable (f μ) in @[simp] theorem integral_zero_cbm : ∫ᵛ x, f x ∂[(0 : E →L[ℝ] F →L[ℝ] G); μ] = 0 := by simp [integral] -theorem integral_add_cbm (hB : μ.Integrable f B) (hC : μ.Integrable f C) : - ∫ᵛ x, f x ∂[B + C; μ] = ∫ᵛ x, f x ∂[B; μ] + ∫ᵛ x, f x ∂[C; μ] := - setToFun_add_left'' (by simp [transpose]) hB hC (by simp [variation_add_le]) - zero_le_one zero_le_one zero_le_one +theorem integral_add_cbm (hB : μ.Integrable f) : + ∫ᵛ x, f x ∂[B + C; μ] = ∫ᵛ x, f x ∂[B; μ] + ∫ᵛ x, f x ∂[C; μ] := by + refine setToFun_add_left'' (by simp [transpose]) hB hB ?_ + (norm_nonneg _) (norm_nonneg _) (norm_nonneg _) + nth_rw 1 [← add_zero μ.variation] + gcongr + exact Measure.zero_le μ.variation theorem integral_finsetSum_cbm {B : ι → E →L[ℝ] F →L[ℝ] G} - {s : Finset ι} (hf : ∀ i ∈ s, μ.Integrable f (B i)) : + {s : Finset ι} (hf : μ.Integrable f) : ∫ᵛ x, f x ∂[∑ i ∈ s, B i; μ] = ∑ i ∈ s, ∫ᵛ x, f x ∂[B i; μ] := by classical induction s using Finset.induction_on with | empty => simp | insert a s ha ih => - simp only [Finset.mem_insert, forall_eq_or_imp, ha, not_false_eq_true, - Finset.sum_insert] at hf ⊢ - rw [integral_add_cbm hf.1 (Integrable.finsetSum_cbm hf.2), ih hf.2] + simp only [ha, not_false_eq_true, Finset.sum_insert] + rw [integral_add_cbm hf, ih] @[integral_simps] theorem integral_neg_cbm : ∫ᵛ x, f x ∂[-B; μ] = -∫ᵛ x, f x ∂[B; μ] := by simp [integral, ← setToFun_neg'] -theorem integral_sub_cbm (hB : μ.Integrable f B) (hC : μ.Integrable f C) : +theorem integral_sub_cbm (hB : μ.Integrable f) : ∫ᵛ x, f x ∂[B - C; μ] = ∫ᵛ x, f x ∂[B; μ] - ∫ᵛ x, f x ∂[C; μ] := by rw [sub_eq_add_neg, integral_add_cbm hB, integral_neg_cbm, ← sub_eq_add_neg] - simpa [VectorMeasure.Integrable] using hC end cbm -theorem Integrable.of_integral_ne_zero (h : ∫ᵛ a, f a ∂[B; μ] ≠ 0) : μ.Integrable f B := +theorem Integrable.of_integral_ne_zero (h : ∫ᵛ a, f a ∂[B; μ] ≠ 0) : μ.Integrable f := Not.imp_symm integral_undef h theorem integral_non_aestronglyMeasurable {f : X → E} - (h : ¬AEStronglyMeasurable f (μ.transpose B).variation) : + (h : ¬AEStronglyMeasurable f μ.variation) : ∫ᵛ a, f a ∂[B; μ] = 0 := integral_undef <| not_and_of_not_left _ h @@ -610,28 +607,55 @@ lemma integral_indicator₂ {β : Type*} (f : β → X → E) (s : Set β) (b : ∫ᵛ y, s.indicator (f · y) b ∂[B; μ] = s.indicator (fun x ↦ ∫ᵛ y, f x y ∂[B; μ]) b := by by_cases hb : b ∈ s <;> simp [hb] +theorem continuous_integral : Continuous fun f : X →₁[μ.variation] E => ∫ᵛ a, f a ∂[B; μ] := by + simp only [integral_eq_setToFun] + exact continuous_setToFun _ + theorem norm_integral_le_lintegral_norm : - ‖∫ᵛ a, f a ∂[B; μ]‖ ≤ ENNReal.toReal (∫⁻ a, ENNReal.ofReal ‖f a‖ ∂(μ.transpose B).variation) := + ‖∫ᵛ a, f a ∂[B; μ]‖ ≤ ‖B‖ * ENNReal.toReal (∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ.variation) := (norm_setToFun_le_toReal _ (by simp)).trans (by simp) -theorem enorm_integral_le_lintegral_enorm : - ‖∫ᵛ a, f a ∂[B; μ]‖ₑ ≤ ∫⁻ a, ‖f a‖ₑ ∂(μ.transpose B).variation := - (enorm_setToFun_le _ (by simp)).trans (by simp) +theorem norm_integral_le_integral_norm : + ‖∫ᵛ a, f a ∂[B; μ]‖ ≤ ‖B‖ * ∫ a, ‖f a‖ ∂μ.variation := by + have le_ae : ∀ᵐ a ∂μ.variation, 0 ≤ ‖f a‖ := + Eventually.of_forall fun a => norm_nonneg _ + by_cases h : AEStronglyMeasurable f μ.variation + · calc ‖∫ᵛ a, f a ∂[B; μ]‖ + _ ≤ ‖B‖ * ENNReal.toReal (∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ.variation) := + norm_integral_le_lintegral_norm + _ = ‖B‖ * ∫ a, ‖f a‖ ∂μ.variation := by + rw [integral_eq_lintegral_of_nonneg_ae le_ae <| h.norm] + · rw [integral_non_aestronglyMeasurable h, norm_zero] + positivity -theorem dist_integral_le_lintegral_edist (hf : μ.Integrable f B) (hg : μ.Integrable g B) : +theorem enorm_integral_le_lintegral_enorm : + ‖∫ᵛ a, f a ∂[B; μ]‖ₑ ≤ ‖B‖ₑ * ∫⁻ a, ‖f a‖ₑ ∂μ.variation := by + apply (enorm_setToFun_le _ (by simp)).trans + gcongr + simp [← coe_nnnorm] + +theorem enorm_integral_le_lintegral_enorm_transpose : + ‖∫ᵛ a, f a ∂[B; μ]‖ₑ ≤ ∫⁻ a, ‖f a‖ₑ ∂(μ.transpose B).variation := by + by_cases hf : μ.Integrable f + · rw [integral_eq_setToFun_transpose hf] + apply (enorm_setToFun_le _ (by simp)).trans (by simp) + · simp [integral_undef hf] + +theorem dist_integral_le_lintegral_edist (hf : μ.Integrable f) (hg : μ.Integrable g) : dist (∫ᵛ a, f a ∂[B; μ]) (∫ᵛ a, g a ∂[B; μ]) ≤ - (∫⁻ a, edist (f a) (g a) ∂(μ.transpose B).variation).toReal := by + ‖B‖ * (∫⁻ a, edist (f a) (g a) ∂μ.variation).toReal := by grw [dist_eq_norm, ← integral_sub hf hg, norm_integral_le_lintegral_norm] simp [edist_eq_enorm_sub] -theorem edist_integral_le_lintegral_edist (hf : μ.Integrable f B) (hg : μ.Integrable g B) : +theorem edist_integral_le_lintegral_edist (hf : μ.Integrable f) (hg : μ.Integrable g) : edist (∫ᵛ a, f a ∂[B; μ]) (∫ᵛ a, g a ∂[B; μ]) ≤ - ∫⁻ a, edist (f a) (g a) ∂(μ.transpose B).variation := by + ‖B‖ₑ * ∫⁻ a, edist (f a) (g a) ∂μ.variation := by rw [edist_dist] - exact ENNReal.ofReal_le_of_le_toReal (dist_integral_le_lintegral_edist hf hg) + apply ENNReal.ofReal_le_of_le_toReal + grw [dist_integral_le_lintegral_edist hf hg, ENNReal.toReal_mul, toReal_enorm] theorem frequently_ae_ne_zero_of_integral_ne_zero - (h : ∫ᵛ a, f a ∂[B; μ] ≠ 0) : ∃ᶠ a in ae (μ.transpose B).variation, f a ≠ 0 := + (h : ∫ᵛ a, f a ∂[B; μ] ≠ 0) : ∃ᶠ a in ae μ.variation, f a ≠ 0 := fun h' ↦ h (integral_eq_zero_of_ae (h'.mono fun _ ↦ not_not.mp)) theorem exists_ne_zero_of_integral_ne_zero @@ -643,7 +667,7 @@ theorem exists_ne_zero_of_integral_ne_zero rcases subsingleton_or_nontrivial G with h'G | h'G · apply Subsingleton.elim rw [integral_eq_setToFun, MeasureTheory.integral_eq_setToFun] - simp only [variation_transpose_lsmul_flip, variation_toSignedMeasure] + simp only [Measure.variation_toSignedMeasure] apply setToFun_congr_left' _ _ (fun s hs h's ↦ ?_) simp only [transpose, ContinuousLinearMap.flip_flip, mapRange_apply, Measure.toSignedMeasure_apply, hs, ↓reduceIte, LinearMap.toAddMonoidHom_coe, @@ -662,7 +686,7 @@ theorem integral_dirac' [MeasurableSpace X] [CompleteSpace G] {a : X} {v : F} calc ∫ᵛ x, f x ∂[B; VectorMeasure.dirac a v] = ∫ᵛ _, f a ∂[B; VectorMeasure.dirac a v] := by apply integral_congr_ae - simp only [transpose_dirac, variation_dirac] + simp only [variation_dirac] exact Measure.ae_smul_measure (ae_eq_dirac' hfm.measurable) _ _ = B (f a) v := by simp @@ -677,7 +701,7 @@ theorem integral_dirac [MeasurableSpace X] [MeasurableSingletonClass X] [Complet calc ∫ᵛ x, f x ∂[B; VectorMeasure.dirac a v] = ∫ᵛ _, f a ∂[B; VectorMeasure.dirac a v] := by apply integral_congr_ae - simp only [transpose_dirac, variation_dirac] + simp only [variation_dirac] exact Measure.ae_smul_measure (ae_eq_dirac f) _ _ = B (f a) v := by simp @@ -689,17 +713,17 @@ theorem integral_unique [Unique X] [CompleteSpace G] : /-- If `F i → f` in `L1`, then `∫ᵛ x, F i x ∂[B; μ] → ∫ᵛ x, f x ∂[B; μ]`. -/ theorem tendsto_integral_of_L1 {ι} (f : X → E) - (hfi : AEStronglyMeasurable f (μ.transpose B).variation) {F : ι → X → E} - {l : Filter ι} (hFi : ∀ᶠ i in l, μ.Integrable (F i) B) - (hF : Tendsto (fun i ↦ ∫⁻ x, ‖F i x - f x‖ₑ ∂(μ.transpose B).variation) l (𝓝 0)) : + (hfi : AEStronglyMeasurable f μ.variation) {F : ι → X → E} + {l : Filter ι} (hFi : ∀ᶠ i in l, μ.Integrable (F i)) + (hF : Tendsto (fun i ↦ ∫⁻ x, ‖F i x - f x‖ₑ ∂μ.variation) l (𝓝 0)) : Tendsto (fun i ↦ ∫ᵛ x, F i x ∂[B; μ]) l (𝓝 <| ∫ᵛ x, f x ∂[B; μ]) := tendsto_setToFun_of_L1 _ f hfi hFi hF /-- If `F i → f` in `L1`, then `∫ᵛ x, F i x ∂[B; μ] → ∫ᵛ x, f x ∂[B; μ]`. -/ lemma tendsto_integral_of_L1' {ι} (f : X → E) - (hfi : AEStronglyMeasurable f (μ.transpose B).variation) {F : ι → X → E} - {l : Filter ι} (hFi : ∀ᶠ i in l, μ.Integrable (F i) B) - (hF : Tendsto (fun i ↦ eLpNorm (F i - f) 1 (μ.transpose B).variation) l (𝓝 0)) : + (hfi : AEStronglyMeasurable f μ.variation) {F : ι → X → E} + {l : Filter ι} (hFi : ∀ᶠ i in l, μ.Integrable (F i)) + (hF : Tendsto (fun i ↦ eLpNorm (F i - f) 1 μ.variation) l (𝓝 0)) : Tendsto (fun i ↦ ∫ᵛ x, F i x ∂[B; μ]) l (𝓝 (∫ᵛ x, f x ∂[B; μ])) := by refine tendsto_integral_of_L1 f hfi hFi ?_ simp_rw [eLpNorm_one_eq_lintegral_enorm, Pi.sub_apply] at hF @@ -708,67 +732,72 @@ lemma tendsto_integral_of_L1' {ι} (f : X → E) variable {Y : Type*} [TopologicalSpace Y] [FirstCountableTopology Y] theorem continuousWithinAt_of_dominated {F : Y → X → E} {x₀ : Y} {bound : X → ℝ} {s : Set Y} - (hF_meas : ∀ᶠ x in 𝓝[s] x₀, AEStronglyMeasurable (F x) (μ.transpose B).variation) - (h_bound : ∀ᶠ x in 𝓝[s] x₀, ∀ᵐ a ∂(μ.transpose B).variation, ‖F x a‖ ≤ bound a) - (bound_integrable : Integrable bound (μ.transpose B).variation) - (h_cont : ∀ᵐ a ∂(μ.transpose B).variation, ContinuousWithinAt (fun x ↦ F x a) s x₀) : + (hF_meas : ∀ᶠ x in 𝓝[s] x₀, AEStronglyMeasurable (F x) μ.variation) + (h_bound : ∀ᶠ x in 𝓝[s] x₀, ∀ᵐ a ∂μ.variation, ‖F x a‖ ≤ bound a) + (bound_integrable : Integrable bound μ.variation) + (h_cont : ∀ᵐ a ∂μ.variation, ContinuousWithinAt (fun x ↦ F x a) s x₀) : ContinuousWithinAt (fun x ↦ ∫ᵛ a, F x a ∂[B; μ]) s x₀ := continuousWithinAt_setToFun_of_dominated _ hF_meas h_bound bound_integrable h_cont theorem continuousAt_of_dominated {F : Y → X → E} {x₀ : Y} {bound : X → ℝ} - (hF_meas : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.transpose B).variation) - (h_bound : ∀ᶠ x in 𝓝 x₀, ∀ᵐ a ∂(μ.transpose B).variation, ‖F x a‖ ≤ bound a) - (bound_integrable : Integrable bound (μ.transpose B).variation) - (h_cont : ∀ᵐ a ∂(μ.transpose B).variation, ContinuousAt (fun x ↦ F x a) x₀) : + (hF_meas : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (F x) μ.variation) + (h_bound : ∀ᶠ x in 𝓝 x₀, ∀ᵐ a ∂μ.variation, ‖F x a‖ ≤ bound a) + (bound_integrable : Integrable bound μ.variation) + (h_cont : ∀ᵐ a ∂μ.variation, ContinuousAt (fun x ↦ F x a) x₀) : ContinuousAt (fun x ↦ ∫ᵛ a, F x a ∂[B; μ]) x₀ := continuousAt_setToFun_of_dominated _ hF_meas h_bound bound_integrable h_cont theorem continuousOn_of_dominated {F : Y → X → E} {bound : X → ℝ} {s : Set Y} - (hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) (μ.transpose B).variation) - (h_bound : ∀ x ∈ s, ∀ᵐ a ∂(μ.transpose B).variation, ‖F x a‖ ≤ bound a) - (bound_integrable : Integrable bound (μ.transpose B).variation) - (h_cont : ∀ᵐ a ∂(μ.transpose B).variation, ContinuousOn (fun x ↦ F x a) s) : + (hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ.variation) + (h_bound : ∀ x ∈ s, ∀ᵐ a ∂μ.variation, ‖F x a‖ ≤ bound a) + (bound_integrable : Integrable bound μ.variation) + (h_cont : ∀ᵐ a ∂μ.variation, ContinuousOn (fun x ↦ F x a) s) : ContinuousOn (fun x ↦ ∫ᵛ a, F x a ∂[B; μ]) s := continuousOn_setToFun_of_dominated _ hF_meas h_bound bound_integrable h_cont theorem continuous_of_dominated {F : Y → X → E} {bound : X → ℝ} - (hF_meas : ∀ x, AEStronglyMeasurable (F x) (μ.transpose B).variation) - (h_bound : ∀ x, ∀ᵐ a ∂(μ.transpose B).variation, ‖F x a‖ ≤ bound a) - (bound_integrable : Integrable bound (μ.transpose B).variation) - (h_cont : ∀ᵐ a ∂(μ.transpose B).variation, Continuous fun x ↦ F x a) : + (hF_meas : ∀ x, AEStronglyMeasurable (F x) μ.variation) + (h_bound : ∀ x, ∀ᵐ a ∂μ.variation, ‖F x a‖ ≤ bound a) + (bound_integrable : Integrable bound μ.variation) + (h_cont : ∀ᵐ a ∂μ.variation, Continuous fun x ↦ F x a) : Continuous fun x ↦ ∫ᵛ a, F x a ∂[B; μ] := continuous_setToFun_of_dominated _ hF_meas h_bound bound_integrable h_cont -theorem norm_integral_le_of_norm_le_const [IsFiniteMeasure (μ.transpose B).variation] - {C : ℝ} (h : ∀ᵐ x ∂(μ.transpose B).variation, ‖f x‖ ≤ C) : - ‖∫ᵛ x, f x ∂[B; μ]‖ ≤ C * (μ.transpose B).variation.real univ := calc +theorem norm_integral_le_of_norm_le_const [IsFiniteMeasure μ.variation] + {C : ℝ} (h : ∀ᵐ x ∂μ.variation, ‖f x‖ ≤ C) : + ‖∫ᵛ x, f x ∂[B; μ]‖ ≤ C * ‖B‖ * μ.variation.real univ := calc ‖∫ᵛ x, f x ∂[B; μ]‖ - _ ≤ (∫⁻ a, ENNReal.ofReal ‖f a‖ ∂(μ.transpose B).variation).toReal := + _ ≤ ‖B‖ * (∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ.variation).toReal := norm_integral_le_lintegral_norm - _ ≤ (∫⁻ a, ENNReal.ofReal C ∂(μ.transpose B).variation).toReal := by + _ ≤ ‖B‖ * (∫⁻ a, ENNReal.ofReal C ∂μ.variation).toReal := by + gcongr 1 apply ENNReal.toReal_mono · simp only [lintegral_const, ne_eq] finiteness · apply lintegral_mono_ae filter_upwards [h] with x hx using ENNReal.ofReal_mono hx - _ = C * (μ.transpose B).variation.real univ := by - by_cases hμ : (μ.transpose B).variation = 0 + _ = ‖B‖ * (C * μ.variation.real univ) := by + by_cases hμ : μ.variation = 0 · simp [hμ] - have : (ae (μ.transpose B).variation).NeBot := ae_neBot.mpr hμ + have : (ae μ.variation).NeBot := ae_neBot.mpr hμ have hC : 0 ≤ C := by obtain ⟨x, hx⟩ := h.exists exact (norm_nonneg _).trans hx simp [ENNReal.toReal_ofReal hC, Measure.real] + _ = C * ‖B‖ * μ.variation.real univ := by ring theorem enorm_integral_le_of_enorm_le_const - {C : ℝ≥0∞} (h : ∀ᵐ x ∂(μ.transpose B).variation, ‖f x‖ₑ ≤ C) : - ‖∫ᵛ x, f x ∂[B; μ]‖ₑ ≤ C * (μ.transpose B).variation univ := - enorm_integral_le_lintegral_enorm.trans ((lintegral_mono_ae h).trans (by simp)) + {C : ℝ≥0∞} (h : ∀ᵐ x ∂μ.variation, ‖f x‖ₑ ≤ C) : + ‖∫ᵛ x, f x ∂[B; μ]‖ₑ ≤ C * ‖B‖ₑ * μ.variation univ := by + apply enorm_integral_le_lintegral_enorm.trans + rw [mul_comm C, mul_assoc] + gcongr + exact (lintegral_mono_ae h).trans (by simp) theorem nndist_integral_add_vectorMeasure_le_lintegral - (h₁ : μ.Integrable f B) (h₂ : ν.Integrable f B) : + (h₁ : μ.Integrable f) (h₂ : ν.Integrable f) : (nndist (∫ᵛ x, f x ∂[B; μ]) (∫ᵛ x, f x ∂[B; (μ + ν)]) : ℝ≥0∞) ≤ - ∫⁻ x, ‖f x‖ₑ ∂(ν.transpose B).variation := by + ‖B‖ₑ * ∫⁻ x, ‖f x‖ₑ ∂ν.variation := by rw [integral_add_vectorMeasure h₁ h₂, nndist_comm, nndist_eq_nnnorm, add_sub_cancel_left] exact enorm_integral_le_lintegral_enorm @@ -778,21 +807,22 @@ lemma variation_transpose_map_le : ((μ.map φ).transpose B).variation ≤ Measure.map φ (μ.transpose B).variation := by grw [transpose_map, variation_map_le] +omit [NormedSpace ℝ E] [NormedSpace ℝ F] in theorem Integrable.map {β : Type*} [MeasurableSpace β] {φ : X → β} - {f : β → E} (hfm : AEStronglyMeasurable f ((μ.transpose B).variation.map φ)) - (h : μ.Integrable (f ∘ φ) B) : (μ.map φ).Integrable f B := by + {f : β → E} (hfm : AEStronglyMeasurable f (μ.variation.map φ)) + (h : μ.Integrable (f ∘ φ)) : (μ.map φ).Integrable f := by by_cases hφ : Measurable φ; swap · simp [VectorMeasure.map, hφ] simp_rw [VectorMeasure.Integrable] at h ⊢ apply ((integrable_map_measure hfm hφ.aemeasurable).2 h).mono_measure - apply variation_transpose_map_le + apply variation_map_le theorem integral_map {β : Type*} [MeasurableSpace β] {φ : X → β} (hφ : Measurable φ) {f : β → E} - (hfm : AEStronglyMeasurable f ((μ.transpose B).variation.map φ)) - (hfi' : μ.Integrable (f ∘ φ) B) : + (hfm : AEStronglyMeasurable f (μ.variation.map φ)) + (hfi' : μ.Integrable (f ∘ φ)) : ∫ᵛ y, f y ∂[B; μ.map φ] = ∫ᵛ x, f (φ x) ∂[B; μ] := by - apply setToFun_of_le_map _ _ hfi' hfm hφ variation_transpose_map_le + apply setToFun_of_le_map _ _ hfi' hfm hφ variation_map_le intro s x hs simp [hs, VectorMeasure.map, transpose, hφ] @@ -800,24 +830,24 @@ theorem _root_.MeasurableEmbedding.variation_transpose_map (hφ : MeasurableEmbe ((μ.map φ).transpose B).variation = (μ.transpose B).variation.map φ := by rw [transpose_map, hφ.variation_map] +omit [NormedSpace ℝ E] [NormedSpace ℝ F] in theorem _root_.MeasurableEmbedding.integrable_map_vectorMeasure (hφ : MeasurableEmbedding φ) {f : β → E} : - (μ.map φ).Integrable f B ↔ μ.Integrable (f ∘ φ) B := by - simp_rw [VectorMeasure.Integrable, - ← hφ.integrable_map_iff (g := f) (μ := (μ.transpose B).variation), hφ.variation_transpose_map] + (μ.map φ).Integrable f ↔ μ.Integrable (f ∘ φ) := by + simp_rw [VectorMeasure.Integrable, ← hφ.integrable_map_iff, hφ.variation_map] theorem _root_.MeasurableEmbedding.integral_map_vectorMeasure (hφ : MeasurableEmbedding φ) {f : β → E} : ∫ᵛ y, f y ∂[B; μ.map φ] = ∫ᵛ x, f (φ x) ∂[B; μ] := by - by_cases hfm : AEStronglyMeasurable f ((μ.transpose B).variation.map φ) - · by_cases h'fm : μ.Integrable (f ∘ φ) B + by_cases hfm : AEStronglyMeasurable f (μ.variation.map φ) + · by_cases h'fm : μ.Integrable (f ∘ φ) · apply integral_map hφ.measurable hfm h'fm · rw [integral_undef, integral_undef] · exact h'fm · rwa [hφ.integrable_map_vectorMeasure] · rw [integral_non_aestronglyMeasurable, integral_non_aestronglyMeasurable] · rwa [hφ.aestronglyMeasurable_map_iff] at hfm - · rwa [hφ.variation_transpose_map] + · rwa [hφ.variation_map] theorem _root_.Topology.IsClosedEmbedding.integral_map_vectorMeasure [TopologicalSpace X] [BorelSpace X] @@ -832,40 +862,40 @@ theorem integral_map_equiv {β} [MeasurableSpace β] (e : X ≃ᵐ β) (f : β /-- **Lebesgue dominated convergence theorem** provides sufficient conditions under which almost everywhere convergence of a sequence of functions implies the convergence of their integrals. We could weaken the condition `bound_integrable` to require - `HasFiniteIntegral bound (μ.transpose B).variation` instead (i.e. not requiring that `bound` is + `HasFiniteIntegral bound μ.variation` instead (i.e. not requiring that `bound` is measurable), but in all applications proving integrability is easier. -/ theorem tendsto_integral_of_dominated_convergence {F : ℕ → X → E} {f : X → E} (bound : X → ℝ) - (F_measurable : ∀ n, AEStronglyMeasurable (F n) (μ.transpose B).variation) - (bound_integrable : Integrable bound (μ.transpose B).variation) - (h_bound : ∀ n, ∀ᵐ a ∂(μ.transpose B).variation, ‖F n a‖ ≤ bound a) - (h_lim : ∀ᵐ a ∂(μ.transpose B).variation, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))) : + (F_measurable : ∀ n, AEStronglyMeasurable (F n) μ.variation) + (bound_integrable : Integrable bound μ.variation) + (h_bound : ∀ n, ∀ᵐ a ∂μ.variation, ‖F n a‖ ≤ bound a) + (h_lim : ∀ᵐ a ∂μ.variation, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))) : Tendsto (fun n ↦ ∫ᵛ a, F n a ∂[B; μ]) atTop (𝓝 <| ∫ᵛ a, f a ∂[B; μ]) := tendsto_setToFun_of_dominated_convergence _ bound F_measurable bound_integrable h_bound h_lim /-- Lebesgue dominated convergence theorem for filters with a countable basis -/ theorem tendsto_integral_filter_of_dominated_convergence {l : Filter ι} [l.IsCountablyGenerated] {F : ι → X → E} {f : X → E} (bound : X → ℝ) - (hF_meas : ∀ᶠ n in l, AEStronglyMeasurable (F n) (μ.transpose B).variation) - (h_bound : ∀ᶠ n in l, ∀ᵐ a ∂(μ.transpose B).variation, ‖F n a‖ ≤ bound a) - (bound_integrable : Integrable bound (μ.transpose B).variation) - (h_lim : ∀ᵐ a ∂(μ.transpose B).variation, Tendsto (fun n ↦ F n a) l (𝓝 (f a))) : + (hF_meas : ∀ᶠ n in l, AEStronglyMeasurable (F n) μ.variation) + (h_bound : ∀ᶠ n in l, ∀ᵐ a ∂μ.variation, ‖F n a‖ ≤ bound a) + (bound_integrable : Integrable bound μ.variation) + (h_lim : ∀ᵐ a ∂μ.variation, Tendsto (fun n ↦ F n a) l (𝓝 (f a))) : Tendsto (fun n ↦ ∫ᵛ a, F n a ∂[B; μ]) l (𝓝 <| ∫ᵛ a, f a ∂[B; μ]) := tendsto_setToFun_filter_of_dominated_convergence _ bound hF_meas h_bound bound_integrable h_lim /-- Lebesgue dominated convergence theorem for series. -/ theorem hasSum_integral_of_dominated_convergence [Countable ι] {F : ι → X → E} {f : X → E} - (bound : ι → X → ℝ) (hF_meas : ∀ n, AEStronglyMeasurable (F n) (μ.transpose B).variation) - (h_bound : ∀ n, ∀ᵐ a ∂(μ.transpose B).variation, ‖F n a‖ ≤ bound n a) - (bound_summable : ∀ᵐ a ∂(μ.transpose B).variation, Summable fun n ↦ bound n a) - (bound_integrable : Integrable (fun a ↦ ∑' n, bound n a) (μ.transpose B).variation) - (h_lim : ∀ᵐ a ∂(μ.transpose B).variation, HasSum (fun n ↦ F n a) (f a)) : + (bound : ι → X → ℝ) (hF_meas : ∀ n, AEStronglyMeasurable (F n) μ.variation) + (h_bound : ∀ n, ∀ᵐ a ∂μ.variation, ‖F n a‖ ≤ bound n a) + (bound_summable : ∀ᵐ a ∂μ.variation, Summable fun n ↦ bound n a) + (bound_integrable : Integrable (fun a ↦ ∑' n, bound n a) μ.variation) + (h_lim : ∀ᵐ a ∂μ.variation, HasSum (fun n ↦ F n a) (f a)) : HasSum (fun n ↦ ∫ᵛ a, F n a ∂[B; μ]) (∫ᵛ a, f a ∂[B; μ]) := hasSum_setToFun_of_dominated_convergence _ bound hF_meas h_bound bound_summable bound_integrable h_lim theorem integral_tsum [CompleteSpace E] [Countable ι] - {f : ι → X → E} (hf : ∀ i, AEStronglyMeasurable (f i) (μ.transpose B).variation) - (hf' : ∑' i, ∫⁻ a : X, ‖f i a‖ₑ ∂(μ.transpose B).variation ≠ ∞) : + {f : ι → X → E} (hf : ∀ i, AEStronglyMeasurable (f i) μ.variation) + (hf' : ∑' i, ∫⁻ a : X, ‖f i a‖ₑ ∂μ.variation ≠ ∞) : ∫ᵛ a, ∑' i, f i a ∂[B; μ] = ∑' i, ∫ᵛ a, f i a ∂[B; μ] := setToFun_tsum _ hf hf' @@ -874,10 +904,10 @@ theorem integral_tsum [CompleteSpace E] [Countable ι] function `f`, then the integrals of `F n` with respect to a vector measure `μ` with finite variation converge to the integral of `f`. -/ theorem tendsto_integral_filter_of_norm_le_const {l : Filter ι} [l.IsCountablyGenerated] - {F : ι → X → E} [IsFiniteMeasure (μ.transpose B).variation] {f : X → E} - (h_meas : ∀ᶠ n in l, AEStronglyMeasurable (F n) (μ.transpose B).variation) - (h_bound : ∃ C, ∀ᶠ n in l, ∀ᵐ a ∂(μ.transpose B).variation, ‖F n a‖ ≤ C) - (h_lim : ∀ᵐ a ∂(μ.transpose B).variation, Tendsto (fun n ↦ F n a) l (𝓝 (f a))) : + {F : ι → X → E} [IsFiniteMeasure μ.variation] {f : X → E} + (h_meas : ∀ᶠ n in l, AEStronglyMeasurable (F n) μ.variation) + (h_bound : ∃ C, ∀ᶠ n in l, ∀ᵐ a ∂μ.variation, ‖F n a‖ ≤ C) + (h_lim : ∀ᵐ a ∂μ.variation, Tendsto (fun n ↦ F n a) l (𝓝 (f a))) : Tendsto (fun n ↦ ∫ᵛ a, F n a ∂[B; μ]) l (𝓝 (∫ᵛ a, f a ∂[B; μ])) := tendsto_setToFun_filter_of_norm_le_const _ h_meas h_bound h_lim diff --git a/Mathlib/MeasureTheory/VectorMeasure/Prod.lean b/Mathlib/MeasureTheory/VectorMeasure/Prod.lean new file mode 100644 index 00000000000000..3b8ffc3487bdef --- /dev/null +++ b/Mathlib/MeasureTheory/VectorMeasure/Prod.lean @@ -0,0 +1,458 @@ +/- +Copyright (c) 2026 Sébastien Gouëzel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sébastien Gouëzel +-/ +module + +public import Mathlib.MeasureTheory.Integral.Prod +public import Mathlib.MeasureTheory.VectorMeasure.SetIntegral +public import Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation + +/-! +# Product of vector measures +-/ + +public section + +open Filter Function MeasureTheory RCLike Set TopologicalSpace Topology +open scoped ENNReal NNReal Finset + +variable {ι X Y E F G H I J : Type*} {mX : MeasurableSpace X} {mY : MeasurableSpace Y} + [NormedAddCommGroup E] [NormedSpace ℝ E] + [NormedAddCommGroup F] [NormedSpace ℝ F] + [NormedAddCommGroup G] [NormedSpace ℝ G] + [NormedAddCommGroup H] [NormedSpace ℝ H] + [NormedAddCommGroup I] [NormedSpace ℝ I] + [NormedAddCommGroup J] [NormedSpace ℝ J] + {μ : VectorMeasure X E} {ν : VectorMeasure Y F} + {B : E →L[ℝ] F →L[ℝ] G} {f g : X → E} {s t : Set X} + +namespace MeasureTheory.VectorMeasure + +open scoped Classical in +/-- The product of two vector measures `μ` and `ν` with respect to a continuous bilinear map `B`, +giving mass `B (μ s) (ν s)` to a measurable set `s`. +If such a measure does not exist, we use the junk value `0`. -/ +noncomputable def prod (μ : VectorMeasure X E) (ν : VectorMeasure Y F) (B : E →L[ℝ] F →L[ℝ] G) : + VectorMeasure (X × Y) G := + if h : ∃ ρ : VectorMeasure (X × Y) G, ∀ (s : Set X) (t : Set Y), + MeasurableSet s → MeasurableSet t → ρ (s ×ˢ t) = B (μ s) (ν t) then h.choose + else 0 + +/-- Two vector measures `μ` and `ν` have a product with respect to `B` if there exists a +measure giving mass `B (μ s) (ν t)` to any measurable product `s × t`. +This is satisfied whenever `μ` or `ν` has finite variation. -/ +class HasProd (μ : VectorMeasure X E) (ν : VectorMeasure Y F) (B : E →L[ℝ] F →L[ℝ] G) : Prop where + exists_prod : ∃ ρ : VectorMeasure (X × Y) G, ∀ (s : Set X) (t : Set Y), + MeasurableSet s → MeasurableSet t → ρ (s ×ˢ t) = B (μ s) (ν t) + +lemma prod_eq_zero_of_not_hasProd (h : ¬HasProd μ ν B) : + μ.prod ν B = 0 := by + grind [HasProd, prod] + +@[simp] lemma prod_apply [h : HasProd μ ν B] {s : Set X} {t : Set Y} : + μ.prod ν B (s ×ˢ t) = B (μ s) (ν t) := by + rcases eq_or_ne s ∅ with rfl | hs + · simp + rcases eq_or_ne t ∅ with rfl | ht + · simp + by_cases h's : MeasurableSet s; swap + · simp only [h's, not_false_eq_true, not_measurable, _root_.map_zero, _root_.zero_apply] + rw [not_measurable] + simp [measurableSet_prod, hs, ht, h's] + by_cases h't : MeasurableSet t; swap + · simp only [h't, not_false_eq_true, not_measurable, _root_.map_zero] + rw [not_measurable] + simp [measurableSet_prod, hs, ht, h't] + simpa [prod, h.exists_prod] using h.exists_prod.choose_spec s t h's h't + +lemma HasProd.flip [HasProd μ ν B] : HasProd ν μ B.flip where + exists_prod := by + refine ⟨(μ.prod ν B).map Prod.swap, fun s t hs ht ↦ ?_⟩ + rw [map_apply _ (by fun_prop) (hs.prod ht)] + simp + +omit [NormedSpace ℝ F] in +/-- If `ν` is a vector measure, and `s ⊆ X × Y` is measurable, then `x ↦ ν { y | (x, y) ∈ s }` is +a strongly measurable function. -/ +theorem stronglyMeasurable_vectorMeasure_prodMk_left {s : Set (X × Y)} + (hs : MeasurableSet s) : StronglyMeasurable fun x ↦ ν (Prod.mk x ⁻¹' s) := by + induction s, hs + using MeasurableSpace.induction_on_inter generateFrom_prod.symm isPiSystem_prod with + | empty => simp [stronglyMeasurable_const] + | basic s hs => + obtain ⟨s, hs, t, -, rfl⟩ := hs + classical + simpa [mk_preimage_prod_right_eq_if, of_if] using stronglyMeasurable_const.indicator hs + | compl s hs ihs => + simp_rw [preimage_compl, VectorMeasure.of_compl (measurable_prodMk_left hs)] + exact stronglyMeasurable_const.sub ihs + | iUnion f hfd hfm ihf => + have (a : X) : HasSum (fun i ↦ ν (Prod.mk a ⁻¹' f i)) (ν (Prod.mk a ⁻¹' ⋃ i, f i)) := by + rw [preimage_iUnion] + apply hasSum_of_disjoint_iUnion + exacts [fun i ↦ measurable_prodMk_left (hfm i), hfd.mono fun _ _ ↦ .preimage _] + exact StronglyMeasurable.hasSum ihf this + +omit [NormedSpace ℝ E] in +theorem integrable_vectorMeasure_prodMk_left [IsFiniteMeasure μ.variation] + {s : Set (X × Y)} (hs : MeasurableSet s) : + μ.Integrable fun x ↦ ν (Prod.mk x ⁻¹' s) := by + refine Integrable.of_bound (μ := μ.variation) ?_ ν.bound ?_ + · exact (stronglyMeasurable_vectorMeasure_prodMk_left hs).aestronglyMeasurable + · exact Eventually.of_forall (fun x ↦ norm_apply_le_bound) + +open scoped Classical in +/-- The product of two vector measures when the first one has finite variation, obtained by +integrating the measure of the fibers, as in the definition of the product of positive measures. +*Do not use*: This is only used to instantiate the typeclass `HasProd`. Instead, use `μ.prod ν B`, +which uses the typeclass instance. -/ +noncomputable def prodOfIsFiniteMeasureLeft + (μ : VectorMeasure X E) (ν : VectorMeasure Y F) (B : E →L[ℝ] F →L[ℝ] G) + [IsFiniteMeasure μ.variation] : + VectorMeasure (X × Y) G where + measureOf' s := if MeasurableSet s then ∫ᵛ x, ν (Prod.mk x ⁻¹' s) ∂[B.flip; μ] else 0 + empty' := by simp + not_measurable' := by simp +contextual + m_iUnion' f f_meas f_disj := by + simp only [f_meas, ↓reduceIte, implies_true, MeasurableSet.iUnion, preimage_iUnion, + HasSum, SummationFilter.unconditional_filter] + have A (a : Finset ℕ) : ∑ y ∈ a, ∫ᵛ x, ν (Prod.mk x ⁻¹' f y) ∂[B.flip; μ] + = ∫ᵛ x, ∑ y ∈ a, ν (Prod.mk x ⁻¹' f y) ∂[B.flip; μ] := by + rw [integral_finsetSum _ (fun i hi ↦ integrable_vectorMeasure_prodMk_left (f_meas i))] + simp_rw [A] + apply tendsto_integral_filter_of_dominated_convergence (bound := fun x ↦ ν.bound) + · apply Eventually.of_forall (fun a ↦ ?_) + apply StronglyMeasurable.aestronglyMeasurable + apply Finset.stronglyMeasurable_fun_sum _ (fun i hi ↦ ?_) + apply stronglyMeasurable_vectorMeasure_prodMk_left (f_meas i) + · filter_upwards with a + filter_upwards with x + rw [← VectorMeasure.of_biUnion_finset] + · apply norm_apply_le_bound + · exact fun i hi j hj hij ↦ (f_disj hij).preimage _ + · exact fun i hi ↦ measurable_prodMk_left (f_meas i) + · apply integrable_const + · filter_upwards with x + apply hasSum_of_disjoint_iUnion + · exact fun i ↦ measurable_prodMk_left (f_meas i) + · exact fun i j hij ↦ (f_disj hij).preimage _ + +instance [CompleteSpace G] [IsFiniteMeasure μ.variation] : HasProd μ ν B where + exists_prod := by + classical + refine ⟨prodOfIsFiniteMeasureLeft μ ν B, fun s t hs ht ↦ ?_⟩ + simp only [prodOfIsFiniteMeasureLeft, hs.prod ht, ↓reduceIte, mk_preimage_prod_right_eq_if, + of_if, integral_indicator hs, setIntegral_const, ContinuousLinearMap.flip_apply] + +instance [CompleteSpace G] [h : IsFiniteMeasure ν.variation] : HasProd μ ν B := by + rw [← B.flip_flip] + apply HasProd.flip + +lemma prod_eq_of_forall_apply_prod {ρ : VectorMeasure (X × Y) G} (hρ : ∀ (s : Set X) (t : Set Y), + MeasurableSet s → MeasurableSet t → ρ (s ×ˢ t) = B (μ s) (ν t)) : + μ.prod ν B = ρ := by + have : HasProd μ ν B := ⟨ρ, hρ⟩ + apply ext_of_generateFrom _ _ generateFrom_prod.symm isPiSystem_prod + · rw [← univ_prod_univ, hρ _ _ MeasurableSet.univ MeasurableSet.univ, prod_apply] + · rintro - ⟨s, hs, t, ht, rfl⟩ + rw [prod_apply, hρ _ _ hs ht] + +lemma prod_apply_eq_integral [CompleteSpace G] [IsFiniteMeasure μ.variation] + {s : Set (X × Y)} (hs : MeasurableSet s) : + μ.prod ν B s = ∫ᵛ x, ν (Prod.mk x ⁻¹' s) ∂[B.flip; μ] := by + have : μ.prod ν B = prodOfIsFiniteMeasureLeft μ ν B := by + classical + apply prod_eq_of_forall_apply_prod (fun s t hs ht ↦ ?_) + simp only [prodOfIsFiniteMeasureLeft, hs.prod ht, ↓reduceIte, mk_preimage_prod_right_eq_if, + of_if, integral_indicator hs, setIntegral_const, ContinuousLinearMap.flip_apply] + rw [this] + simp [prodOfIsFiniteMeasureLeft, hs] + +lemma prod_flip_apply_eq_integral [CompleteSpace G] [IsFiniteMeasure μ.variation] + {B : F →L[ℝ] E →L[ℝ] G} {s : Set (X × Y)} (hs : MeasurableSet s) : + μ.prod ν B.flip s = ∫ᵛ x, ν (Prod.mk x ⁻¹' s) ∂[B; μ] := by + simp [prod_apply_eq_integral hs] + +lemma hasProd_flip [HasProd μ ν B] : HasProd ν μ B.flip where + exists_prod := by + refine ⟨(μ.prod ν B).map MeasurableEquiv.prodComm, fun s t hs ht ↦ ?_⟩ + rw [map_apply _ MeasurableEquiv.prodComm.measurable (hs.prod ht)] + simp [MeasurableEquiv.prodComm] + +lemma hasProd_flip_iff : HasProd ν μ B.flip ↔ HasProd μ ν B := + ⟨fun h ↦ by simpa using hasProd_flip (μ := ν) (ν := μ) (B := B.flip), fun h ↦ hasProd_flip⟩ + +lemma variation_prod_le [CompleteSpace G] [IsFiniteMeasure μ.variation] [SFinite ν.variation] : + (μ.prod ν B).variation ≤ ‖B‖ₑ • μ.variation.prod ν.variation := by + apply variation_le_of_forall_enorm_le (fun s hs ↦ ?_) + rw [prod_apply_eq_integral hs] + simp only [Measure.smul_apply, smul_eq_mul, Measure.prod_apply hs] + grw [enorm_integral_le_lintegral_enorm, ContinuousLinearMap.opENorm_flip, + enorm_measure_le_variation] + +instance [CompleteSpace G] [IsFiniteMeasure μ.variation] [IsFiniteMeasure ν.variation] : + IsFiniteMeasure (μ.prod ν B).variation := by + have : IsFiniteMeasure (‖B‖ₑ • μ.variation.prod ν.variation) := by + simp only [enorm_eq_nnnorm, Measure.coe_nnreal_smul] + infer_instance + exact isFiniteMeasure_of_le _ variation_prod_le + +omit [NormedSpace ℝ H] in +lemma _root_.MeasureTheory.Integrable.prod_vectorMeasure + [CompleteSpace G] [IsFiniteMeasure μ.variation] [IsFiniteMeasure ν.variation] + {f : X × Y → H} (hf : Integrable f (μ.variation.prod ν.variation)) : + (μ.prod ν B).Integrable f := + Integrable.of_measure_le_smul (by simp) variation_prod_le hf + +theorem integral_prod_swap (f : X × Y → H) {A : E →L[ℝ] F →L[ℝ] G} {B : H →L[ℝ] G →L[ℝ] I} : + ∫ᵛ z, f z.swap ∂[B; ν.prod μ A.flip] = ∫ᵛ z, f z ∂[B; μ.prod ν A] := by + have I (z : Y × X) : z.swap = MeasurableEquiv.prodComm z := rfl + simp_rw [I, ← integral_map_equiv] + congr + by_cases h : HasProd μ ν A; swap + · simp [prod_eq_zero_of_not_hasProd, h, hasProd_flip_iff] + have : HasProd ν μ A.flip := hasProd_flip + apply (prod_eq_of_forall_apply_prod (fun s t hs ht ↦ ?_)).symm + rw [map_apply _ MeasurableEquiv.prodComm.measurable (hs.prod ht)] + simp [MeasurableEquiv.prodComm] + +/-- The vector measure integral is measurable. This shows that the integrand of (the right-hand-side +of) Fubini's theorem is measurable. This version has `f` in curried form. -/ +theorem _root_.MeasureTheory.StronglyMeasurable.integral_vectorMeasure_prod_right + {B : G →L[ℝ] F →L[ℝ] H} [SFinite ν.variation] ⦃f : X → Y → G⦄ + (hf : StronglyMeasurable (uncurry f)) : StronglyMeasurable fun x ↦ ∫ᵛ y, f x y ∂[B; ν] := by + simp only [integral_eq_setToFun] + apply StronglyMeasurable.setToFun_prod_right _ (fun s hs ↦ ?_) hf + exact stronglyMeasurable_vectorMeasure_prodMk_left hs + +/-- The vector measure integral is measurable. This shows that the integrand of (the right-hand-side +of) Fubini's theorem is measurable. -/ +theorem _root_.MeasureTheory.StronglyMeasurable.integral_vectorMeasure_prod_right' + {B : G →L[ℝ] F →L[ℝ] H} [SFinite ν.variation] ⦃f : X × Y → G⦄ + (hf : StronglyMeasurable f) : StronglyMeasurable fun x ↦ ∫ᵛ y, f (x, y) ∂[B; ν] := by + rw [← uncurry_curry f] at hf; exact hf.integral_vectorMeasure_prod_right + +/-- The vector measure integral is measurable. This shows that the integrand of (the right-hand-side +of) the symmetric version of Fubini's theorem is measurable. +This version has `f` in curried form. -/ +theorem _root_.MeasureTheory.StronglyMeasurable.integral_vectorMeasure_prod_left + {B : G →L[ℝ] E →L[ℝ] H} [SFinite μ.variation] ⦃f : X → Y → G⦄ + (hf : StronglyMeasurable (uncurry f)) : StronglyMeasurable fun y ↦ ∫ᵛ x, f x y ∂[B; μ] := + (hf.comp_measurable measurable_swap).integral_vectorMeasure_prod_right' + +/-- The vector measure integral is measurable. This shows that the integrand of (the right-hand-side +of) the symmetric version of Fubini's theorem is measurable. -/ +theorem _root_.MeasureTheory.StronglyMeasurable.integral_vectorMeasure_prod_left' + {B : G →L[ℝ] E →L[ℝ] H} [SFinite μ.variation] ⦃f : X × Y → G⦄ + (hf : StronglyMeasurable f) : StronglyMeasurable fun y ↦ ∫ᵛ x, f (x, y) ∂[B; μ] := + (hf.comp_measurable measurable_swap).integral_vectorMeasure_prod_right' + +/-- The vector measure integral is a.e.-measurable. +This shows that the integrand of (the right-hand-side of) Fubini's theorem is a.e.-measurable. -/ +theorem _root_.MeasureTheory.AEStronglyMeasurable.integral_vectorMeasure_prod_right' + {B : G →L[ℝ] F →L[ℝ] H} [SFinite ν.variation] {μ : Measure X} + ⦃f : X × Y → G⦄ (hf : AEStronglyMeasurable f (μ.prod ν.variation)) : + AEStronglyMeasurable (fun x ↦ ∫ᵛ y, f (x, y) ∂[B; ν]) μ := + ⟨fun x ↦ ∫ᵛ y, hf.mk f (x, y) ∂[B; ν], + hf.stronglyMeasurable_mk.integral_vectorMeasure_prod_right', + by filter_upwards [Measure.ae_ae_of_ae_prod hf.ae_eq_mk] with _ hx using integral_congr_ae hx⟩ + +theorem _root_.MeasureTheory.Integrable.integral_vectorMeasure_prod_left {B : G →L[ℝ] F →L[ℝ] H} + [SFinite ν.variation] + {μ : Measure X} ⦃f : X × Y → G⦄ (hf : Integrable f (μ.prod ν.variation)) : + Integrable (fun x ↦ ∫ᵛ y, f (x, y) ∂[B; ν]) μ := by + apply Integrable.mono (hf.integral_norm_prod_left.const_mul ‖B‖) + (hf.aestronglyMeasurable.integral_vectorMeasure_prod_right') + filter_upwards with x + grw [norm_integral_le_integral_norm] + exact le_abs_self _ + +/-- Vector measure integrals commute with subtraction inside a lower Lebesgue integral. -/ +theorem lintegral_fn_integral_sub ⦃f g : X × Y → G⦄ {μ : Measure X} + {B : G →L[ℝ] F →L[ℝ] H} [SFinite μ] [SFinite ν.variation] + (φ : H → ℝ≥0∞) (hf : Integrable f (μ.prod ν.variation)) + (hg : Integrable g (μ.prod ν.variation)) : + (∫⁻ x, φ (∫ᵛ y, f (x, y) - g (x, y) ∂[B; ν]) ∂μ) = + ∫⁻ x, φ ((∫ᵛ y, f (x, y) ∂[B; ν]) - ∫ᵛ y, g (x, y) ∂[B; ν]) ∂μ := by + refine lintegral_congr_ae ?_ + filter_upwards [hf.prod_right_ae, hg.prod_right_ae] with x h2f h2g + simp [integral_fun_sub h2f h2g] + +/-- The map that sends an L¹-function `f : X × Y → G` to `∫∫f` is continuous. -/ +theorem continuous_integral_integral {B : G →L[ℝ] F →L[ℝ] H} {C : H →L[ℝ] E →L[ℝ] I} + [SFinite ν.variation] [SFinite μ.variation] : + Continuous fun f : X × Y →₁[μ.variation.prod ν.variation] G ↦ + ∫ᵛ x, (∫ᵛ y, f (x, y) ∂[B; ν]) ∂[C; μ] := by + rw [continuous_iff_continuousAt]; intro g + apply tendsto_integral_of_L1 + · exact (Integrable.integral_vectorMeasure_prod_left (L1.integrable_coeFn g)).aestronglyMeasurable + · filter_upwards with h + exact Integrable.integral_vectorMeasure_prod_left (L1.integrable_coeFn h) + simp_rw [← lintegral_fn_integral_sub _ (L1.integrable_coeFn _) (L1.integrable_coeFn g)] + apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds _ (fun i ↦ zero_le) _ + (h := fun i ↦ ∫⁻ x, ‖B‖ₑ * ∫⁻ y, + ‖i (x, y) - g (x, y)‖ₑ ∂ν.variation ∂μ.variation); swap + · exact fun i ↦ lintegral_mono fun x ↦ enorm_integral_le_lintegral_enorm + have this (i : X × Y →₁[μ.variation.prod ν.variation] G) : Measurable fun z ↦ ‖i z - g z‖ₑ := + ((Lp.stronglyMeasurable i).sub (Lp.stronglyMeasurable g)).enorm + simp_rw [lintegral_const_mul' ‖B‖ₑ _ (by simp)] + simp_rw [← lintegral_prod _ (this _).aemeasurable, ← L1.ofReal_norm_sub_eq_lintegral, + ofReal_norm] + suffices Tendsto (fun i ↦ ‖B‖ₑ * ‖i - g‖ₑ) (𝓝 g) (𝓝 (‖B‖ₑ * 0)) by simpa + apply ENNReal.Tendsto.const_mul _ (by simp) + rw [← tendsto_iff_enorm_sub_tendsto_zero] + exact tendsto_id + +/-- **Fubini's Theorem**: For integrable functions on `X × Y`, +the vector measure integral of `f` for the product vector measure is equal to the iterated vector +measure integral. We express this with respect to general pairing functions, with a compatibility +condition saying that the compositions coincide up to reordering. -/ +theorem integral_prod {B : G →L[ℝ] F →L[ℝ] J} {C : J →L[ℝ] E →L[ℝ] I} + {A : E →L[ℝ] F →L[ℝ] H} {D : G →L[ℝ] H →L[ℝ] I} + [CompleteSpace H] [CompleteSpace J] + [IsFiniteMeasure ν.variation] [IsFiniteMeasure μ.variation] + {f : X × Y → G} (hf : Integrable f (μ.variation.prod ν.variation)) + (h : ∀ x y z, D x (A y z) = C (B x z) y) : + ∫ᵛ z, f z ∂[D; μ.prod ν A] = ∫ᵛ x, (∫ᵛ y, f (x, y) ∂[B; ν]) ∂[C; μ] := by + by_cases hI : CompleteSpace I; swap + · simp only [integral_of_not_completeSpace hI] + revert f + apply Integrable.induction + · intro c s hs h2s + simp_rw [integral_indicator hs, ← indicator_comp_right, Function.comp_def, + integral_indicator (measurable_prodMk_left hs), setIntegral_const] + rw [integral_continuousLinearMap_comp (integrable_vectorMeasure_prodMk_left hs), + ← prod_flip_apply_eq_integral hs] + suffices (μ.prod ν A).mapRange (D c) (D c).continuous = μ.prod ν (C ∘SL B c).flip by + simp [← this] + apply (prod_eq_of_forall_apply_prod _).symm + intro s t hs ht + simp [h] + · intro f g hfg fint gint hf hg + rw [integral_add fint.prod_vectorMeasure gint.prod_vectorMeasure, hf, hg, + ← integral_add fint.integral_vectorMeasure_prod_left gint.integral_vectorMeasure_prod_left] + apply integral_congr_ae + filter_upwards [fint.prod_right_ae, gint.prod_right_ae] with x hx h'x + simp only [Pi.add_apply] + rw [integral_fun_add hx h'x] + · apply isClosed_eq ?_ continuous_integral_integral + let P : Lp G 1 (μ.variation.prod ν.variation) →L[ℝ] Lp G 1 (μ.prod ν A).variation := + Lp.LpToLpOfMeasureLeSMul (by simp) variation_prod_le + have M (f : Lp G 1 (μ.variation.prod ν.variation)) : + ∫ᵛ z, f z ∂[D; μ.prod ν A] = ∫ᵛ z, (P f) z ∂[D; μ.prod ν A] := by + apply integral_congr_ae + grw [Lp.coeFn_LpToLpOfMeasureLeSMul] + simp_rw [M] + exact Continuous.comp continuous_integral P.continuous + · intro f g hfg hf h'f + have ac : (μ.prod ν A).variation ≪ μ.variation.prod ν.variation := + Measure.absolutelyContinuous_of_le_smul variation_prod_le + rw [← integral_congr_ae (ac.ae_eq hfg), h'f] + apply integral_congr_ae + filter_upwards [Measure.ae_ae_of_ae_prod hfg] with x hx + exact integral_congr_ae hx + +/-- **Fubini's Theorem**: For integrable functions on `X × Y`, +the vector measure integral of `f` for the product vector measure is equal to the iterated vector +measure integral. Version where `f` is scalar. -/ +theorem integral_prod_smul [CompleteSpace F] {B : E →L[ℝ] F →L[ℝ] H} + [IsFiniteMeasure ν.variation] [IsFiniteMeasure μ.variation] + {f : X × Y → ℝ} (hf : Integrable f (μ.variation.prod ν.variation)) : + ∫ᵛ z, f z ∂•(μ.prod ν B) = ∫ᵛ x, (∫ᵛ y, f (x, y) ∂•ν) ∂[B.flip; μ] := by + by_cases h : CompleteSpace H + · exact integral_prod hf (fun x y z ↦ by simp) + · simp [integral_of_not_completeSpace, h] + +/-- Symmetric version of **Fubini's Theorem**: For integrable functions on `X × Y`, +the vector measure integral of `f` for the product vector measure is equal to the iterated vector +measure integral. We express this with respect to general pairing functions, with a compatibility +condition saying that the compositions coincide up to reordering. +This version has the integrals on the right-hand side in the other order. -/ +theorem integral_prod_symm {B : G →L[ℝ] E →L[ℝ] J} {C : J →L[ℝ] F →L[ℝ] I} + {A : E →L[ℝ] F →L[ℝ] H} {D : G →L[ℝ] H →L[ℝ] I} + [CompleteSpace H] [CompleteSpace J] + [IsFiniteMeasure ν.variation] [IsFiniteMeasure μ.variation] + {f : X × Y → G} (hf : Integrable f (μ.variation.prod ν.variation)) + (h : ∀ x y z, (D x) (A z y) = C (B x z) y) : + ∫ᵛ z, f z ∂[D; μ.prod ν A] = ∫ᵛ y, (∫ᵛ x, f (x, y) ∂[B; μ]) ∂[C; ν] := by + rw [← integral_prod_swap f] + exact integral_prod hf.swap h + +/-- **Fubini's Theorem**: For integrable functions on `X × Y`, +the vector measure integral of `f` for the product vector measure is equal to the iterated vector +measure integral. Version where `f` is scalar. +This version has the integrals on the right-hand side in the other order. -/ +theorem integral_prod_smul_symm [CompleteSpace E] {B : E →L[ℝ] F →L[ℝ] H} + [IsFiniteMeasure ν.variation] [IsFiniteMeasure μ.variation] + {f : X × Y → ℝ} (hf : Integrable f (μ.variation.prod ν.variation)) : + ∫ᵛ z, f z ∂•(μ.prod ν B) = ∫ᵛ y, (∫ᵛ x, f (x, y) ∂•μ) ∂[B; ν] := by + by_cases h : CompleteSpace H + · exact integral_prod_symm hf (fun x y z ↦ by simp) + · simp [integral_of_not_completeSpace, h] + +/-- Reversed version of **Fubini's Theorem**. -/ +theorem integral_integral {B : G →L[ℝ] F →L[ℝ] J} {C : J →L[ℝ] E →L[ℝ] I} + {A : E →L[ℝ] F →L[ℝ] H} {D : G →L[ℝ] H →L[ℝ] I} + [CompleteSpace H] [CompleteSpace J] + [IsFiniteMeasure ν.variation] [IsFiniteMeasure μ.variation] + {f : X → Y → G} (hf : Integrable (uncurry f) (μ.variation.prod ν.variation)) + (h : ∀ x y z, D x (A y z) = C (B x z) y) : + ∫ᵛ x, (∫ᵛ y, f x y ∂[B; ν]) ∂[C; μ] = ∫ᵛ z, f z.1 z.2 ∂[D; μ.prod ν A] := + (integral_prod hf h).symm + +/-- Reversed version of **Fubini's Theorem**, version with a scalar function. -/ +theorem integral_integral_smul [CompleteSpace F] {B : E →L[ℝ] F →L[ℝ] H} + [IsFiniteMeasure ν.variation] [IsFiniteMeasure μ.variation] + {f : X → Y → ℝ} (hf : Integrable (uncurry f) (μ.variation.prod ν.variation)) : + ∫ᵛ x, (∫ᵛ y, f x y ∂•ν) ∂[B.flip; μ] = ∫ᵛ z, f z.1 z.2 ∂•(μ.prod ν B) := + (integral_prod_smul hf).symm + +/-- Reversed version of **Fubini's Theorem** (symmetric version). -/ +theorem integral_integral_symm {B : G →L[ℝ] E →L[ℝ] J} {C : J →L[ℝ] F →L[ℝ] I} + {A : E →L[ℝ] F →L[ℝ] H} {D : G →L[ℝ] H →L[ℝ] I} + [CompleteSpace H] [CompleteSpace J] + [IsFiniteMeasure ν.variation] [IsFiniteMeasure μ.variation] + {f : X → Y → G} (hf : Integrable (uncurry f) (μ.variation.prod ν.variation)) + (h : ∀ x y z, (D x) (A z y) = C (B x z) y) : + ∫ᵛ y, (∫ᵛ x, f x y ∂[B; μ]) ∂[C; ν] = ∫ᵛ z, f z.1 z.2 ∂[D; μ.prod ν A] := + (integral_prod_symm hf h).symm + +/-- Reversed version of **Fubini's Theorem** (symmetric version), version with a scalar function. -/ +theorem integral_integral_smul_symm [CompleteSpace E] {B : E →L[ℝ] F →L[ℝ] H} + [IsFiniteMeasure ν.variation] [IsFiniteMeasure μ.variation] + {f : X → Y → ℝ} (hf : Integrable (uncurry f) (μ.variation.prod ν.variation)) : + ∫ᵛ y, (∫ᵛ x, f x y ∂•μ) ∂[B; ν] = ∫ᵛ z, f z.1 z.2 ∂•(μ.prod ν B) := + (integral_prod_smul_symm hf).symm + +/-- Change the order of Bochner integration in integrals wrt vector measures. +We express this with respect to general pairing functions, with a compatibility +condition saying that the compositions coincide up to reordering. -/ +theorem integral_integral_swap + [IsFiniteMeasure ν.variation] [IsFiniteMeasure μ.variation] + ⦃f : X → Y → G⦄ [CompleteSpace H] [CompleteSpace J] + {B : G →L[ℝ] F →L[ℝ] H} {C : H →L[ℝ] E →L[ℝ] I} + {A : G →L[ℝ] E →L[ℝ] J} {D : J →L[ℝ] F →L[ℝ] I} + (hf : Integrable (uncurry f) (μ.variation.prod ν.variation)) + (h : ∀ x y z, C (B x y) z = D (A x z) y) : + ∫ᵛ x, ∫ᵛ y, f x y ∂[B; ν] ∂[C; μ] = ∫ᵛ y, ∫ᵛ x, f x y ∂[A; μ] ∂[D; ν] := by + by_cases hI : CompleteSpace I; swap + · simp [integral_of_not_completeSpace, hI] + let P : (H →L[ℝ] I) →L[ℝ] (G →L[ℝ] H) →L[ℝ] (G →L[ℝ] I) := + ContinuousLinearMap.compL ℝ G H I + let A' := ContinuousLinearMap.bilinearComp P C.flip B.flip + let D' : G →L[ℝ] (G →L[ℝ] I) →L[ℝ] I := ContinuousLinearMap.apply ℝ I + rw [integral_integral (A := A') (D := D') hf (by simp [D', A', P])] + exact (integral_integral_symm hf (by simp [D', A', P, h])).symm + +/-- Change the order of Bochner integration in integrals wrt vector measures. +Case where `f` is scalar. -/ +theorem integral_integral_smul_swap [CompleteSpace E] [CompleteSpace F] + [IsFiniteMeasure ν.variation] [IsFiniteMeasure μ.variation] + ⦃f : X → Y → ℝ⦄ {B : E →L[ℝ] F →L[ℝ] G} + (hf : Integrable (uncurry f) (μ.variation.prod ν.variation)) : + ∫ᵛ x, ∫ᵛ y, f x y ∂•ν ∂[B.flip; μ] = ∫ᵛ y, ∫ᵛ x, f x y ∂•μ ∂[B; ν] := + integral_integral_swap hf (by simp) + +end MeasureTheory.VectorMeasure diff --git a/Mathlib/MeasureTheory/VectorMeasure/SetIntegral.lean b/Mathlib/MeasureTheory/VectorMeasure/SetIntegral.lean new file mode 100644 index 00000000000000..f03dcad579c6b2 --- /dev/null +++ b/Mathlib/MeasureTheory/VectorMeasure/SetIntegral.lean @@ -0,0 +1,591 @@ +/- +Copyright (c) 2026 Sébastien Gouëzel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sébastien Gouëzel +-/ +module + +public import Mathlib.MeasureTheory.VectorMeasure.Integral + +/-! +# Set integral + +In this file we prove properties of `∫ᵛ x in s, f x ∂[B; μ]`. Recall that this notation +is defined as `∫ᵛ x, f x ∂[B; μ.restrict s]`. + +The API in this file is modelled on the API for the Bochner integral. +-/ + +@[expose] public section + +assert_not_exists InnerProductSpace + +open Filter Function MeasureTheory RCLike Set TopologicalSpace Topology ContinuousLinearMap +open scoped ENNReal NNReal Finset + +variable {ι X E F G H : Type*} {mX : MeasurableSpace X} + [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [NormedAddCommGroup H] + {μ ν : VectorMeasure X F} {f g : X → E} {s t : Set X} + +namespace MeasureTheory.VectorMeasure + +theorem IntegrableOn.mono (hs : MeasurableSet s) (hts : t ⊆ s) (h : μ.IntegrableOn f s) : + μ.IntegrableOn f t := by + by_cases ht : MeasurableSet t; swap + · simp [VectorMeasure.IntegrableOn, restrict_not_measurable _ ht] + apply Integrable.mono_measure h + simp [variation_restrict, hs, ht, Measure.restrict_mono hts le_rfl] + +theorem IntegrableOn.union (hs : MeasurableSet s) (ht : MeasurableSet t) + (hf : μ.IntegrableOn f s) (h'f : μ.IntegrableOn f t) : + μ.IntegrableOn f (s ∪ t) := by + apply Integrable.mono_measure (hf.add_measure h'f) + grw [variation_restrict_le, Measure.restrict_union_le] + simp [variation_restrict, hs, ht] + +/- `simpNF` complains that this lemma can be proved by `simp`, because the `simp`-generated lemma +unfolds the abbrev `VectorMeasure.Integrable`. TODO: fix `simp`. See lean4#13958. -/ +@[simp, nolint simpNF] theorem IntegrableOn.empty : μ.IntegrableOn f ∅ := by + simp [VectorMeasure.IntegrableOn] + +theorem IntegrableOn.biUnion_finite + {s : Set ι} (hs : s.Finite) {t : ι → Set X} (ht : ∀ i ∈ s, MeasurableSet (t i)) + (h't : ∀ i ∈ s, μ.IntegrableOn f (t i)) : + μ.IntegrableOn f (⋃ i ∈ s, t i) := by + induction s, hs using Set.Finite.induction_on with + | empty => simp + | insert _ h's hf => + simp only [mem_insert_iff, forall_eq_or_imp, iUnion_iUnion_eq_or_left] at ht h't ⊢ + exact IntegrableOn.union ht.1 (h's.measurableSet_biUnion ht.2) h't.1 (hf ht.2 h't.2) + +theorem IntegrableOn.biUnion_finset {s : Finset ι} {t : ι → Set X} + (ht : ∀ i ∈ s, MeasurableSet (t i)) (h't : ∀ i ∈ s, μ.IntegrableOn f (t i)) : + μ.IntegrableOn f (⋃ i ∈ s, t i) := + IntegrableOn.biUnion_finite s.finite_toSet ht h't + +theorem IntegrableOn.iUnion_finite [Finite ι] {t : ι → Set X} + (ht : ∀ i, MeasurableSet (t i)) (h't : ∀ i, μ.IntegrableOn f (t i)) : + μ.IntegrableOn f (⋃ i, t i) := by + cases nonempty_fintype ι + simpa using IntegrableOn.biUnion_finset (f := f) (μ := μ) (s := Finset.univ) (t := t) + (fun i hi ↦ ht i) (fun i hi ↦ h't i) + +@[simp] theorem integrableOn_univ : μ.IntegrableOn f univ ↔ μ.Integrable f := by + simp [VectorMeasure.IntegrableOn] + +theorem Integrable.integrableOn (h : μ.Integrable f) : μ.IntegrableOn f s := by + rw [← integrableOn_univ] at h + exact h.mono MeasurableSet.univ (subset_univ _) + +theorem integrable_indicator_iff (hs : MeasurableSet s) : + μ.Integrable (indicator s f) ↔ μ.IntegrableOn f s := by + simp [VectorMeasure.Integrable, VectorMeasure.IntegrableOn, MeasureTheory.IntegrableOn, + MeasureTheory.integrable_indicator_iff hs, variation_restrict hs] + +theorem IntegrableOn.integrable_indicator (h : μ.IntegrableOn f s) (hs : MeasurableSet s) : + μ.Integrable (indicator s f) := + (integrable_indicator_iff hs).2 h + +variable [NormedSpace ℝ E] [NormedSpace ℝ F] [NormedSpace ℝ G] [NormedSpace ℝ H] + {B : E →L[ℝ] F →L[ℝ] G} + +theorem setIntegral_eq_zero_of_not_measurableSet (hs : ¬MeasurableSet s) : + ∫ᵛ x in s, f x ∂[B; μ] = 0 := by + simp [restrict_not_measurable _ hs] + +theorem setIntegral_congr_ae (h : ∀ᵐ x ∂μ.variation, x ∈ s → f x = g x) : + ∫ᵛ x in s, f x ∂[B; μ] = ∫ᵛ x in s, g x ∂[B; μ] := by + by_cases hs : MeasurableSet s; swap + · simp [setIntegral_eq_zero_of_not_measurableSet hs] + apply integral_congr_ae + rw [variation_restrict hs] + exact (ae_restrict_iff' hs).2 h + +theorem setIntegral_congr_fun (h : EqOn f g s) : + ∫ᵛ x in s, f x ∂[B; μ] = ∫ᵛ x in s, g x ∂[B; μ] := + setIntegral_congr_ae <| Eventually.of_forall h + +theorem setIntegral_union (hst : Disjoint s t) (hs : MeasurableSet s) (ht : MeasurableSet t) + (hfs : μ.IntegrableOn f s) (hft : μ.IntegrableOn f t) : + ∫ᵛ x in s ∪ t, f x ∂[B; μ] = ∫ᵛ x in s, f x ∂[B; μ] + ∫ᵛ x in t, f x ∂[B; μ] := by + rw [← integral_add_vectorMeasure hfs hft, μ.restrict_union hst hs ht] + +theorem setIntegral_sdiff (hs : MeasurableSet s) (ht : MeasurableSet t) + (hfs : μ.IntegrableOn f s) (hts : t ⊆ s) : + ∫ᵛ x in s \ t, f x ∂[B; μ] = ∫ᵛ x in s, f x ∂[B; μ] - ∫ᵛ x in t, f x ∂[B; μ] := by + rw [eq_sub_iff_add_eq, ← setIntegral_union (by grind) (hs.diff ht) ht (hfs.mono hs sdiff_subset) + (hfs.mono hs hts), sdiff_union_of_subset hts] + +theorem setIntegral_inter_add_sdiff (hs : MeasurableSet s) (ht : MeasurableSet t) + (hfs : μ.IntegrableOn f s) : + ∫ᵛ x in s ∩ t, f x ∂[B; μ] + ∫ᵛ x in s \ t, f x ∂[B; μ] = ∫ᵛ x in s, f x ∂[B; μ] := by + rw [← μ.restrict_inter_add_sdiff hs ht, + integral_add_vectorMeasure (hfs.mono hs inter_subset_left) (hfs.mono hs sdiff_subset)] + +theorem setIntegral_biUnion_finset {ι : Type*} (t : Finset ι) {s : ι → Set X} + (hs : ∀ i ∈ t, MeasurableSet (s i)) (h's : Set.Pairwise (↑t) (Disjoint on s)) + (hf : ∀ i ∈ t, μ.IntegrableOn f (s i)) : + ∫ᵛ x in ⋃ i ∈ t, s i, f x ∂[B; μ] = ∑ i ∈ t, ∫ᵛ x in s i, f x ∂[B; μ] := by + classical + induction t using Finset.induction_on with + | empty => simp + | insert _ _ hat IH => + simp only [Finset.coe_insert, Finset.forall_mem_insert, Set.pairwise_insert, + Finset.set_biUnion_insert] at hs hf h's ⊢ + rw [setIntegral_union] + · rw [Finset.sum_insert hat, IH hs.2 h's.1 hf.2] + · simp only [disjoint_iUnion_right] + exact fun i hi => (h's.2 i hi (ne_of_mem_of_not_mem hi hat).symm).1 + · exact hs.1 + · exact Finset.measurableSet_biUnion _ hs.2 + · exact hf.1 + · apply IntegrableOn.biUnion_finset hs.2 hf.2 + +theorem setIntegral_iUnion_fintype {ι : Type*} [Fintype ι] {s : ι → Set X} + (hs : ∀ i, MeasurableSet (s i)) (h's : Pairwise (Disjoint on s)) + (hf : ∀ i, μ.IntegrableOn f (s i)) : + ∫ᵛ x in ⋃ i, s i, f x ∂[B; μ] = ∑ i, ∫ᵛ x in s i, f x ∂[B; μ] := by + convert setIntegral_biUnion_finset Finset.univ (fun i _ => hs i) _ fun i _ => hf i + · simp + · simp [pairwise_univ, h's] + +theorem setIntegral_empty : ∫ᵛ x in ∅, f x ∂[B; μ] = 0 := by simp + +theorem setIntegral_univ : ∫ᵛ x in univ, f x ∂[B; μ] = ∫ᵛ x, f x ∂[B; μ] := by simp + +theorem setIntegral_add_compl (hs : MeasurableSet s) (hfi : μ.Integrable f) : + ∫ᵛ x in s, f x ∂[B; μ] + ∫ᵛ x in sᶜ, f x ∂[B; μ] = ∫ᵛ x, f x ∂[B; μ] := by + rw [← setIntegral_union disjoint_compl_right + hs hs.compl hfi.integrableOn hfi.integrableOn, union_compl_self, setIntegral_univ] + +theorem setIntegral_compl (hs : MeasurableSet s) (hfi : μ.Integrable f) : + ∫ᵛ x in sᶜ, f x ∂[B; μ] = ∫ᵛ x, f x ∂[B; μ] - ∫ᵛ x in s, f x ∂[B; μ] := by + rw [← setIntegral_add_compl (μ := μ) hs hfi, add_sub_cancel_left] + +/-- For a function `f` and a measurable set `s`, the integral of `indicator s f` +over the whole space is equal to `∫ᵛ x in s, f x ∂[B; μ]` +defined as `∫ᵛ x, f x ∂[B; μ.restrict s]`. -/ +theorem integral_indicator (hs : MeasurableSet s) : + ∫ᵛ x, indicator s f x ∂[B; μ] = ∫ᵛ x in s, f x ∂[B; μ] := by + by_cases hfi : μ.IntegrableOn f s; swap + · rw [integral_undef hfi, integral_undef] + rw [integrable_indicator_iff hs] + simpa [transpose_restrict, variation_restrict hs] using hfi + calc + ∫ᵛ x, indicator s f x ∂[B; μ] + _ = ∫ᵛ x in s, indicator s f x ∂[B; μ] + ∫ᵛ x in sᶜ, indicator s f x ∂[B; μ] := + (setIntegral_add_compl hs (hfi.integrable_indicator hs)).symm + _ = ∫ᵛ x in s, f x ∂[B; μ] + ∫ᵛ x in sᶜ, 0 ∂[B; μ] := by + apply congr_arg₂ (· + ·) (integral_congr_ae ?_) (integral_congr_ae ?_) + · rw [variation_restrict hs] + exact indicator_ae_eq_restrict hs + · rw [variation_restrict hs.compl] + exact indicator_ae_eq_restrict_compl hs + _ = ∫ᵛ x in s, f x ∂[B; μ] := by simp + +theorem setIntegral_indicator (hs : MeasurableSet s) (ht : MeasurableSet t) : + ∫ᵛ x in s, t.indicator f x ∂[B; μ] = ∫ᵛ x in s ∩ t, f x ∂[B; μ] := by + rw [integral_indicator ht, μ.restrict_restrict ht hs, Set.inter_comm] + +theorem setIntegral_congr_set + (hs : MeasurableSet s) (ht : MeasurableSet t) (hst : s =ᵐ[μ.variation] t) : + ∫ᵛ x in s, f x ∂[B; μ] = ∫ᵛ x in t, f x ∂[B; μ] := by + rw [← integral_indicator hs, ← integral_indicator ht] + apply integral_congr_ae + filter_upwards [hst] with x hx + replace hx : x ∈ s ↔ x ∈ t := by simpa using! hx + simp [indicator] + grind + +theorem integral_piecewise [DecidablePred (· ∈ s)] + (hs : MeasurableSet s) (hf : μ.IntegrableOn f s) (hg : μ.IntegrableOn g sᶜ) : + ∫ᵛ x, s.piecewise f g x ∂[B; μ] = ∫ᵛ x in s, f x ∂[B; μ] + ∫ᵛ x in sᶜ, g x ∂[B; μ] := by + rw [← Set.indicator_add_compl_eq_piecewise, + integral_add (hf.integrable_indicator hs) (hg.integrable_indicator hs.compl), + integral_indicator hs, integral_indicator hs.compl] + +theorem setIntegral_eq_zero_of_ae_eq_zero + (ht_eq : ∀ᵐ x ∂μ.variation, x ∈ t → f x = 0) : + ∫ᵛ x in t, f x ∂[B; μ] = 0 := by + by_cases ht : MeasurableSet t; swap + · simp [setIntegral_eq_zero_of_not_measurableSet ht] + by_cases hf : AEStronglyMeasurable f (μ.restrict t).variation; swap + · rw [integral_undef] + contrapose hf + exact hf.1 + simp only [variation_restrict ht] at hf + have : ∫ᵛ x in t, hf.mk f x ∂[B; μ] = 0 := by + refine integral_eq_zero_of_ae ?_ + simp only [variation_restrict ht] + apply (ae_restrict_iff' ht).2 + filter_upwards [ae_imp_of_ae_restrict hf.ae_eq_mk, ht_eq] with x hx h'x h''x + rw [← hx h''x] + exact h'x h''x + rw [← this] + apply integral_congr_ae + simp only [variation_restrict ht] + exact hf.ae_eq_mk + +theorem setIntegral_eq_zero_of_forall_eq_zero (ht_eq : ∀ x ∈ t, f x = 0) : + ∫ᵛ x in t, f x ∂[B; μ] = 0 := + setIntegral_eq_zero_of_ae_eq_zero (Eventually.of_forall ht_eq) + +theorem frequently_ae_ne_zero_of_setIntegral_ne_zero (hU : ∫ᵛ x in t, f x ∂[B; μ] ≠ 0) : + ∃ᶠ x in ae (μ.variation.restrict t), f x ≠ 0 := by + have ht : MeasurableSet t := by + contrapose! hU + simp [setIntegral_eq_zero_of_not_measurableSet hU] + rw [← variation_restrict ht] + exact frequently_ae_ne_zero_of_integral_ne_zero hU + +theorem exists_ne_zero_of_setIntegral_ne_zero (hU : ∫ᵛ x in t, f x ∂[B; μ] ≠ 0) : + ∃ x, x ∈ t ∧ f x ≠ 0 := by + contrapose! hU; exact setIntegral_eq_zero_of_forall_eq_zero hU + +theorem setIntegral_of_variation_apply_eq_zero (f : X → E) {s : Set X} + (hs : μ.variation s = 0) : + ∫ᵛ x in s, f x ∂[B; μ] = 0 := by + by_cases h's : MeasurableSet s; swap + · simp [restrict_not_measurable μ h's] + have : (μ.restrict s).variation = 0 := by + rw [variation_restrict h's] + apply Measure.restrict_eq_zero.2 hs + have : μ.restrict s = 0 := variation_eq_zero.1 this + simp [integral_eq_setToFun, this] + +theorem setIntegral_dirac' {mX : MeasurableSpace X} [CompleteSpace G] {a : X} {v : F} + (hf : StronglyMeasurable f) {s : Set X} (hs : MeasurableSet s) [Decidable (a ∈ s)] : + ∫ᵛ x in s, f x ∂[B; VectorMeasure.dirac a v] = if a ∈ s then B (f a) v else 0 := by + rw [restrict_dirac hs] + split_ifs + · exact integral_dirac' hf + · exact integral_zero_vectorMeasure + +theorem setIntegral_dirac [MeasurableSpace X] [MeasurableSingletonClass X] [CompleteSpace G] + {a : X} {v : F} {s : Set X} (hs : MeasurableSet s) [Decidable (a ∈ s)] : + ∫ᵛ x in s, f x ∂[B; VectorMeasure.dirac a v] = if a ∈ s then B (f a) v else 0 := by + rw [restrict_dirac hs] + split_ifs + · exact integral_dirac + · exact integral_zero_vectorMeasure + +theorem integral_singleton' [CompleteSpace G] {a : X} (hf : StronglyMeasurable f) : + ∫ᵛ a in {a}, f a ∂[B; μ] = B (f a) (μ {a}) := by + simp only [restrict_singleton, integral_dirac' hf] + +theorem integral_singleton [MeasurableSingletonClass X] {a : X} [CompleteSpace G] : + ∫ᵛ a in {a}, f a ∂[B; μ] = B (f a) (μ {a}) := by + simp only [restrict_singleton, integral_dirac] + +theorem setIntegral_union_eq_left_of_ae (hs : MeasurableSet s) (ht : MeasurableSet t) + (ht_eq : ∀ᵐ x ∂μ.variation.restrict t, f x = 0) : + ∫ᵛ x in s ∪ t, f x ∂[B; μ] = ∫ᵛ x in s, f x ∂[B; μ] := by + classical + rw [← integral_indicator hs, ← integral_indicator (hs.union ht)] + apply integral_congr_ae + rw [ae_restrict_iff' ht] at ht_eq + filter_upwards [ht_eq] with x hx + classical + simp only [indicator_apply, mem_union] + grind + +theorem setIntegral_union_eq_left_of_forall (hs : MeasurableSet s) (ht : MeasurableSet t) + (ht_eq : ∀ x ∈ t, f x = 0) : ∫ᵛ x in s ∪ t, f x ∂[B; μ] = ∫ᵛ x in s, f x ∂[B; μ] := by + apply setIntegral_union_eq_left_of_ae hs ht + rw [ae_restrict_iff' ht] + filter_upwards with x using ht_eq x + +theorem setIntegral_eq_of_subset_of_ae_sdiff_eq_zero (hs : MeasurableSet s) (ht : MeasurableSet t) + (hts : s ⊆ t) (h't : ∀ᵐ x ∂μ.variation.restrict (t \ s), f x = 0) : + ∫ᵛ x in t, f x ∂[B; μ] = ∫ᵛ x in s, f x ∂[B; μ] := by + rwa [← union_sdiff_cancel hts, setIntegral_union_eq_left_of_ae hs (ht.diff hs)] + +/-- If a function vanishes on `t \ s` with `s ⊆ t`, then its integrals on `s` +and `t` coincide. -/ +theorem setIntegral_eq_of_subset_of_forall_sdiff_eq_zero + (hs : MeasurableSet s) (ht : MeasurableSet t) (hts : s ⊆ t) + (h't : ∀ x ∈ t \ s, f x = 0) : ∫ᵛ x in t, f x ∂[B; μ] = ∫ᵛ x in s, f x ∂[B; μ] := by + apply setIntegral_eq_of_subset_of_ae_sdiff_eq_zero hs ht hts + apply (ae_restrict_iff' (ht.diff hs)).2 + filter_upwards with x using h't x + +/-- If a function vanishes almost everywhere on `sᶜ`, then its integral on `s` +coincides with its integral on the whole space. -/ +theorem setIntegral_eq_integral_of_ae_compl_eq_zero (hs : MeasurableSet s) + (h : ∀ᵐ x ∂μ.variation, x ∉ s → f x = 0) : + ∫ᵛ x in s, f x ∂[B; μ] = ∫ᵛ x, f x ∂[B; μ] := by + symm + nth_rw 1 [← setIntegral_univ] + apply setIntegral_eq_of_subset_of_ae_sdiff_eq_zero hs MeasurableSet.univ (subset_univ _) + apply (ae_restrict_iff' (MeasurableSet.univ.diff hs)).2 + filter_upwards [h] with x hx h'x using hx h'x.2 + +/-- If a function vanishes on `sᶜ`, then its integral on `s` coincides with its integral on the +whole space. -/ +theorem setIntegral_eq_integral_of_forall_compl_eq_zero (hs : MeasurableSet s) + (h : ∀ x, x ∉ s → f x = 0) : + ∫ᵛ x in s, f x ∂[B; μ] = ∫ᵛ x, f x ∂[B; μ] := + setIntegral_eq_integral_of_ae_compl_eq_zero hs (Eventually.of_forall h) + +theorem setIntegral_const [CompleteSpace G] [IsFiniteMeasure (μ.variation.restrict s)] + (c : E) : ∫ᵛ _ in s, c ∂[B; μ] = B c (μ s) := by + by_cases hs : MeasurableSet s + · have : IsFiniteMeasure (μ.restrict s).variation := by + rwa [variation_restrict hs] + rw [integral_const, restrict_apply _ hs MeasurableSet.univ, univ_inter] + · simp [setIntegral_eq_zero_of_not_measurableSet hs, μ.not_measurable' hs] + +@[simp] +theorem integral_indicator_const [CompleteSpace G] + (e : E) ⦃s : Set X⦄ [IsFiniteMeasure (μ.variation.restrict s)] + (s_meas : MeasurableSet s) : + ∫ᵛ x, s.indicator (fun _ : X ↦ e) x ∂[B; μ] = B e (μ s) := by + rw [integral_indicator s_meas, ← setIntegral_const] + +theorem setIntegral_map {β : Type*} [MeasurableSpace β] + {φ : X → β} (hφ : Measurable φ) {f : β → E} {s : Set β} (hs : MeasurableSet s) + (hfm : AEStronglyMeasurable f ((μ.restrict (φ ⁻¹' s)).variation.map φ)) + (hfi' : μ.Integrable (f ∘ φ)) : + ∫ᵛ y in s, f y ∂[B; μ.map φ] = ∫ᵛ x in φ ⁻¹' s, f (φ x) ∂[B; μ] := by + rw [restrict_map μ hφ hs, integral_map hφ hfm hfi'.integrableOn] + +theorem _root_.MeasurableEmbedding.setIntegral_map_vectorMeasure {β : Type*} [MeasurableSpace β] + {φ : X → β} {f : β → E} (hφ : MeasurableEmbedding φ) {s : Set β} (hs : MeasurableSet s) : + ∫ᵛ y in s, f y ∂[B; μ.map φ] = ∫ᵛ x in φ ⁻¹' s, f (φ x) ∂[B; μ] := by + rw [restrict_map μ hφ.measurable hs, hφ.integral_map_vectorMeasure] + +theorem _root_.Topology.IsClosedEmbedding.setIntegral_map_vectorMeasure + [TopologicalSpace X] [BorelSpace X] {β : Type*} + [MeasurableSpace β] [TopologicalSpace β] [BorelSpace β] {φ : X → β} {f : β → E} {s : Set β} + (hs : MeasurableSet s) (hφ : IsClosedEmbedding φ) : + ∫ᵛ y in s, f y ∂[B; μ.map φ] = ∫ᵛ x in φ ⁻¹' s, f (φ x) ∂[B; μ] := + hφ.measurableEmbedding.setIntegral_map_vectorMeasure hs + +theorem setIntegral_map_equiv {β : Type*} [MeasurableSpace β] {e : X ≃ᵐ β} {f : β → E} {s : Set β} + (hs : MeasurableSet s) : + ∫ᵛ y in s, f y ∂[B; μ.map e] = ∫ᵛ x in e ⁻¹' s, f (e x) ∂[B; μ] := + e.measurableEmbedding.setIntegral_map_vectorMeasure hs + +theorem continuousLinearMap_apply_integral + [CompleteSpace G] [CompleteSpace H] + {C : G →L[ℝ] H} (hf : Integrable f μ.variation) : + C (∫ᵛ y, f y ∂[B; μ]) = ∫ᵛ y, f y ∂[((compL ℝ F G H C) ∘L B); μ] := by + apply hf.induction (P := fun f ↦ C (∫ᵛ y, f y ∂[B; μ]) = ∫ᵛ y, f y ∂[((compL ℝ F G H C) ∘L B); μ]) + · intro c s hs hc + have : IsFiniteMeasure (μ.variation.restrict s) := ⟨by simpa⟩ + simp [integral_indicator_const _ hs] + · intro f g _ f_int g_int hf hg + simp only [Pi.add_apply] + simp [integral_fun_add, f_int, g_int, hf, hg] + · apply isClosed_eq + · apply C.continuous.comp continuous_integral + · exact continuous_integral + · intro f g hfg _ hf + rw [← integral_congr_ae hfg, ← integral_congr_ae hfg, hf] + +theorem integral_continuousLinearMap_comp + {f : X → H} {C : H →L[ℝ] E} (hf : Integrable f μ.variation) : + ∫ᵛ y, C (f y) ∂[B; μ] = ∫ᵛ y, f y ∂[B ∘L C; μ] := by + by_cases hG : CompleteSpace G; swap + · simp [integral_of_not_completeSpace hG] + apply hf.induction (P := fun f ↦ ∫ᵛ y, C (f y) ∂[B; μ] = ∫ᵛ y, f y ∂[B ∘L C; μ]) + · intro c s hs hc + have : IsFiniteMeasure (μ.variation.restrict s) := ⟨by simpa⟩ + rw [integral_indicator_const _ hs] + have : (fun y ↦ C (s.indicator (fun x ↦ c) y)) = s.indicator (fun x ↦ C c) := by + ext; simp only [indicator]; grind + simp_rw [this] + rw [integral_indicator_const _ hs] + rfl + · intro f g _ f_int g_int hf hg + simp only [Pi.add_apply, _root_.map_add] + rw [integral_fun_add (C.integrable_comp f_int) (C.integrable_comp g_int), hf, hg, + integral_fun_add f_int g_int] + · apply isClosed_eq + · have I (f : Lp H 1 μ.variation) : ∫ᵛ x, C (f x) ∂[B; μ] = ∫ᵛ x, (C.compLp f) x ∂[B; μ] := + (integral_congr_ae (coeFn_compLp _ _)).symm + simp_rw [I] + exact continuous_integral.comp (C.compLpL 1 μ.variation).continuous + · exact continuous_integral + · intro f g hfg _ hf + have : ∀ᵐ x ∂μ.variation, C (f x) = C (g x) := by + filter_upwards [hfg] with x hx using by simp [hx] + rw [← integral_congr_ae hfg, ← integral_congr_ae this, hf] + +theorem enorm_setIntegral_le_of_enorm_le_const_ae {C : ℝ≥0∞} + (hC : ∀ᵐ x ∂μ.variation.restrict s, ‖f x‖ₑ ≤ C) : + ‖∫ᵛ x in s, f x ∂[B; μ]‖ₑ ≤ C * ‖B‖ₑ * μ.variation s := by + by_cases hs : MeasurableSet s; swap + · simp [setIntegral_eq_zero_of_not_measurableSet hs] + rw [← variation_restrict hs] at hC + apply (enorm_integral_le_of_enorm_le_const hC).trans + rw [variation_restrict hs, Measure.restrict_apply MeasurableSet.univ] + simp + +theorem enorm_setIntegral_le_of_enorm_le_const {C : ℝ≥0∞} + (hC : ∀ x ∈ s, ‖f x‖ₑ ≤ C) : + ‖∫ᵛ x in s, f x ∂[B; μ]‖ₑ ≤ C * ‖B‖ₑ * μ.variation s := by + by_cases hs : MeasurableSet s; swap + · simp [setIntegral_eq_zero_of_not_measurableSet hs] + apply enorm_setIntegral_le_of_enorm_le_const_ae + apply (ae_restrict_iff' hs).2 + filter_upwards with x using hC x + +theorem norm_setIntegral_le_of_norm_le_const_ae {C : ℝ} + [h : IsFiniteMeasure (μ.variation.restrict s)] + (hC : ∀ᵐ x ∂μ.variation.restrict s, ‖f x‖ ≤ C) : + ‖∫ᵛ x in s, f x ∂[B; μ]‖ ≤ C * ‖B‖ * μ.variation.real s := by + by_cases hs : MeasurableSet s; swap + · simp only [setIntegral_eq_zero_of_not_measurableSet hs, norm_zero] + by_cases h's : μ.variation s = 0 + · simp [Measure.real, h's] + · have : NeBot (ae (μ.variation.restrict s)) := by simpa using h's + obtain ⟨x, hx⟩ : ∃ x, ‖f x‖ ≤ C := hC.exists + have : 0 ≤ C := le_trans (norm_nonneg _) hx + positivity + rw [← variation_restrict hs] at hC h + apply (norm_integral_le_of_norm_le_const hC).trans_eq + simp [variation_restrict hs] + +theorem norm_setIntegral_le_of_norm_le_const {C : ℝ} + [h : IsFiniteMeasure (μ.variation.restrict s)] + (hC : ∀ x ∈ s, ‖f x‖ ≤ C) : + ‖∫ᵛ x in s, f x ∂[B; μ]‖ ≤ C * ‖B‖ * μ.variation.real s := by + rcases eq_empty_or_nonempty s with rfl | ⟨x, hx⟩ + · simp + by_cases hs : MeasurableSet s; swap + · simp only [setIntegral_eq_zero_of_not_measurableSet hs, norm_zero] + have : 0 ≤ C := le_trans (norm_nonneg _) (hC x hx) + positivity + apply norm_setIntegral_le_of_norm_le_const_ae + filter_upwards [ae_restrict_mem hs] with x hx using hC x hx + +theorem enorm_setIntegral_le_lintegral_enorm : + ‖∫ᵛ x in s, f x ∂[B; μ]‖ₑ ≤ ‖B‖ₑ * ∫⁻ x in s, ‖f x‖ₑ ∂μ.variation := by + grw [enorm_integral_le_lintegral_enorm, variation_restrict_le] + +theorem enorm_setIntegral_le_lintegral_enorm_transpose : + ‖∫ᵛ x in s, f x ∂[B; μ]‖ₑ ≤ ∫⁻ x in s, ‖f x‖ₑ ∂(μ.transpose B).variation := by + grw [enorm_integral_le_lintegral_enorm_transpose, transpose_restrict,variation_restrict_le] + +private theorem hasSum_setIntegral_iUnion_nat {s : ℕ → Set X} + (hm : ∀ i, MeasurableSet (s i)) (hd : Pairwise (Disjoint on s)) + (hfi : μ.IntegrableOn f (⋃ i, s i)) : + HasSum (fun n ↦ ∫ᵛ x in s n, f x ∂[B; μ]) (∫ᵛ x in ⋃ n, s n, f x ∂[B; μ]) := by + by_cases hG : CompleteSpace G; swap + · simp [integral_of_not_completeSpace hG] + have I : ∑' i, ‖B‖ₑ * ∫⁻ x in s i, ‖f x‖ₑ ∂μ.variation < ∞ := calc + ∑' i, ‖B‖ₑ * ∫⁻ x in s i, ‖f x‖ₑ ∂μ.variation + _ = ‖B‖ₑ * ∫⁻ x in (⋃ i, s i), ‖f x‖ₑ ∂μ.variation := by + rw [ENNReal.tsum_mul_left, lintegral_iUnion hm hd] + _ < ∞ := by + simp only [VectorMeasure.IntegrableOn, VectorMeasure.Integrable, + variation_restrict (MeasurableSet.iUnion hm)] at hfi + exact ENNReal.mul_lt_top (by simp) hfi.2 + have : Summable (fun n ↦ ∫ᵛ x in s n, f x ∂[B; μ]) := by + apply Summable.of_enorm (lt_of_le_of_lt _ I).ne + gcongr + exact enorm_setIntegral_le_lintegral_enorm + apply (Summable.hasSum_iff_tendsto_nat this).2 + simp_rw [tendsto_iff_edist_tendsto_0, edist_eq_enorm_sub, enorm_sub_rev] + apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds + (ENNReal.tendsto_sum_nat_add _ I.ne) (by positivity) (fun N ↦ ?_) + have : ⋃ n, s n = (⋃ n ∈ Finset.range N, s n) ∪ (⋃ n, s (n + N)) := by + ext x + have : (∃ i, x ∈ s (i + N)) ↔ (∃ i ≥ N, x ∈ s i) := + ⟨fun ⟨i, hi⟩ ↦ ⟨i + N, by grind⟩, fun ⟨i, hi, h'i⟩ ↦ ⟨i - N, by grind⟩⟩ + simp only [mem_iUnion, Finset.mem_range, mem_union, exists_prop, this, ge_iff_le] + grind + rw [this, setIntegral_union]; rotate_left + · simp only [Finset.mem_range, disjoint_iUnion_right, disjoint_iUnion_left] + intro i j hi + apply hd (by grind) + · apply MeasurableSet.biUnion (Finset.countable_toSet _) (fun i hi ↦ hm i) + · apply MeasurableSet.iUnion (fun i ↦ hm _) + · apply hfi.mono (MeasurableSet.iUnion hm) (by simp [subset_iUnion s]) + · apply hfi.mono (MeasurableSet.iUnion hm) (by simp [subset_iUnion s]) + rw [setIntegral_biUnion_finset]; rotate_left + · exact fun i hi ↦ hm i + · exact fun i hi j hj hij ↦ hd hij + · exact fun i hi ↦ hfi.mono (MeasurableSet.iUnion hm) (by simp [subset_iUnion s]) + simp only [add_sub_cancel_left] + apply enorm_setIntegral_le_lintegral_enorm.trans_eq + rw [lintegral_iUnion (fun i ↦ hm _), ENNReal.tsum_mul_left] + exact fun i j hij ↦ hd (by grind) + +theorem hasSum_setIntegral_iUnion {ι : Type*} [Countable ι] {s : ι → Set X} + (hm : ∀ i, MeasurableSet (s i)) (hd : Pairwise (Disjoint on s)) + (hfi : μ.IntegrableOn f (⋃ i, s i)) : + HasSum (fun n ↦ ∫ᵛ x in s n, f x ∂[B; μ]) (∫ᵛ x in ⋃ n, s n, f x ∂[B; μ]) := by + classical + rcases finite_or_infinite ι with hι | hι + · letI : Fintype ι := Fintype.ofFinite ι + have : ∫ᵛ x in ⋃ n, s n, f x ∂[B; μ] = ∑ i, ∫ᵛ x in s i, f x ∂[B; μ] := by + rw [setIntegral_iUnion_fintype hm hd (fun i ↦ ?_)] + exact hfi.mono (MeasurableSet.iUnion hm) (by simp [subset_iUnion s]) + rw [this] + apply hasSum_fintype + obtain ⟨e⟩ : Nonempty (ι ≃ ℕ) := nonempty_equiv_of_countable + rw [← e.symm.surjective.iUnion_comp, ← e.symm.hasSum_iff] + apply hasSum_setIntegral_iUnion_nat (fun i ↦ hm _) (fun i j hij ↦ hd (by simp [hij])) + rwa [e.symm.surjective.iUnion_comp] + +theorem integral_iUnion {ι : Type*} [Countable ι] {s : ι → Set X} (hm : ∀ i, MeasurableSet (s i)) + (hd : Pairwise (Disjoint on s)) (hfi : μ.IntegrableOn f (⋃ i, s i)) : + ∫ᵛ x in ⋃ n, s n, f x ∂[B; μ] = ∑' n, ∫ᵛ x in s n, f x ∂[B; μ] := + (HasSum.tsum_eq (hasSum_setIntegral_iUnion hm hd hfi)).symm + +@[simp] theorem setIntegral_toSignedMeasure {μ : Measure X} [IsFiniteMeasure μ] + {f : X → G} {s : Set X} (hs : MeasurableSet s) : + ∫ᵛ x in s, f x ∂<•μ.toSignedMeasure = ∫ x in s, f x ∂μ := by + rw [← integral_toSignedMeasure, restrict_toSignedMeasure hs] + +/-- If `f` is integrable, then `∫ᵛ x in s, f x ∂[B; μ]` is absolutely continuous in `s`: +it tends to zero as `μ.variation s` tends to zero. -/ +theorem Integrable.tendsto_setIntegral_nhds_zero {ι : Type*} + (hf : μ.Integrable f) {l : Filter ι} {s : ι → Set X} + (hs : Tendsto (μ.variation ∘ s) l (𝓝 0)) : + Tendsto (fun i ↦ ∫ᵛ x in s i, f x ∂[B; μ]) l (𝓝 0) := by + rw [tendsto_zero_iff_norm_tendsto_zero] + simp_rw [← coe_nnnorm, ← NNReal.coe_zero, NNReal.tendsto_coe, ← ENNReal.tendsto_coe, + ENNReal.coe_zero] + have : Tendsto (fun i ↦ ‖B‖ₑ * ∫⁻ (x : X) in s i, ‖f x‖ₑ ∂μ.variation) l (𝓝 (‖B‖ₑ * 0)) := + ENNReal.Tendsto.const_mul (tendsto_setLIntegral_zero (ne_of_lt hf.2) hs) (by simp) + rw [mul_zero] at this + apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds this (fun i ↦ zero_le) + intro i + apply enorm_integral_le_lintegral_enorm.trans + dsimp + gcongr + exact variation_restrict_le + +/-- If `F i → f` in `L1`, then `∫ᵛ x in s, F i x ∂[B; μ] → ∫ᵛ x in s, f x ∂[B; μ]`. -/ +lemma tendsto_setIntegral_of_L1 {ι} (f : X → E) + (hfi : AEStronglyMeasurable f μ.variation) {F : ι → X → E} + {l : Filter ι} (hFi : ∀ᶠ i in l, μ.Integrable (F i)) + (hF : Tendsto (fun i ↦ ∫⁻ x, ‖F i x - f x‖ₑ ∂μ.variation) l (𝓝 0)) + (s : Set X) : + Tendsto (fun i ↦ ∫ᵛ x in s, F i x ∂[B; μ]) l (𝓝 (∫ᵛ x in s, f x ∂[B; μ])) := by + refine tendsto_integral_of_L1 f ?_ ?_ ?_ + · apply hfi.mono_measure + grw [variation_restrict_le, Measure.restrict_le_self] + · filter_upwards [hFi] with i hi using hi.restrict + · simp_rw [← eLpNorm_one_eq_lintegral_enorm] at hF ⊢ + apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hF (fun _ ↦ zero_le) + (fun i ↦ ?_) + apply eLpNorm_mono_measure + grw [variation_restrict_le] + apply Measure.restrict_le_self + +/-- If `F i → f` in `L1`, then `∫ᵛ x in s, F i x ∂[B; μ] → ∫ᵛ x in s, f x ∂[B; μ]`. -/ +lemma tendsto_setIntegral_of_L1' {ι} (f : X → E) + (hfi : AEStronglyMeasurable f μ.variation) {F : ι → X → E} + {l : Filter ι} (hFi : ∀ᶠ i in l, μ.Integrable (F i)) + (hF : Tendsto (fun i ↦ eLpNorm (F i - f) 1 μ.variation) l (𝓝 0)) + (s : Set X) : + Tendsto (fun i ↦ ∫ᵛ x in s, F i x ∂[B; μ]) l (𝓝 (∫ᵛ x in s, f x ∂[B; μ])) := by + refine tendsto_setIntegral_of_L1 f hfi hFi ?_ s + simp_rw [eLpNorm_one_eq_lintegral_enorm, Pi.sub_apply] at hF + exact hF + +end MeasureTheory.VectorMeasure diff --git a/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean b/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean index 90022637bbd5a5..be1a0b591dc30f 100644 --- a/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean +++ b/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean @@ -75,6 +75,31 @@ lemma le_variation (μ : VectorMeasure X V) {s : Set X} (hs : MeasurableSet s) { simp only [sup_set_eq_biUnion, id_eq] exact hs.diff <| .biUnion (Finset.countable_toSet _) (by simp) +/-- Measure version of `preVariation.exists_Finpartition_sum_gt`. -/ +lemma exists_lt_sum_of_lt_variation (μ : VectorMeasure X V) {s : Set X} (hs : MeasurableSet s) + {a : ℝ≥0∞} (ha : a < μ.variation s) : + ∃ (P : Finset (Set X)), (∀ t ∈ P, t ⊆ s) ∧ ((P : Set (Set X)).PairwiseDisjoint id) ∧ + (∀ t ∈ P, MeasurableSet t) ∧ a < ∑ p ∈ P, ‖μ p‖ₑ := by + simp only [variation_apply, preVariation, ennrealToMeasure_apply hs, ennrealPreVariation_apply] + at ha ⊢ + obtain ⟨P, hP⟩ : ∃ P : Finpartition (⟨s, hs⟩ : Subtype MeasurableSet), + a < ∑ p ∈ P.parts, (fun x ↦ ‖μ x‖ₑ) p := + preVariation.exists_Finpartition_sum_gt (‖μ ·‖ₑ) _ ha + refine ⟨P.parts.map (Function.Embedding.subtype _), ?_, ?_, ?_, ?_⟩ + · simp only [mem_map, Function.Embedding.subtype_apply, Subtype.exists, exists_and_right, + exists_eq_right, forall_exists_index] + intro t ht h't + exact P.le h't + · intro i hi j hj hij + simp only [coe_map, Function.Embedding.subtype_apply, Set.mem_image, SetLike.mem_coe, + Subtype.exists, exists_and_right, exists_eq_right] at hi hj + rcases hi with ⟨h'i, i_mem⟩ + rcases hj with ⟨h'j, j_mem⟩ + exact (disjoint_subtype_iff (fun _ _ hs ht ↦ hs.inter ht) _).1 + (P.disjoint i_mem j_mem (by simpa using hij)) + · simp +contextual + · rwa [Finset.sum_map] + /-- Measure version of `preVariation.exists_Finpartition_sum_ge'`. -/ lemma exists_variation_le_add' (μ : VectorMeasure X V) {s : Set X} (hs : MeasurableSet s) {ε : ℝ≥0∞} (hε : 0 < ε) (hμ : μ.variation s ≠ ∞) : @@ -306,7 +331,8 @@ instance {x : X} {v : V} : IsFiniteMeasure (VectorMeasure.dirac x v).variation : simp only [variation_dirac, enorm_eq_nnnorm, Measure.coe_nnreal_smul] infer_instance -@[simp] lemma variation_toSignedMeasure {μ : Measure X} [IsFiniteMeasure μ] : +@[simp] lemma _root_.MeasureTheory.Measure.variation_toSignedMeasure + {μ : Measure X} [IsFiniteMeasure μ] : μ.toSignedMeasure.variation = μ := by apply le_antisymm · apply variation_le_of_forall_enorm_le (fun s hs ↦ ?_) @@ -315,6 +341,67 @@ instance {x : X} {v : V} : IsFiniteMeasure (VectorMeasure.dirac x v).variation : apply le_trans ?_ (enorm_measure_le_variation _ _) simp [Measure.toSignedMeasure_apply, hs, Measure.real, Real.enorm_eq_ofReal] +/-- For a signed measure, the variation is realized by the norm of the measure of a single set, up +to a factor of `2` and an arbitrarily small error. -/ +lemma _root_.MeasureTheory.SignedMeasure.exists_subset_lt_enorm_apply_of_lt_variation + (μ : SignedMeasure X) {s : Set X} (hs : MeasurableSet s) + {a : ℝ≥0∞} (ha : a < μ.variation s) : + ∃ t ⊆ s, MeasurableSet t ∧ a < 2 * ‖μ t‖ₑ := by + /- One may almost realize the variation through a partition into finitely many sets. + As their measures are real numbers, we can group together those of positive measure, and + also those of negative measure. This gives two measurable sets. Among these two, the one with the + largest measure in absolute value satisfies the result. -/ + obtain ⟨P, Ps, P_disj, P_meas, hP⟩ : ∃ (P : Finset (Set X)), (∀ t ∈ P, t ⊆ s) ∧ + ((P : Set (Set X)).PairwiseDisjoint id) ∧ + (∀ t ∈ P, MeasurableSet t) ∧ a < ∑ p ∈ P, ‖μ p‖ₑ := exists_lt_sum_of_lt_variation _ hs ha + have I : (∑ p ∈ P.filter (fun p ↦ 0 ≤ μ p), ‖μ p‖ₑ) = + ‖μ (⋃ p ∈ P.filter (fun p ↦ 0 ≤ μ p), p)‖ₑ := by + simp only [Real.norm_eq_abs, enorm_eq_nnnorm, + ← ENNReal.ofNNReal_finsetSum, ENNReal.coe_inj, ← NNReal.coe_inj, + NNReal.coe_sum, coe_nnnorm, Real.norm_eq_abs] + have A : ∑ x ∈ P with 0 ≤ μ x, |μ x| = μ (⋃ x ∈ P.filter (fun x ↦ 0 ≤ μ x), x) := calc + _ = ∑ x ∈ P with 0 ≤ μ x, μ x := by + apply Finset.sum_congr rfl (fun p hp ↦ ?_) + simp only [Finset.mem_filter] at hp + simp [hp] + _ = μ (⋃ x ∈ P.filter (fun x ↦ 0 ≤ μ x), x) := by + rw [of_biUnion_finset] + · apply P_disj.subset (by grind) + · grind + rw [A, abs_of_nonneg] + rw [← A] + exact Finset.sum_nonneg (fun p hp ↦ by positivity) + have J : (∑ p ∈ P.filter (fun p ↦ ¬ 0 ≤ μ p), ‖μ p‖ₑ) = + ‖μ (⋃ p ∈ P.filter (fun p ↦ ¬ 0 ≤ μ p), p)‖ₑ := by + simp only [not_le, enorm_eq_nnnorm, ← ENNReal.ofNNReal_finsetSum, + ENNReal.coe_inj, ← NNReal.coe_inj, NNReal.coe_sum, coe_nnnorm, Real.norm_eq_abs] + have A : ∑ x ∈ P with μ x < 0, |μ x| = - μ (⋃ x ∈ P.filter (fun x ↦ μ x < 0), x) := calc + ∑ x ∈ P with μ x < 0, |μ x| + _ = ∑ x ∈ P with μ x < 0, -μ x := by + refine Finset.sum_congr rfl (fun p hp ↦ ?_) + simp only [Finset.mem_filter] at hp + simp [hp.2.le] + _ = -μ (⋃ x ∈ P.filter (fun x ↦ μ x < 0), x) := by + rw [of_biUnion_finset] + · simp + · apply P_disj.subset (by grind) + · grind + rw [A, abs_of_nonpos] + rw [← neg_nonneg, ← A] + exact Finset.sum_nonneg (fun p hp ↦ by positivity) + simp_rw [two_mul] + rw [← Finset.sum_filter_add_sum_filter_not _ (fun p ↦ 0 ≤ μ p), I, J] at hP + rcases le_total (‖μ (⋃ p ∈ P.filter (fun p ↦ ¬ 0 ≤ μ p), p)‖ₑ) + (‖μ (⋃ p ∈ P.filter (fun p ↦ 0 ≤ μ p), p)‖ₑ) with h | h + · refine ⟨⋃ p ∈ P.filter (fun p ↦ 0 ≤ μ p), p, ?_, ?_, ?_⟩ + · simp; grind + · exact Finset.measurableSet_biUnion _ (by grind) + · exact hP.trans_le (by gcongr) + · refine ⟨⋃ p ∈ P.filter (fun p ↦ ¬ 0 ≤ μ p), p, ?_, ?_, ?_⟩ + · simp; grind + · exact Finset.measurableSet_biUnion _ (by grind) + · exact hP.trans_le (by gcongr) + end NormedAddCommGroup end MeasureTheory.VectorMeasure diff --git a/Mathlib/MeasureTheory/VectorMeasure/Variation/Semivariation.lean b/Mathlib/MeasureTheory/VectorMeasure/Variation/Semivariation.lean new file mode 100644 index 00000000000000..3fe6060781a2d4 --- /dev/null +++ b/Mathlib/MeasureTheory/VectorMeasure/Variation/Semivariation.lean @@ -0,0 +1,186 @@ +/- +Copyright (c) 2026 Sébastien Gouëzel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sébastien Gouëzel +-/ +module + +public import Mathlib.MeasureTheory.VectorMeasure.Variation.Basic + +import Mathlib.Analysis.Normed.Module.HahnBanach +import Mathlib.Analysis.Normed.Operator.NormedSpace + +/-! +# The semivariation of a vector measure + +The semivariation of a vector measure is the supremum of the variations of its push-forwards +to `ℝ` through all linear forms of norm at most `1`. The interest of this notion is that, in the +reals, any set has nonnegative or nonnegative measure, so that the variation is realized by +a subset (up to a factor of at most `2`). This property is inherited by the semivariation in +general: one has the inequalities +``` +‖μ s‖ₑ ≤ μ.semivariation s ≤ 2 sup_{t ⊆ s} ‖μ t‖ₑ +``` + +The notion of semivariation can in particular be used to show that any vector measure is bounded: +there exists `C < ∞` such that `‖μ s‖ ≤ C` for all `s`. + +## Main results + +* `μ.semivariation`: the semivariation of the vector measure `μ`. +* `exists_subset_lt_enorm_apply_of_lt_semivariation`: given `s`, there exists `t ⊆ s` such that + `μ.semivariation s ≤ 2 ‖μ t‖ₑ` up to an arbitrarily small error. +* `μ.bound`: the semivariation of `univ`, in `ℝ≥0`. It is finite by definition. +* `enorm_apply_le_bound`: the inequality `‖μ s‖ₑ ≤ μ.bound`, uniformly in `s`. + +## References + +* [J. Diestel and J.J. Uhl, Vector Measures][DiestelUhl1977] + +-/ + +public section + +open scoped ENNReal Function Topology NNReal +open Set Filter + +namespace MeasureTheory.VectorMeasure + +variable {X E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {mX : MeasurableSpace X} + {μ : VectorMeasure X E} {s t : Set X} + +/-- The semivariation of a vector measure, defined as the supremum of the variations +of the images of the vector measures under continuous linear forms of norm at most `1`. -/ +noncomputable def semivariation (μ : VectorMeasure X E) (s : Set X) : ℝ≥0∞ := + ⨆ ℓ ∈ {ℓ : StrongDual ℝ E | ‖ℓ‖ₑ ≤ 1}, (μ.mapRange (ℓ : E →+ ℝ) ℓ.continuous).variation s + +lemma semivariation_union_le : + μ.semivariation (s ∪ t) ≤ μ.semivariation s + μ.semivariation t := by + simp only [semivariation, iSup_le_iff] + intro ℓ hℓ + apply (measure_union_le _ _).trans + gcongr <;> apply le_biSup _ hℓ + +lemma semivariation_mono (hst : s ⊆ t) : μ.semivariation s ≤ μ.semivariation t := by + simp only [semivariation, iSup_le_iff] + intro ℓ hℓ + apply (measure_mono hst).trans + apply le_biSup _ hℓ + +lemma semivariation_le_variation : μ.semivariation s ≤ μ.variation s := by + simp only [semivariation, iSup_le_iff] + intro ℓ hℓ + suffices (μ.mapRange (ℓ : E →+ ℝ) ℓ.continuous).variation ≤ μ.variation from this s + apply variation_le_of_forall_enorm_le (fun t ht ↦ ?_) + simp only [mapRange_apply, AddMonoidHom.coe_coe] + apply le_trans ?_ (enorm_measure_le_variation _ _) + exact (ContinuousLinearMap.le_opNorm_enorm _ _).trans (mul_le_of_le_one_left (by positivity) hℓ) + +lemma enorm_apply_le_semivariation : ‖μ s‖ₑ ≤ μ.semivariation s := by + by_cases hs : MeasurableSet s; swap + · simp [not_measurable, hs] + obtain ⟨ℓ, ℓ_norm, hℓ⟩ : ∃ ℓ : StrongDual ℝ E, ‖ℓ‖ ≤ 1 ∧ ℓ (μ s) = ‖μ s‖ := + exists_dual_vector'' _ _ + have h'ℓ : ℓ ∈ {ℓ : StrongDual ℝ E | ‖ℓ‖ₑ ≤ 1} := by + simp [enorm_eq_nnnorm, ← NNReal.coe_le_one, ℓ_norm] + calc ‖μ s‖ₑ + _ = ‖(μ.mapRange (ℓ : E →+ ℝ) ℓ.continuous) s‖ₑ := by simp [← ofReal_norm, hℓ] + _ ≤ (μ.mapRange (ℓ : E →+ ℝ) ℓ.continuous).variation s := enorm_measure_le_variation _ _ + _ ≤ μ.semivariation s := by apply le_biSup _ h'ℓ + +lemma enorm_apply_le_semivariation_of_subset (hst : s ⊆ t) : + ‖μ s‖ₑ ≤ μ.semivariation t := + enorm_apply_le_semivariation.trans (semivariation_mono hst) + +lemma exists_subset_lt_enorm_apply_of_lt_semivariation (hs : MeasurableSet s) + {a : ℝ≥0∞} (ha : a < μ.semivariation s) : + ∃ t ⊆ s, MeasurableSet t ∧ a < 2 * ‖μ t‖ₑ := by + obtain ⟨ℓ, hℓ, h'ℓ⟩ : ∃ ℓ ∈ {ℓ : StrongDual ℝ E | ‖ℓ‖ₑ ≤ 1}, + a < (μ.mapRange (ℓ : E →+ ℝ) ℓ.continuous).variation s := lt_biSup_iff.1 ha + obtain ⟨t, ts, t_meas, ht⟩ : + ∃ t ⊆ s, MeasurableSet t ∧ a < 2 * ‖μ.mapRange (ℓ : E →+ ℝ) ℓ.continuous t‖ₑ := + SignedMeasure.exists_subset_lt_enorm_apply_of_lt_variation _ hs h'ℓ + refine ⟨t, ts, t_meas, ht.trans_le ?_⟩ + gcongr + exact (ContinuousLinearMap.le_opNorm_enorm _ _).trans (mul_le_of_le_one_left (by positivity) hℓ) + +private lemma exists_one_le_enorm_apply_of_semivariation_eq_top + (hs : MeasurableSet s) (h's : μ.semivariation s = ∞) : + ∃ t, MeasurableSet t ∧ t ⊆ s ∧ μ.semivariation t = ∞ ∧ 1 ≤ ‖μ (s \ t)‖ₑ := by + obtain ⟨t, ts, t_meas, ht⟩ : ∃ t ⊆ s, MeasurableSet t ∧ 2 * ‖μ s‖ₑ + 2 < 2 * ‖μ t‖ₑ := by + apply exists_subset_lt_enorm_apply_of_lt_semivariation hs + rw [h's] + finiteness + have h't : 1 + ‖μ s‖ₑ ≤ ‖μ t‖ₑ := by + apply (ENNReal.mul_le_mul_iff_right (a := 2) (by simp) (by simp)).1 + rw [mul_add, add_comm, mul_one] + exact ht.le + have I : ∞ ≤ μ.semivariation t + μ.semivariation (s \ t) := by + rw [← h's] + apply le_trans (semivariation_mono (by simp)) semivariation_union_le + simp only [top_le_iff, ENNReal.add_eq_top] at I + rcases I with hI | hI + · refine ⟨t, t_meas, ts, hI, ?_⟩ + have : 1 + ‖μ s‖ₑ ≤ ‖μ (s \ t)‖ₑ + ‖μ s‖ₑ := by + apply h't.trans + have : μ t = μ s - μ (s \ t) := by rw [← of_add_of_sdiff t_meas hs ts]; abel + rw [this, add_comm] + exact enorm_sub_le + rwa [ENNReal.add_le_add_iff_right (by simp)] at this + · refine ⟨s \ t, hs.diff t_meas, sdiff_subset, hI, ?_⟩ + simp only [_root_.sdiff_sdiff_right_self, le_eq_subset, ts, inf_of_le_right] + exact le_trans (by simp) h't + +private lemma semivariation_univ_lt_top : μ.semivariation univ < ∞ := by + apply Ne.lt_top (fun h ↦ ?_) + have A (s : Set X) (hs : MeasurableSet s) (h's : μ.semivariation s = ∞) : + ∃ t, MeasurableSet t ∧ t ⊆ s ∧ μ.semivariation t = ∞ ∧ 1 ≤ ‖μ (s \ t)‖ₑ := + exists_one_le_enorm_apply_of_semivariation_eq_top hs h's + choose! t t_meas t_subs t_var ht using A + let s n := t^[n] univ + have hs n : MeasurableSet (s n) ∧ μ.semivariation (s n) = ∞ := by + induction n with + | zero => simp [s, h] + | succ n ih => + simp only [Function.iterate_succ', Function.comp_apply, s] + exact ⟨t_meas _ ih.1 ih.2, t_var _ ih.1 ih.2⟩ + let u n := s n \ s (n + 1) + have hu n : 1 ≤ ‖μ (u n)‖ₑ := by + simp only [Function.iterate_succ', Function.comp_apply, u, s] + exact ht _ (hs n).1 (hs n).2 + have s_anti : Antitone s := by + apply antitone_nat_of_succ_le (fun n ↦ ?_) + simp only [Function.iterate_succ', Function.comp_apply, s] + apply t_subs _ (hs n).1 (hs n).2 + have u_disj : Pairwise (Disjoint on u) := by + apply (pairwise_disjoint_on _).2 (fun m n hmn ↦ ?_) + have : Disjoint (u m) (s (m + 1)) := by simp [u, disjoint_sdiff_left] + apply this.mono_right + simp only [sdiff_le_iff, sup_eq_union, le_eq_subset, u] + exact Subset.trans (s_anti (by grind)) subset_union_right + have : HasSum (fun i => μ (u i)) (μ (⋃ i, u i)) := + hasSum_of_disjoint_iUnion (fun n ↦ (hs n).1.diff (hs (n + 1)).1) u_disj + have : Tendsto (fun x ↦ ‖μ (u x)‖ₑ) atTop (𝓝 0) := + tendsto_zero_iff_enorm_tendsto_zero.1 this.summable.tendsto_atTop_zero + obtain ⟨n, hn⟩ : ∃ n, ‖μ (u n)‖ₑ < 1 := ((tendsto_order.1 this).2 _ zero_lt_one).exists + order [hu n] + +/-- A constant bounding the norm of `μ s` for any set `s`. -/ +protected noncomputable def bound : ℝ≥0 := (μ.semivariation univ).toNNReal + +lemma semivariation_apply_le_bound : μ.semivariation s ≤ μ.bound := by + apply (semivariation_mono (subset_univ _)).trans_eq + simp only [VectorMeasure.bound] + rw [ENNReal.coe_toNNReal semivariation_univ_lt_top.ne] + +lemma enorm_apply_le_bound : ‖μ s‖ₑ ≤ μ.bound := + (enorm_apply_le_semivariation).trans semivariation_apply_le_bound + +lemma nnnorm_apply_le_bound : ‖μ s‖₊ ≤ μ.bound := by + rw [← ENNReal.coe_le_coe, ← enorm_eq_nnnorm] + exact enorm_apply_le_bound + +lemma norm_apply_le_bound : ‖μ s‖ ≤ μ.bound := by + simpa [← coe_nnnorm] using nnnorm_apply_le_bound + +end MeasureTheory.VectorMeasure diff --git a/Mathlib/MeasureTheory/VectorMeasure/WithDensityVec.lean b/Mathlib/MeasureTheory/VectorMeasure/WithDensityVec.lean new file mode 100644 index 00000000000000..02c52dbb6d66ef --- /dev/null +++ b/Mathlib/MeasureTheory/VectorMeasure/WithDensityVec.lean @@ -0,0 +1,390 @@ +/- +Copyright (c) 2026 Sébastien Gouëzel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sébastien Gouëzel +-/ +module + +public import Mathlib.MeasureTheory.VectorMeasure.SetIntegral +public import Mathlib.MeasureTheory.VectorMeasure.WithDensity + +/-! +# Vector measure with density with respect to a vector measure + +-/ + +open Set Filter +open scoped Topology ENNReal + +@[expose] public section + +namespace MeasureTheory.VectorMeasure + +local infixr:25 " →ₛ " => SimpleFunc + +variable {X E F G : Type*} {mX : MeasurableSpace X} + [NormedAddCommGroup E] [NormedSpace ℝ E] + [NormedAddCommGroup F] [NormedSpace ℝ F] + [NormedAddCommGroup G] [NormedSpace ℝ G] + {μ : VectorMeasure X F} {f g : X → E} {B : E →L[ℝ] F →L[ℝ] G} {s : Set X} + +open scoped Classical in +/-- The vector measure with density `f` with respect to a vector measure `μ`, associating to a +measurable set the mass `∫ᵛ x in s, f x ∂[B; μ]`. +If `f` is not integrable, we use the junk value `0`. -/ +noncomputable def withDensity (μ : VectorMeasure X F) (f : X → E) (B : E →L[ℝ] F →L[ℝ] G) : + VectorMeasure X G := + if h : μ.Integrable f then + { measureOf' s := ∫ᵛ x in s, f x ∂[B; μ] + empty' := by simp + not_measurable' s hs := setIntegral_eq_zero_of_not_measurableSet hs + m_iUnion' s s_meas s_disj := hasSum_setIntegral_iUnion s_meas s_disj h.integrableOn } + else 0 + +lemma withDensity_apply (hf : μ.Integrable f) : + μ.withDensity f B s = ∫ᵛ x in s, f x ∂[B; μ] := by + simp [withDensity, hf] + +lemma withDensity_apply_univ : μ.withDensity f B univ = ∫ᵛ x, f x ∂[B; μ] := by + by_cases hf : μ.Integrable f + · simp [withDensity_apply hf] + · simp [withDensity, hf, integral_undef] + +@[simp] +lemma withDensity_zero_vectorMeasure : (0 : VectorMeasure X F).withDensity f B = 0 := by + ext s hs + simp [withDensity_apply] + +@[to_fun (attr := simp) withDensity_fun_zero] +lemma withDensity_zero : μ.withDensity 0 B = 0 := by + ext s hs + simp [withDensity_apply] + +lemma withDensity_congr (h : f =ᵐ[μ.variation] g) : + μ.withDensity f B = μ.withDensity g B := by + by_cases hf : μ.Integrable f + · simp only [withDensity, hf, ↓reduceDIte, Integrable.congr hf h, mk.injEq] + ext s + apply setIntegral_congr_ae + filter_upwards [h] with x hx xs using hx + · have : ¬(μ.Integrable g) := by simpa [← integrable_congr h] using hf + simp [withDensity, hf, this] + +lemma restrict_withDensity (hf : μ.Integrable f) : + (μ.withDensity f B).restrict s = (μ.restrict s).withDensity f B := by + by_cases hs : MeasurableSet s; swap + · simp [restrict_not_measurable _ hs] + · ext t ht + simp only [hs, ht, restrict_apply] + rw [withDensity_apply hf, withDensity_apply hf.restrict, restrict_restrict _ ht hs] + +lemma variation_WithDensity_le : + (μ.withDensity f B).variation ≤ (μ.transpose B).variation.withDensity (fun x ↦ ‖f x‖ₑ) := by + by_cases hf : μ.Integrable f + · apply variation_le_of_forall_enorm_le (fun s hs ↦ ?_) + rw [withDensity_apply hf, MeasureTheory.withDensity_apply _ hs] + apply enorm_setIntegral_le_lintegral_enorm_transpose + · simp [withDensity, hf, Measure.zero_le ] + +/-- If `‖B x y‖ = ‖B · y‖ * ‖x‖` for all `x, y`, then the variation of a vector measure with +density `f` wrt `μ` is the measure with density `‖f‖ₑ` with respect to the variation of `μ`. + +The condition on `B` is necessary: for a counterexample without it, let `B` be the scalar +product in `ℝ²` and `f x` everywhere horizontal and `μ s` everywhere vertical. +Then `μ.withDensity f B = 0` so its variation is zero, while the integral of `‖f‖ₑ` is not. + +See also `variation_withDensity` under the very common condition `‖B x y‖ = ‖x‖ ‖y‖`. +-/ +lemma variation_withDensity' [CompleteSpace G] + (hf : μ.Integrable f) (hB : ∀ x y, ‖B x y‖₊ = ‖B.flip y‖₊ * ‖x‖₊) : + (μ.withDensity f B).variation = (μ.transpose B).variation.withDensity (fun x ↦ ‖f x‖ₑ) := by + apply le_antisymm variation_WithDensity_le + apply Measure.le_iff.2 (fun s hs ↦ ?_) + /- For the nontrivial direction, we have to show that for each measurable set `s`, + `∫⁻ (a : X) in s, ‖f a‖ₑ ∂(μ.transpose B).variation ≤ (μ.withDensity f B).variation s`. + As the variation is a supremum over finite partitions, we need to exhibit a partition. For this, + we approximate `f` by a simple function `g`. Then the left term is approximately + `∑ i, ‖g i‖ₑ * (μ.transpose B).variation (g ⁻¹' {i})`. + By definition, the variation of `g ⁻¹' {i}` is close to a sum `∑ j, ‖(μ.transpose B) Pᵢⱼ‖ₑ` over + a partition `Pᵢⱼ` of `g ⁻¹' {i}`. Putting all these together, one gets the desired + partition of `s`, for which `∫⁻ a in s, ‖f a‖ₑ ∂(μ.transpose B).variation` is close to + `∑ i j, ‖∫ x in Pᵢⱼ, f x ∂[B; μ]‖ₑ`, i.e., `∑ i j, ‖(μ.withDensity f B) Pᵢⱼ‖ₑ`. The latter sum + is bounded by `(μ.withDensity f B).variation s` as desired. -/ + rw [MeasureTheory.withDensity_apply _ hs] + apply ENNReal.le_of_forall_pos_le_add + rintro ε εpos - + let δ := ε / 3 + have δpos : 0 < δ := div_pos εpos (by norm_num) + -- first step: approximate `f` by a simple function `g`. + obtain ⟨g, hg, gmem⟩ : ∃ (g : X →ₛ E), eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ δ + ∧ MemLp (⇑g) 1 μ.variation := by + obtain ⟨ρ, ρpos, hδ⟩ : ∃ ρ > 0, ‖B‖₊ * ρ ≤ δ := by + rcases eq_or_ne (‖B‖₊) 0 with hB | hB + · exact ⟨1, zero_lt_one, by simp [hB]⟩ + · refine ⟨‖B‖₊ ⁻¹ * δ, by positivity, ?_⟩ + rw [← mul_assoc] + apply mul_le_of_le_one_left (by positivity) mul_inv_le_one + obtain ⟨g, h'g, gmem⟩ : ∃ (g : X →ₛ E), eLpNorm (f - ⇑g) 1 μ.variation < ρ + ∧ MemLp (⇑g) 1 μ.variation := + (memLp_one_iff_integrable.2 hf).exists_simpleFunc_eLpNorm_sub_lt (by simp) + (by simpa using ρpos.ne') + refine ⟨g, ?_, gmem⟩ + grw [variation_transpose_le] + rw [eLpNorm_smul_measure_of_ne_top' (by simp)] + grw [h'g.le] + simp only [ENNReal.toReal_one, inv_one, NNReal.rpow_one, ENNReal.smul_def, smul_eq_mul] + exact_mod_cast hδ + -- the integral of `‖f‖ₑ` is approximated up to `δ` by that of `‖g‖ₑ`. + have I1 : ∫⁻ a in s, ‖f a‖ₑ ∂(μ.transpose B).variation + ≤ ∫⁻ a in s, ‖g a‖ₑ ∂(μ.transpose B).variation + δ := calc + _ ≤ ∫⁻ a in s, ‖f a - g a‖ₑ + ‖g a‖ₑ ∂(μ.transpose B).variation := by + gcongr with a + nth_rw 1 [show f a = (f a - g a) + g a by abel] + exact enorm_add_le (f a - g a) (g a) + _ = ∫⁻ a in s, ‖g a‖ₑ ∂(μ.transpose B).variation + + ∫⁻ a in s, ‖f a - g a‖ₑ ∂(μ.transpose B).variation := by + rw [lintegral_add_right, add_comm] + exact g.stronglyMeasurable.enorm + _ ≤ ∫⁻ a in s, ‖g a‖ₑ ∂(μ.transpose B).variation + + ∫⁻ a, ‖f a - g a‖ₑ ∂(μ.transpose B).variation := by + gcongr + exact Measure.restrict_le_self + _ ≤ ∫⁻ a in s, ‖g a‖ₑ ∂(μ.transpose B).variation + δ := by + rw [eLpNorm_one_eq_lintegral_enorm] at hg + gcongr + exact hg + -- the integral of `‖g‖ₑ` can be rewritten as a weighted sum of measures, as `g` is a simple + -- function. + have I2 : ∫⁻ a in s, ‖g a‖ₑ ∂(μ.transpose B).variation = + ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (g ⁻¹' {i}) := calc + _ = (g.map (‖·‖ₑ)).lintegral ((μ.transpose B).variation.restrict s) := + SimpleFunc.lintegral_eq_lintegral _ _ + _ = ∑ i ∈ g.range, ‖i‖ₑ * (μ.transpose B).variation.restrict s (g ⁻¹' {i}) := + SimpleFunc.map_lintegral _ _ + _ = ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (g ⁻¹' {i}) := by + simp_rw [variation_restrict hs] + -- For each `i`, choose a partition `P i` of `g ⁻¹' {i}` such that the sum of the enorms + -- of their measures approximates well enough the variation, by definition of the variation. + obtain ⟨ρ,ρpos, hρ⟩ : ∃ ρ > 0, ∑ i ∈ g.range, ‖i‖ₑ * ρ ≤ δ := by + refine ⟨δ * (∑ i ∈ g.range, ‖i‖ₑ)⁻¹, by simp [δpos], ?_⟩ + grw [← Finset.sum_mul, mul_comm (δ : ℝ≥0∞), ← mul_assoc, ENNReal.mul_inv_le_one, one_mul] + have C i : ∃ (P : Finset (Set X)), (∀ t ∈ P, t ⊆ g ⁻¹' {i}) + ∧ ((P : Set (Set X)).PairwiseDisjoint id) ∧ + (∀ t ∈ P, MeasurableSet t) ∧ + ‖i‖ₑ * ((μ.transpose B).restrict s).variation (g ⁻¹' {i}) ≤ + ‖i‖ₑ * (∑ p ∈ P, ‖(μ.transpose B).restrict s p‖ₑ + ρ) := by + rcases eq_or_ne i 0 with rfl | hi + · exact ⟨∅, by simp⟩ + suffices ∃ (P : Finset (Set X)), (∀ t ∈ P, t ⊆ g ⁻¹' {i}) + ∧ ((P : Set (Set X)).PairwiseDisjoint id) ∧ (∀ t ∈ P, MeasurableSet t) ∧ + ((μ.transpose B).restrict s).variation (g ⁻¹' {i}) ≤ + (∑ p ∈ P, ‖(μ.transpose B).restrict s p‖ₑ + ρ) by + obtain ⟨P, hP, h'P, h''P, h'''P⟩ := this + exact ⟨P, hP, h'P, h''P, by gcongr⟩ + apply exists_variation_le_add' _ (g.measurableSet_fiber i) ρpos + rw [variation_restrict hs] + have : MemLp (⇑g) 1 (μ.transpose B).variation := + gmem.of_measure_le_smul (c := ‖B‖₊) (by simp) (variation_transpose_le _ _) + exact (g.integrable_iff.1 (memLp_one_iff_integrable.1 this).restrict i hi).ne + choose P Pg Pdisj Pmeas hP using C + -- rewrite everything in terms of the global partition made by putting together the `Pᵢ`, + -- and register that the resulting error is bounded by `δ`. + have I3 : ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (g ⁻¹' {i}) ≤ + ∑ i ∈ g.range.sigma P, ‖i.1‖ₑ * ‖(μ.transpose B).restrict s i.2‖ₑ + δ := calc + ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (g ⁻¹' {i}) + _ ≤ ∑ i ∈ g.range, ‖i‖ₑ * ((∑ p ∈ P i, ‖(μ.transpose B).restrict s p‖ₑ) + ρ) := by + gcongr 1 with i hi + exact hP i + _ ≤ ∑ i ∈ g.range, ∑ p ∈ P i, ‖i‖ₑ * ‖(μ.transpose B).restrict s p‖ₑ + δ := by + simp_rw [mul_add, Finset.sum_add_distrib, Finset.mul_sum] + gcongr + _ = ∑ i ∈ g.range.sigma P, ‖i.1‖ₑ * ‖(μ.transpose B).restrict s i.2‖ₑ + δ := by + rw [Finset.sum_sigma'] + -- in the above sum, replace the values of `g` by `f`, as these two functions are close + -- in `L^1` norm. + have I4 : ∑ i ∈ g.range.sigma P, ‖i.1‖ₑ * ‖(μ.transpose B).restrict s i.2‖ₑ + ≤ ∑ i ∈ g.range.sigma P, ‖∫ᵛ x in i.2, f x ∂[B; μ.restrict s]‖ₑ + δ := calc + ∑ i ∈ g.range.sigma P, ‖i.1‖ₑ * ‖(μ.transpose B).restrict s i.2‖ₑ + _ = ∑ i ∈ g.range.sigma P, ‖∫ᵛ x in i.2, i.1 ∂[B; μ.restrict s]‖ₑ := by + congr! with ⟨i, p⟩ hi + rcases eq_or_ne i 0 with rfl | h'i + · simp + simp only [Finset.mem_sigma] at hi + have pmeas : MeasurableSet p := Pmeas i _ hi.2 + have : IsFiniteMeasure ((μ.restrict s).variation.restrict p) := by + constructor + rw [variation_restrict hs, Measure.restrict_restrict pmeas, + MeasureTheory.Measure.restrict_apply_univ] + apply lt_of_le_of_lt ?_ (g.integrable_iff.1 (memLp_one_iff_integrable.1 gmem) i h'i) + exact measure_mono (inter_subset_left.trans (Pg i _ hi.2)) + rw [setIntegral_const, restrict_apply _ hs pmeas, restrict_apply _ hs pmeas] + simp [transpose, hB, enorm_eq_nnnorm, mul_comm] + _ = ∑ i ∈ g.range.sigma P, ‖∫ᵛ x in i.2, g x ∂[B; μ.restrict s]‖ₑ := by + congr! 2 with ⟨i, p⟩ hi + simp only [Finset.mem_sigma] at hi + apply setIntegral_congr_ae + filter_upwards with x hx using (Pg i _ hi.2 hx).symm + _ = ∑ i ∈ g.range.sigma P, ‖∫ᵛ x in i.2, (g x - f x) + f x ∂[B; μ.restrict s]‖ₑ := by simp + _ = ∑ i ∈ g.range.sigma P, ‖∫ᵛ x in i.2, (g x - f x) ∂[B; μ.restrict s] + + ∫ᵛ x in i.2, f x ∂[B; μ.restrict s]‖ₑ := by + congr! with i hi + rw [integral_fun_add] + · apply Integrable.restrict + apply Integrable.restrict + apply Integrable.sub (memLp_one_iff_integrable.1 gmem) hf + · apply hf.restrict.restrict + _ ≤ ∑ i ∈ g.range.sigma P, ‖∫ᵛ x in i.2, (g x - f x) ∂[B; μ.restrict s]‖ₑ + + ∑ i ∈ g.range.sigma P, ‖∫ᵛ x in i.2, f x ∂[B; μ.restrict s]‖ₑ := by + rw [← Finset.sum_add_distrib] + gcongr with i hi + apply enorm_add_le + _ ≤ ∑ i ∈ g.range.sigma P, ∫⁻ x in i.2, ‖g x - f x‖ₑ ∂(μ.transpose B).variation + + ∑ i ∈ g.range.sigma P, ‖∫ᵛ x in i.2, f x ∂[B; μ.restrict s]‖ₑ := by + gcongr with i hi + grw [enorm_setIntegral_le_lintegral_enorm_transpose] + apply lintegral_mono' _ le_rfl + apply Measure.restrict_mono le_rfl + rw [transpose_restrict, variation_restrict hs] + apply Measure.restrict_le_self + _ = ∫⁻ x in (⋃ i ∈ g.range.sigma P, i.2), ‖g x - f x‖ₑ ∂(μ.transpose B).variation + + ∑ i ∈ g.range.sigma P, ‖∫ᵛ x in i.2, f x ∂[B; μ.restrict s]‖ₑ := by + rw [lintegral_biUnion_finset] + · rintro ⟨i, p⟩ hi ⟨j, q⟩ hj hijpq + simp only [Finset.coe_sigma, SimpleFunc.coe_range, mem_sigma_iff, mem_range, + SetLike.mem_coe] at hi hj + rcases eq_or_ne i j with rfl | hij + · simp only [ne_eq, Sigma.mk.injEq, heq_eq_eq, true_and] at hijpq + exact Pdisj i hi.2 hj.2 hijpq + · have : Disjoint (g ⁻¹' {i}) (g ⁻¹' {j}) := by grind + exact this.mono (Pg i p hi.2) (Pg j q hj.2) + · rintro ⟨i, p⟩ hip + simp only [Finset.mem_sigma, SimpleFunc.mem_range, mem_range] at hip + exact Pmeas i p hip.2 + _ ≤ ∑ i ∈ g.range.sigma P, ‖∫ᵛ x in i.2, f x ∂[B; μ.restrict s]‖ₑ + + ∫⁻ x, ‖g x - f x‖ₑ ∂(μ.transpose B).variation := by + rw [add_comm] + gcongr + apply Measure.restrict_le_self + _ ≤ ∑ i ∈ g.range.sigma P, ‖∫ᵛ x in i.2, f x ∂[B; μ.restrict s]‖ₑ + δ := by + gcongr + simp_rw [enorm_sub_rev, ← eLpNorm_one_eq_lintegral_enorm] + exact hg + -- register that the sum of the enorms of the integrals of `f` over the pieces `Pᵢⱼ` of the + -- partition is bounded by the variation of `μ.withDensity f B`, by definition of the variation. + have I5 : ∑ i ∈ g.range.sigma P, ‖∫ᵛ x in i.2, f x ∂[B; μ.restrict s]‖ₑ + ≤ (μ.withDensity f B).variation s := by + let Q : Finset (Set X) := (g.range.sigma P).image (fun p ↦ p.2 ∩ s) + calc ∑ i ∈ g.range.sigma P, ‖∫ᵛ x in i.2, f x ∂[B; μ.restrict s]‖ₑ + _ = ∑ j ∈ Q, ‖∫ᵛ x in j, f x ∂[B; μ]‖ₑ := by + simp only [Q] + rw [Finset.sum_image_of_pairwise_eq_zero]; swap + · rintro ⟨i, p⟩ hi ⟨j, q⟩ hj hijpq h'ij + simp only [Finset.coe_sigma, SimpleFunc.coe_range, mem_sigma_iff, mem_range, + SetLike.mem_coe] at hi hj + suffices H : Disjoint p q by + have : Disjoint (p ∩ s) (q ∩ s) := H.mono inter_subset_left inter_subset_left + rw [← h'ij, disjoint_self] at this + simp [this] + rcases eq_or_ne i j with rfl | hij + · simp only [ne_eq, Sigma.mk.injEq, heq_eq_eq, true_and] at hijpq + exact Pdisj i hi.2 hj.2 hijpq + · have : Disjoint (g ⁻¹' {i}) (g ⁻¹' {j}) := by grind + exact this.mono (Pg i p hi.2) (Pg j q hj.2) + apply Finset.sum_congr rfl + rintro ⟨i, p⟩ hi + simp only [Finset.mem_sigma, SimpleFunc.mem_range, mem_range] at hi + rw [restrict_restrict _ (Pmeas i p hi.2) hs] + _ = ∑ j ∈ Q, ‖μ.withDensity f B j‖ₑ := + Finset.sum_congr rfl (fun t ht ↦ by rw [withDensity_apply hf]) + _ ≤ (μ.withDensity f B).variation s := by + apply le_variation _ hs + · intro t ht + simp only [Finset.mem_image, Finset.mem_sigma, SimpleFunc.mem_range, mem_range, + Sigma.exists, ↓existsAndEq, true_and, exists_and_right, Q] at ht + rcases ht with ⟨p, -, rfl⟩ + exact inter_subset_right + · intro t ht u hu htu + simp only [Finset.coe_image, Finset.coe_sigma, SimpleFunc.coe_range, mem_image, + mem_sigma_iff, mem_range, SetLike.mem_coe, Sigma.exists, ↓existsAndEq, true_and, + exists_and_right, Q] at ht hu + rcases ht with ⟨p, ⟨i, hi⟩, rfl⟩ + rcases hu with ⟨q, ⟨j, hj⟩, rfl⟩ + have hpq : p ≠ q := by grind only + suffices H : Disjoint p q from H.mono inter_subset_left inter_subset_left + rcases eq_or_ne (g i) (g j) with hij | hij + · rw [← hij] at hj + exact Pdisj (g i) hi hj hpq + · have : Disjoint (g ⁻¹' {g i}) (g ⁻¹' {g j}) := by grind + exact this.mono (Pg (g i) p hi) (Pg (g j) q hj) + -- finally, put together the above inequalities, and argue that the overall error `3δ` is + -- bounded by `ε` by design. + calc ∫⁻ (a : X) in s, ‖f a‖ₑ ∂(μ.transpose B).variation + _ ≤ ∫⁻ a in s, ‖g a‖ₑ ∂(μ.transpose B).variation + δ := I1 + _ = ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (g ⁻¹' {i}) + δ := by rw [I2] + _ ≤ (∑ i ∈ g.range.sigma P, ‖i.1‖ₑ * ‖(μ.transpose B).restrict s i.2‖ₑ + δ) + δ := by gcongr + _ ≤ ((∑ i ∈ g.range.sigma P, ‖∫ᵛ x in i.2, f x ∂[B; μ.restrict s]‖ₑ + δ) + δ) + δ := by gcongr + _ = (∑ i ∈ g.range.sigma P, ‖∫ᵛ x in i.2, f x ∂[B; μ.restrict s]‖ₑ) + 3 * δ := by ring + _ ≤ (μ.withDensity f B).variation s + 3 * δ := by gcongr + _ ≤ (μ.withDensity f B).variation s + ε := by + simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, ENNReal.coe_div, ENNReal.coe_ofNat, δ] + rw [ENNReal.mul_div_cancel (by simp) (by simp)] + +/-- If `‖B x y‖ = ‖x‖ * ‖y‖` for all `x, y`, then the variation of a vector measure with +density `f` wrt `μ` is the measure with density `‖f‖ₑ` with respect to the variation of `μ`. + +The condition on `B` is necessary: for a counterexample without it, let `B` be the scalar +product in `ℝ²` and `f x` everywhere horizontal and `μ s` everywhere vertical. +Then `μ.withDensity f B = 0` so its variation is zero, while the integral of `‖f‖ₑ` is not. +-/ +lemma variation_withDensity [CompleteSpace G] + (hf : μ.Integrable f) (hB : ∀ x y, ‖B x y‖₊ = ‖x‖₊ * ‖y‖₊) : + (μ.withDensity f B).variation = (μ.transpose B).variation.withDensity (fun x ↦ ‖f x‖ₑ) := by + apply variation_withDensity' hf (fun x y ↦ ?_) + refine le_antisymm (ContinuousLinearMap.le_opNorm (B.flip y) x) ?_ + rw [hB, mul_comm] + gcongr + apply ContinuousLinearMap.opNNNorm_le_bound + simp [hB, mul_comm] + +/-- The variation of a vecture measure with density `f` with respect to a positive measure `μ` +is the measure with density `‖f‖ₑ` with respect to `μ`. -/ +lemma _root_.MeasureTheory.Measure.variation_withDensityᵥ [CompleteSpace E] + {μ : Measure X} {f : X → E} (hf : Integrable f μ) : + (μ.withDensityᵥ f).variation = μ.withDensity (fun x ↦ ‖f x‖ₑ) := by + /- We deduce this statement from the statement `variation_withDensity` for vector measures + with density. For this, we write `μ.withDensityᵥ f` as the vector measure with density `f / ‖f‖` + with respect to the measure `μ.withDensity ‖f‖` interpreted as a signed measure. -/ + rcases subsingleton_or_nontrivial E with hE | hE + · simp [show f = 0 from Subsingleton.elim _ _] + have : IsFiniteMeasure (μ.withDensity fun x ↦ ‖f x‖ₑ) := ⟨by simpa using! hf.2⟩ + have I : (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure.Integrable (fun x ↦ ‖f x‖⁻¹ • f x) := by + simp only [VectorMeasure.Integrable, Measure.variation_toSignedMeasure] + apply Integrable.of_bound (C := 1) + · apply AEStronglyMeasurable.mono_ac (withDensity_absolutelyContinuous _ _) + exact hf.aestronglyMeasurable.norm.inv₀.smul hf.aestronglyMeasurable + · filter_upwards with x using by simp [norm_smul, inv_mul_le_one] + have : μ.withDensityᵥ f = (μ.withDensity (‖f ·‖ₑ)).toSignedMeasure.withDensity + (fun x ↦ ‖f x‖⁻¹ • f x) (ContinuousLinearMap.lsmul ℝ ℝ).flip := by + ext s hs + rw [withDensityᵥ_apply hf hs, withDensity_apply I, setIntegral_toSignedMeasure hs, + setIntegral_withDensity_eq_setIntegral_toReal_smul₀ _ _ _ hs]; rotate_left + · exact hf.aestronglyMeasurable.restrict.enorm + · filter_upwards with x using by simp + congr with x + rcases eq_or_ne (f x) 0 with hx | hx + · simp [hx] + simp only [toReal_enorm, smul_smul] + rw [mul_inv_cancel₀, one_smul] + simpa using hx + rw [this, variation_withDensity I (by simp [nnnorm_smul, mul_comm]), + variation_transpose_eq _ _ (by simp [nnnorm_smul, mul_comm]), Measure.variation_toSignedMeasure, + ← withDensity_mul₀ hf.aestronglyMeasurable.enorm]; swap + · exact (hf.aestronglyMeasurable.norm.inv₀.smul hf.aestronglyMeasurable).enorm + congr with x + rcases eq_or_ne (f x) 0 with hx | hx + · simp [hx] + have h'x : ‖f x‖ ≠ 0 := by simp [hx] + simp only [enorm_smul, Pi.mul_apply, ne_eq, h'x, not_false_eq_true, enorm_inv, enorm_norm] + rw [ENNReal.inv_mul_cancel (by simpa using hx) (by simp), mul_one] + +end MeasureTheory.VectorMeasure diff --git a/Mathlib/Topology/UniformSpace/Dini.lean b/Mathlib/Topology/UniformSpace/Dini.lean index 34c07a3509d4fb..e9280ee5911be1 100644 --- a/Mathlib/Topology/UniformSpace/Dini.lean +++ b/Mathlib/Topology/UniformSpace/Dini.lean @@ -56,7 +56,7 @@ lemma tendstoLocallyUniformly_of_forall_tendsto refine (atTop : Filter ι).eq_or_neBot.elim (fun h ↦ ?eq_bot) (fun _ ↦ ?_) case eq_bot => simp [h, tendstoLocallyUniformly_iff_forall_tendsto] have F_le_f (x : α) (n : ι) : F n x ≤ f x := by - refine ge_of_tendsto (h_tendsto x) ?_ + refine _root_.ge_of_tendsto (h_tendsto x) ?_ filter_upwards [Ici_mem_atTop n] with m hnm exact hF_mono hnm x simp_rw [Metric.tendstoLocallyUniformly_iff, dist_eq_norm'] diff --git a/docs/references.bib b/docs/references.bib index 96ac2dcb039f3c..355c684f0523d4 100644 --- a/docs/references.bib +++ b/docs/references.bib @@ -1659,6 +1659,21 @@ @Book{ diamondshurman2005 zbl = {1062.11022} } +@Book{ DiestelUhl1977, + author = {Diestel, J. and Uhl, J. J. jun.}, + title = {Vector measures}, + fseries = {Mathematical Surveys}, + series = {Math. Surv.}, + issn = {0076-5376}, + volume = {15}, + year = {1977}, + publisher = {American Mathematical Society (AMS), Providence, RI}, + language = {English}, + keywords = {46G10,28B05,28A15,28A20,46-02,46B10,46B99,46E15,46E30,46G05,47A65,47B06,47B10,47B99}, + zbmath = {3576139}, + zbl = {0369.46039} +} + @Article{ dieudonne1953, author = {Dieudonn\'{e}, Jean}, title = {On semi-simple {L}ie algebras},