PL1/VectorDensityBounds.lean

All source files · Download exact source

SHA-256: 5851f3d9d8e089b8e80f819feb4097d7b7d40c1621e72cd3bf210b5bfc25b5dc

1import PL1.RNPBridge2import Mathlib.MeasureTheory.VectorMeasure.WithDensityVec3import Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym4import Mathlib.MeasureTheory.Function.AEEqOfLIntegral56/-! # Pointwise bounds for vector-measure densities -/78noncomputable section9universe u v w10open MeasureTheory11open scoped ENNReal NNReal1213namespace PL1.VectorDensityBounds1415variable {Ω : Type w} [MeasurableSpace Ω]16variable {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E]17variable {E₀ : Type v} [NormedAddCommGroup E₀] [NormedSpace ℝ E₀]1819omit [NormedSpace ℝ E] in20/-- Null-set vanishing of a vector measure implies absolute continuity of its total variation. -/21theorem variation_absolutelyContinuous (μ : Measure Ω) (ν : VectorMeasure Ω E)22    (hAC : ∀ A : Set Ω, MeasurableSet A → μ A = 0 → ν A = 0) :23    ν.variation ≪ μ := by24  apply Measure.AbsolutelyContinuous.mk25  intro A hA hμA26  apply (VectorMeasure.variation_apply_eq_zero hA).mpr27  intro B hBA hB28  exact hAC B hB (measure_mono_null hBA hμA)2930/-- Domination of positive measures with density yields pointwise domination of their densities. -/31theorem ae_le_of_withDensity_le (μ : Measure Ω) [SigmaFinite μ]32    {f g : Ω → ℝ≥0∞} (hf : AEMeasurable f μ)33    (h : μ.withDensity f ≤ μ.withDensity g) : f ≤ᵐ[μ] g := by34  apply ae_le_of_forall_setLIntegral_le_of_sigmaFinite₀ hf35  intro A hA _36  rw [← withDensity_apply f hA, ← withDensity_apply g hA]37  exact h A3839/-- A finite absolutely continuous measure dominating the variation controls a Bochner40density pointwise by its ordinary Radon–Nikodym derivative. -/41theorem ae_norm_density_le_rnDeriv [CompleteSpace E]42    (μ τ : Measure Ω) [IsFiniteMeasure μ] [IsFiniteMeasure τ]43    (hτ : τ ≪ μ) {g : Ω → E} (hg : Integrable g μ)44    (C : ℝ) (hC : 0 ≤ C)45    (hbound : (μ.withDensityᵥ g).variation ≤ ENNReal.ofReal C • τ) :46    ∀ᵐ x ∂μ, ‖g x‖ ≤ C * (τ.rnDeriv μ x).toReal := by47  have hwith : μ.withDensity (fun x => ‖g x‖ₑ) ≤48      μ.withDensity (ENNReal.ofReal C • τ.rnDeriv μ) := by49    rw [withDensity_smul _ (τ.measurable_rnDeriv μ), Measure.withDensity_rnDeriv_eq τ μ hτ]50    rw [← Measure.variation_withDensityᵥ hg]51    exact hbound52  have hae := ae_le_of_withDensity_le μ hg.aestronglyMeasurable.enorm hwith53  filter_upwards [hae, Measure.rnDeriv_lt_top τ μ] with x hx hfinite54  have hreal := ENNReal.toReal_mono55    (ENNReal.mul_ne_top ENNReal.ofReal_ne_top hfinite.ne) hx56  simpa only [Pi.smul_apply, smul_eq_mul, ENNReal.toReal_mul,57    ENNReal.toReal_ofReal hC, toReal_enorm] using hreal5859/-- Applying a bounded linear map to a vector measure gives a uniformly dominated density. -/60theorem ae_norm_map_density_le_rnDeriv [CompleteSpace E]61    (μ : Measure Ω) [IsFiniteMeasure μ] (ν : VectorMeasure Ω E₀)62    [IsFiniteMeasure ν.variation]63    (hAC : ∀ A : Set Ω, MeasurableSet A → μ A = 0 → ν A = 0)64    (T : E₀ →L[ℝ] E) {g : Ω → E} (hg : Integrable g μ)65    (hrep : μ.withDensityᵥ g = RNPBridge.mapVectorMeasure T ν)66    (C : ℝ) (hC : 0 ≤ C) (hT : ‖T‖ ≤ C) :67    ∀ᵐ x ∂μ, ‖g x‖ ≤ C * (ν.variation.rnDeriv μ x).toReal := by68  apply ae_norm_density_le_rnDeriv μ ν.variation69    (variation_absolutelyContinuous μ ν hAC) hg C hC70  rw [hrep]71  apply (RNPBridge.variation_mapVectorMeasure_le T ν).trans72  intro A73  simp only [Measure.smul_apply, smul_eq_mul]74  apply mul_le_mul_of_nonneg_right _ zero_le75  simpa only [ofReal_norm] using ENNReal.ofReal_le_ofReal hT7677end PL1.VectorDensityBounds78