diff --git a/TestingLowerBounds/ForMathlib/AbsolutelyContinuous.lean b/TestingLowerBounds/ForMathlib/AbsolutelyContinuous.lean index bd81bb55..67c24a6e 100644 --- a/TestingLowerBounds/ForMathlib/AbsolutelyContinuous.lean +++ b/TestingLowerBounds/ForMathlib/AbsolutelyContinuous.lean @@ -15,17 +15,17 @@ open ProbabilityTheory MeasurableSpace Set open scoped ENNReal -namespace MeasureTheory +namespace MeasureTheory.Measure variable {α γ : Type*} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {μ ν : Measure α} {κ η : Kernel α γ} -lemma Measure.absolutelyContinuous_compProd_left_iff +lemma absolutelyContinuous_compProd_left_iff [SFinite μ] [SFinite ν] [IsFiniteKernel κ] [∀ a, NeZero (κ a)] : μ ⊗ₘ κ ≪ ν ⊗ₘ κ ↔ μ ≪ ν := - ⟨Measure.absolutelyContinuous_of_compProd, fun h ↦ Measure.absolutelyContinuous_compProd_left h _⟩ + ⟨absolutelyContinuous_of_compProd, fun h ↦ absolutelyContinuous_compProd_left h _⟩ -lemma Measure.mutuallySingular_compProd_left (hμν : μ ⟂ₘ ν) (κ η : Kernel α γ) : +lemma mutuallySingular_compProd_left (hμν : μ ⟂ₘ ν) (κ η : Kernel α γ) : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η := by by_cases hμ : SFinite μ swap; · rw [compProd_of_not_sfinite _ _ hμ]; simp @@ -36,13 +36,81 @@ lemma Measure.mutuallySingular_compProd_left (hμν : μ ⟂ₘ ν) (κ η : Ker by_cases hη : IsSFiniteKernel η swap; · rw [compProd_of_not_isSFiniteKernel _ _ hη]; simp refine ⟨hμν.nullSet ×ˢ univ, hμν.measurableSet_nullSet.prod .univ, ?_⟩ - rw [Measure.compProd_apply_prod hμν.measurableSet_nullSet .univ, compl_prod_eq_union] - simp only [Measure.MutuallySingular.restrict_nullSet, lintegral_zero_measure, compl_univ, + rw [compProd_apply_prod hμν.measurableSet_nullSet .univ, compl_prod_eq_union] + simp only [MutuallySingular.restrict_nullSet, lintegral_zero_measure, compl_univ, prod_empty, union_empty, true_and] - rw [Measure.compProd_apply_prod hμν.measurableSet_nullSet.compl .univ] + rw [compProd_apply_prod hμν.measurableSet_nullSet.compl .univ] simp -lemma Measure.mutuallySingular_compProd_right [CountableOrCountablyGenerated α γ] +lemma mutuallySingular_of_mutuallySingular_compProd {ξ : Measure α} + [SFinite μ] [SFinite ν] [IsSFiniteKernel κ] [IsSFiniteKernel η] + (h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η) (hμ : ξ ≪ μ) (hν : ξ ≪ ν) : + ∀ᵐ x ∂ξ, κ x ⟂ₘ η x := by + have hs : MeasurableSet h.nullSet := h.measurableSet_nullSet + have hμ_zero : (μ ⊗ₘ κ) h.nullSet = 0 := h.measure_nullSet + have hν_zero : (ν ⊗ₘ η) h.nullSetᶜ = 0 := h.measure_compl_nullSet + rw [compProd_apply, lintegral_eq_zero_iff'] at hμ_zero hν_zero + · filter_upwards [hμ hμ_zero, hν hν_zero] with x hxμ hxν + exact ⟨Prod.mk x ⁻¹' h.nullSet, measurable_prod_mk_left hs, ⟨hxμ, hxν⟩⟩ + · exact Kernel.measurable_kernel_prod_mk_left hs.compl |>.aemeasurable + · exact Kernel.measurable_kernel_prod_mk_left hs |>.aemeasurable + · exact hs.compl + · exact hs + +lemma mutuallySingular_compProd_iff_of_same_right (μ ν : Measure α) [IsFiniteMeasure μ] + [IsFiniteMeasure ν] (κ : Kernel α γ) [IsFiniteKernel κ] [hκ : ∀ x, NeZero (κ x)] : + μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ ↔ μ ⟂ₘ ν := by + refine ⟨fun h ↦ ?_, fun h ↦ mutuallySingular_compProd_left h _ _⟩ + rw [← withDensity_rnDeriv_eq_zero] + have hh := mutuallySingular_of_mutuallySingular_compProd h ?_ ?_ (ξ := ν.withDensity (∂μ/∂ν)) + rotate_left + · exact absolutelyContinuous_of_le (μ.withDensity_rnDeriv_le ν) + · exact withDensity_absolutelyContinuous _ _ + simp_rw [MutuallySingular.self_iff, (hκ _).ne] at hh + exact ae_eq_bot.mp (Filter.eventually_false_iff_eq_bot.mp hh) + +lemma absolutelyContinuous_of_add_of_mutuallySingular {ν₁ ν₂ : Measure α} + (h_ms : μ ⟂ₘ ν₂) (h : μ ≪ ν₁ + ν₂) : μ ≪ ν₁ := by + refine AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_ + let t := h_ms.nullSet + have ht : MeasurableSet t := h_ms.measurableSet_nullSet + have htμ : μ t = 0 := h_ms.measure_nullSet + have htν₂ : ν₂ tᶜ = 0 := h_ms.measure_compl_nullSet + have : μ s = μ (s ∩ tᶜ) := by + conv_lhs => rw [← inter_union_compl s t] + rw [measure_union, measure_inter_null_of_null_right _ htμ, zero_add] + · exact (disjoint_compl_right.inter_right' _ ).inter_left' _ + · exact hs.inter ht.compl + rw [this] + refine h ?_ + simp only [Measure.coe_add, Pi.add_apply, add_eq_zero] + exact ⟨measure_inter_null_of_null_left _ hs_zero, measure_inter_null_of_null_right _ htν₂⟩ + +lemma absolutelyContinuous_compProd_of_compProd [SFinite ν] [IsSFiniteKernel η] + (hμν : μ ≪ ν) (hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η) : + μ ⊗ₘ κ ≪ ν ⊗ₘ η := by + by_cases hμ : SFinite μ + swap; · rw [compProd_of_not_sfinite _ _ hμ]; simp + refine AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_ + suffices (μ ⊗ₘ η) s = 0 from hκη this + rw [measure_zero_iff_ae_nmem, ae_compProd_iff hs.compl] at hs_zero ⊢ + exact hμν.ae_le hs_zero + +lemma absolutelyContinuous_compProd_of_compProd' + [SigmaFinite μ] [SigmaFinite ν] [IsSFiniteKernel κ] [IsSFiniteKernel η] + (hκη : μ ⊗ₘ κ ≪ ν ⊗ₘ η) : + μ ⊗ₘ κ ≪ μ ⊗ₘ η := by + rw [ν.haveLebesgueDecomposition_add μ, compProd_add_left, add_comm] at hκη + have h := absolutelyContinuous_of_add_of_mutuallySingular ?_ hκη + · refine h.trans ?_ + refine absolutelyContinuous_compProd_left ?_ _ + exact withDensity_absolutelyContinuous _ _ + · refine mutuallySingular_compProd_left ?_ _ _ + exact (mutuallySingular_singularPart _ _).symm + +variable [CountableOrCountablyGenerated α γ] + +lemma mutuallySingular_compProd_right (μ ν : Measure α) {κ η : Kernel α γ} [IsFiniteKernel κ] [IsFiniteKernel η] (hκη : ∀ᵐ a ∂μ, κ a ⟂ₘ η a) : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η := by @@ -54,7 +122,7 @@ lemma Measure.mutuallySingular_compProd_right [CountableOrCountablyGenerated α have hs : MeasurableSet s := Kernel.measurableSet_mutuallySingularSet κ η symm refine ⟨s, hs, ?_⟩ - rw [Measure.compProd_apply hs, Measure.compProd_apply hs.compl] + rw [compProd_apply hs, compProd_apply hs.compl] have h_eq a : Prod.mk a ⁻¹' s = Kernel.mutuallySingularSetSlice κ η a := rfl have h1 a : η a (Prod.mk a ⁻¹' s) = 0 := by rw [h_eq, Kernel.measure_mutuallySingularSetSlice] have h2 : ∀ᵐ a ∂ μ, κ a (Prod.mk a ⁻¹' s)ᶜ = 0 := by @@ -64,7 +132,7 @@ lemma Measure.mutuallySingular_compProd_right [CountableOrCountablyGenerated α exact ha simp [h1, lintegral_congr_ae h2] -lemma Measure.mutuallySingular_compProd_right' [CountableOrCountablyGenerated α γ] +lemma mutuallySingular_compProd_right' (μ ν : Measure α) {κ η : Kernel α γ} [IsFiniteKernel κ] [IsFiniteKernel η] (hκη : ∀ᵐ a ∂ν, κ a ⟂ₘ η a) : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η := by @@ -72,80 +140,48 @@ lemma Measure.mutuallySingular_compProd_right' [CountableOrCountablyGenerated α swap; · rw [compProd_of_not_sfinite _ _ hμ]; simp by_cases hν : SFinite ν swap; · rw [compProd_of_not_sfinite _ _ hν]; simp - refine (Measure.mutuallySingular_compProd_right _ _ ?_).symm - simp_rw [Measure.MutuallySingular.comm, hκη] + refine (mutuallySingular_compProd_right _ _ ?_).symm + simp_rw [MutuallySingular.comm, hκη] -lemma Measure.mutuallySingular_of_mutuallySingular_compProd {ξ : Measure α} - [SFinite μ] [SFinite ν] [IsSFiniteKernel κ] [IsSFiniteKernel η] - (h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η) (hμ : ξ ≪ μ) (hν : ξ ≪ ν) : - ∀ᵐ x ∂ξ, κ x ⟂ₘ η x := by - have hs : MeasurableSet h.nullSet := h.measurableSet_nullSet - have hμ_zero : (μ ⊗ₘ κ) h.nullSet = 0 := h.measure_nullSet - have hν_zero : (ν ⊗ₘ η) h.nullSetᶜ = 0 := h.measure_compl_nullSet - rw [Measure.compProd_apply, lintegral_eq_zero_iff'] at hμ_zero hν_zero - · filter_upwards [hμ hμ_zero, hν hν_zero] with x hxμ hxν - exact ⟨Prod.mk x ⁻¹' h.nullSet, measurable_prod_mk_left hs, ⟨hxμ, hxν⟩⟩ - · exact Kernel.measurable_kernel_prod_mk_left hs.compl |>.aemeasurable - · exact Kernel.measurable_kernel_prod_mk_left hs |>.aemeasurable - · exact hs.compl - · exact hs - -lemma Measure.mutuallySingular_compProd_iff_of_same_left - [CountableOrCountablyGenerated α γ] (μ : Measure α) [SFinite μ] +lemma mutuallySingular_compProd_iff_of_same_left (μ : Measure α) [SFinite μ] (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η] : μ ⊗ₘ κ ⟂ₘ μ ⊗ₘ η ↔ ∀ᵐ a ∂μ, κ a ⟂ₘ η a := by refine ⟨fun h ↦ ?_, fun h ↦ mutuallySingular_compProd_right _ _ h⟩ exact mutuallySingular_of_mutuallySingular_compProd h (fun _ a ↦ a) (fun _ a ↦ a) -lemma Measure.mutuallySingular_compProd_iff_of_same_right (μ ν : Measure α) [IsFiniteMeasure μ] - [IsFiniteMeasure ν] (κ : Kernel α γ) [IsFiniteKernel κ] [hκ : ∀ x, NeZero (κ x)] : - μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ ↔ μ ⟂ₘ ν := by - refine ⟨fun h ↦ ?_, fun h ↦ mutuallySingular_compProd_left h _ _⟩ - rw [← Measure.withDensity_rnDeriv_eq_zero] - have hh := mutuallySingular_of_mutuallySingular_compProd h ?_ ?_ (ξ := ν.withDensity (∂μ/∂ν)) - rotate_left - · exact Measure.absolutelyContinuous_of_le (μ.withDensity_rnDeriv_le ν) - · exact MeasureTheory.withDensity_absolutelyContinuous _ _ - simp_rw [Measure.MutuallySingular.self_iff, (hκ _).ne] at hh - exact ae_eq_bot.mp (Filter.eventually_false_iff_eq_bot.mp hh) - -variable [CountableOrCountablyGenerated α γ] - section MeasureCompProd -lemma Measure.absolutelyContinuous_kernel_of_compProd +lemma absolutelyContinuous_kernel_of_compProd [SFinite μ] [SFinite ν] [IsFiniteKernel κ] [IsFiniteKernel η] (h : μ ⊗ₘ κ ≪ ν ⊗ₘ η) : ∀ᵐ a ∂μ, κ a ≪ η a := by suffices ∀ᵐ a ∂μ, κ.singularPart η a = 0 by filter_upwards [this] with a ha rwa [Kernel.singularPart_eq_zero_iff_absolutelyContinuous] at ha - rw [← κ.rnDeriv_add_singularPart η, Measure.compProd_add_right, - Measure.AbsolutelyContinuous.add_left_iff] at h + rw [← κ.rnDeriv_add_singularPart η, compProd_add_right, AbsolutelyContinuous.add_left_iff] at h have : μ ⊗ₘ κ.singularPart η ⟂ₘ ν ⊗ₘ η := - Measure.mutuallySingular_compProd_right μ ν - (.of_forall <| Kernel.mutuallySingular_singularPart _ _) + mutuallySingular_compProd_right μ ν (.of_forall <| Kernel.mutuallySingular_singularPart _ _) have h_zero : μ ⊗ₘ κ.singularPart η = 0 := - Measure.eq_zero_of_absolutelyContinuous_of_mutuallySingular h.2 this - simp_rw [← Measure.measure_univ_eq_zero] + eq_zero_of_absolutelyContinuous_of_mutuallySingular h.2 this + simp_rw [← measure_univ_eq_zero] refine (lintegral_eq_zero_iff (Kernel.measurable_coe _ .univ)).mp ?_ - rw [← setLIntegral_univ, ← Measure.compProd_apply_prod .univ .univ, h_zero] + rw [← setLIntegral_univ, ← compProd_apply_prod .univ .univ, h_zero] simp -lemma Measure.absolutelyContinuous_compProd_iff +lemma absolutelyContinuous_compProd_iff [SFinite μ] [SFinite ν] [IsFiniteKernel κ] [IsFiniteKernel η] [∀ a, NeZero (κ a)] : μ ⊗ₘ κ ≪ ν ⊗ₘ η ↔ μ ≪ ν ∧ ∀ᵐ a ∂μ, κ a ≪ η a := - ⟨fun h ↦ ⟨Measure.absolutelyContinuous_of_compProd h, absolutelyContinuous_kernel_of_compProd h⟩, - fun h ↦ Measure.absolutelyContinuous_compProd h.1 h.2⟩ + ⟨fun h ↦ ⟨absolutelyContinuous_of_compProd h, absolutelyContinuous_kernel_of_compProd h⟩, + fun h ↦ absolutelyContinuous_compProd h.1 h.2⟩ -lemma Measure.absolutelyContinuous_compProd_right_iff +lemma absolutelyContinuous_compProd_right_iff {μ : Measure α} {κ η : Kernel α γ} [SFinite μ] [IsFiniteKernel κ] [IsFiniteKernel η] : μ ⊗ₘ κ ≪ μ ⊗ₘ η ↔ ∀ᵐ a ∂μ, κ a ≪ η a := - ⟨absolutelyContinuous_kernel_of_compProd, fun h ↦ Measure.absolutelyContinuous_compProd_right h⟩ + ⟨absolutelyContinuous_kernel_of_compProd, fun h ↦ absolutelyContinuous_compProd_right h⟩ end MeasureCompProd -end MeasureTheory +end MeasureTheory.Measure open MeasureTheory diff --git a/TestingLowerBounds/ForMathlib/RNDerivEqCondexp.lean b/TestingLowerBounds/ForMathlib/RNDerivEqCondexp.lean index 1f38b9f5..55d9b153 100644 --- a/TestingLowerBounds/ForMathlib/RNDerivEqCondexp.lean +++ b/TestingLowerBounds/ForMathlib/RNDerivEqCondexp.lean @@ -46,4 +46,55 @@ lemma toReal_rnDeriv_comp [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hμν : μ filter_upwards [Kernel.rnDeriv_measure_compProd_left μ ν κ] with x hx rw [hx] +theorem _root_.Measurable.setLIntegral_kernel_prod_right' [IsSFiniteKernel κ] + {f : α × β → ℝ≥0∞} (hf : Measurable f) {s : Set β} (hs : MeasurableSet s) : + Measurable fun a => ∫⁻ b in s, f (a, b) ∂κ a := by + simp_rw [← Kernel.lintegral_restrict κ hs]; exact hf.lintegral_kernel_prod_right' + +lemma rnDeriv_compProd [IsFiniteMeasure μ] [IsFiniteMeasure ν] + (hμν : μ ≪ ν) [IsFiniteKernel κ] [IsFiniteKernel η] (h_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η) : + (fun p ↦ μ.rnDeriv ν p.1 * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) p) + =ᵐ[ν ⊗ₘ η] (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) := by + have h_ac1 : μ ⊗ₘ κ ≪ ν ⊗ₘ η := Measure.absolutelyContinuous_compProd_of_compProd hμν h_ac + have h_meas : Measurable fun p ↦ (∂μ/∂ν) p.1 * (∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p := + ((Measure.measurable_rnDeriv _ _).comp measurable_fst).mul (Measure.measurable_rnDeriv _ _) + have h_eq t₁ t₂ : MeasurableSet t₁ → MeasurableSet t₂ → + ∫⁻ p in t₁ ×ˢ t₂, (∂μ/∂ν) p.1 * (∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p ∂ν ⊗ₘ η + = ∫⁻ p in t₁ ×ˢ t₂, (∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p ∂ν ⊗ₘ η := by + intro ht₁ ht₂ + rw [Measure.setLIntegral_compProd h_meas ht₁ ht₂] + simp only + have : ∀ a, ∫⁻ b in t₂, (∂μ/∂ν) a * (∂μ ⊗ₘ κ/∂μ ⊗ₘ η) (a, b) ∂η a + = (∂μ/∂ν) a * ∫⁻ b in t₂, (∂μ ⊗ₘ κ/∂μ ⊗ₘ η) (a, b) ∂η a := fun a ↦ by + rw [lintegral_const_mul] + exact (Measure.measurable_rnDeriv _ _).comp measurable_prod_mk_left + simp_rw [this] + rw [setLIntegral_rnDeriv_mul hμν _ ht₁] + swap + · exact ((Measure.measurable_rnDeriv _ _).setLIntegral_kernel_prod_right' ht₂).aemeasurable + rw [← Measure.setLIntegral_compProd (Measure.measurable_rnDeriv _ _) ht₁ ht₂, + Measure.setLIntegral_rnDeriv h_ac1, Measure.setLIntegral_rnDeriv h_ac] + refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite h_meas ?_ ?_ + · exact Measure.measurable_rnDeriv _ _ + · intro s hs _ + apply induction_on_inter generateFrom_prod.symm isPiSystem_prod _ _ _ _ hs + · simp + · rintro _ ⟨t₁, ht₁, t₂, ht₂, rfl⟩ + exact h_eq t₁ t₂ ht₁ ht₂ + · intro t ht ht_eq + have h_ne_top : ∫⁻ p in t, (∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p ∂ν ⊗ₘ η ≠ ⊤ := by + rw [Measure.setLIntegral_rnDeriv] + · exact measure_ne_top _ _ + · exact h_ac1 + rw [setLintegral_compl ht h_ne_top, setLintegral_compl ht, ht_eq] + swap; · rw [ht_eq]; exact h_ne_top + congr 1 + have h := h_eq .univ .univ .univ .univ + simp only [univ_prod_univ, Measure.restrict_univ] at h + exact h + · intro f' hf_disj hf_meas hf_eq + rw [lintegral_iUnion hf_meas hf_disj, lintegral_iUnion hf_meas hf_disj] + congr with i + exact hf_eq i + end ProbabilityTheory