From a1745ea0fdfaaa1028cb16e8ed6fa4523b7a76c3 Mon Sep 17 00:00:00 2001 From: Lorenzo Luccioli Date: Fri, 30 Aug 2024 12:04:44 +0200 Subject: [PATCH] apply changes --- TestingLowerBounds/Convex.lean | 2 +- .../Divergences/KullbackLeibler.lean | 2 +- TestingLowerBounds/Divergences/Renyi.lean | 2 +- TestingLowerBounds/Divergences/StatInfo.lean | 2 +- TestingLowerBounds/ErealLLR.lean | 10 +- TestingLowerBounds/FDiv/Basic.lean | 50 ++++---- TestingLowerBounds/FDiv/CompProd.lean | 24 ++-- TestingLowerBounds/FDiv/CondFDiv.lean | 63 +++++----- .../FDiv/IntegralRnDerivSingularPart.lean | 116 ++++++++---------- TestingLowerBounds/FDiv/Trim.lean | 2 +- .../LogLikelihoodRatioCompProd.lean | 2 +- .../ForMathlib/RadonNikodym.lean | 93 +++++++------- TestingLowerBounds/ForMathlib/RnDeriv.lean | 59 ++++----- TestingLowerBounds/Kernel/Basic.lean | 4 +- TestingLowerBounds/Kernel/BayesInv.lean | 2 +- TestingLowerBounds/Kernel/Monoidal.lean | 13 +- TestingLowerBounds/MeasureCompProd.lean | 79 +++++------- TestingLowerBounds/Testing/Binary.lean | 46 ++++--- TestingLowerBounds/Testing/ChangeMeasure.lean | 2 +- TestingLowerBounds/Testing/Risk.lean | 12 +- 20 files changed, 272 insertions(+), 313 deletions(-) diff --git a/TestingLowerBounds/Convex.lean b/TestingLowerBounds/Convex.lean index 5e6cdc2e..4bc06da2 100644 --- a/TestingLowerBounds/Convex.lean +++ b/TestingLowerBounds/Convex.lean @@ -78,7 +78,7 @@ lemma comp_neg_iff {𝕜 F β : Type*} [LinearOrderedField 𝕜] [AddCommGroup F exact h.comp_neg --this can be stated in much greater generality -lemma const_mul_id (c : ℝ) : ConvexOn ℝ Set.univ (fun (x : ℝ) ↦ c * x) := by +lemma const_mul_id (c : ℝ) : ConvexOn ℝ .univ (fun (x : ℝ) ↦ c * x) := by refine ⟨convex_univ, fun _ _ _ _ _ _ _ _ _ ↦ Eq.le ?_⟩ simp only [smul_eq_mul] ring diff --git a/TestingLowerBounds/Divergences/KullbackLeibler.lean b/TestingLowerBounds/Divergences/KullbackLeibler.lean index 1d87efd4..ef101adc 100644 --- a/TestingLowerBounds/Divergences/KullbackLeibler.lean +++ b/TestingLowerBounds/Divergences/KullbackLeibler.lean @@ -30,7 +30,7 @@ variable {α : Type*} {mα : MeasurableSpace α} {μ ν : Measure α} section move_this lemma integrable_rnDeriv_smul {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] - [Measure.HaveLebesgueDecomposition μ ν] (hμν : μ ≪ ν) + [μ.HaveLebesgueDecomposition ν] (hμν : μ ≪ ν) [SigmaFinite μ] {f : α → E} (hf : Integrable f μ) : Integrable (fun x ↦ (μ.rnDeriv ν x).toReal • f x) ν := (integrable_rnDeriv_smul_iff hμν).mpr hf diff --git a/TestingLowerBounds/Divergences/Renyi.lean b/TestingLowerBounds/Divergences/Renyi.lean index 0b15a867..d4755061 100644 --- a/TestingLowerBounds/Divergences/Renyi.lean +++ b/TestingLowerBounds/Divergences/Renyi.lean @@ -38,7 +38,7 @@ variable {α β : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} { -- todo: move lemma exp_mul_llr [SigmaFinite μ] [SigmaFinite ν] (hνμ : ν ≪ μ) : (fun x ↦ exp (a * llr μ ν x)) =ᵐ[ν] fun x ↦ (μ.rnDeriv ν x).toReal ^ a := by - filter_upwards [Measure.rnDeriv_lt_top μ ν, Measure.rnDeriv_pos' hνμ] with x hx_lt_top hx_pos + filter_upwards [μ.rnDeriv_lt_top ν, Measure.rnDeriv_pos' hνμ] with x hx_lt_top hx_pos simp only [llr_def] have h_pos : 0 < ((∂μ/∂ν) x).toReal := ENNReal.toReal_pos hx_pos.ne' hx_lt_top.ne rw [← log_rpow h_pos, exp_log (rpow_pos_of_pos h_pos _)] diff --git a/TestingLowerBounds/Divergences/StatInfo.lean b/TestingLowerBounds/Divergences/StatInfo.lean index 7754847e..2e0ac8e3 100644 --- a/TestingLowerBounds/Divergences/StatInfo.lean +++ b/TestingLowerBounds/Divergences/StatInfo.lean @@ -761,7 +761,7 @@ lemma fDiv_ne_top_iff_integrable_fDiv_statInfoFun_of_absolutelyContinuous' simp_rw [this, ← EReal.toReal_toENNReal fDiv_statInfoFun_nonneg] rw [integrable_toReal_iff] rotate_left - · exact hf_cont.measurable.comp (Measure.measurable_rnDeriv μ ν).ennreal_toReal + · exact hf_cont.measurable.comp (μ.measurable_rnDeriv ν).ennreal_toReal |>.ennreal_ofReal.aemeasurable · exact .of_forall fun _ ↦ ENNReal.ofReal_ne_top rw [integrable_toReal_iff] diff --git a/TestingLowerBounds/ErealLLR.lean b/TestingLowerBounds/ErealLLR.lean index 0aface86..85a5a955 100644 --- a/TestingLowerBounds/ErealLLR.lean +++ b/TestingLowerBounds/ErealLLR.lean @@ -54,27 +54,27 @@ lemma EReal.exp_neg_llr' [SigmaFinite μ] [SigmaFinite ν] (hμν : ν ≪ μ) : @[measurability] lemma measurable_ereal_llr (μ ν : Measure α) : Measurable (EReal.llr μ ν) := - (Measure.measurable_rnDeriv μ ν).ennreal_log + (μ.measurable_rnDeriv ν).ennreal_log @[measurability] lemma stronglyMeasurable_ereal_llr (μ ν : Measure α) : StronglyMeasurable (EReal.llr μ ν) := (measurable_ereal_llr μ ν).stronglyMeasurable -lemma EReal.llr_smul_left [IsFiniteMeasure μ] [Measure.HaveLebesgueDecomposition μ ν] +lemma EReal.llr_smul_left [IsFiniteMeasure μ] [μ.HaveLebesgueDecomposition ν] (hμν : μ ≪ ν) (c : ℝ≥0∞) (hc_ne_top : c ≠ ∞) : EReal.llr (c • μ) ν =ᵐ[μ] fun x ↦ EReal.llr μ ν x + ENNReal.log c := by simp only [EReal.llr, EReal.llr_def] - have h := Measure.rnDeriv_smul_left_of_ne_top μ ν hc_ne_top + have h := μ.rnDeriv_smul_left_of_ne_top ν hc_ne_top filter_upwards [hμν.ae_le h] with x hx_eq rw [hx_eq] simp only [Pi.smul_apply, smul_eq_mul, ENNReal.toReal_mul] rw [ENNReal.log_mul_add, add_comm] -lemma EReal.llr_smul_right [IsFiniteMeasure μ] [Measure.HaveLebesgueDecomposition μ ν] +lemma EReal.llr_smul_right [IsFiniteMeasure μ] [μ.HaveLebesgueDecomposition ν] (hμν : μ ≪ ν) (c : ℝ≥0∞) (hc : c ≠ 0) (hc_ne_top : c ≠ ∞) : EReal.llr μ (c • ν) =ᵐ[μ] fun x ↦ EReal.llr μ ν x - ENNReal.log c := by simp only [llr, llr_def] - have h := Measure.rnDeriv_smul_right_of_ne_top μ ν hc hc_ne_top + have h := μ.rnDeriv_smul_right_of_ne_top ν hc hc_ne_top filter_upwards [hμν.ae_le h] with x hx_eq rw [hx_eq] simp only [Pi.smul_apply, smul_eq_mul, ENNReal.toReal_mul] diff --git a/TestingLowerBounds/FDiv/Basic.lean b/TestingLowerBounds/FDiv/Basic.lean index b200cc87..dce4a919 100644 --- a/TestingLowerBounds/FDiv/Basic.lean +++ b/TestingLowerBounds/FDiv/Basic.lean @@ -130,7 +130,7 @@ lemma fDiv_congr' (μ ν : Measure α) (hfg : ∀ᵐ x ∂ν.map (fun x ↦ (( (hfg' : f =ᶠ[atTop] g) : fDiv f μ ν = fDiv g μ ν := by have h : (fun a ↦ f ((∂μ/∂ν) a).toReal) =ᶠ[ae ν] fun a ↦ g ((∂μ/∂ν) a).toReal := - ae_of_ae_map (Measure.measurable_rnDeriv μ ν).ennreal_toReal.aemeasurable hfg + ae_of_ae_map (μ.measurable_rnDeriv ν).ennreal_toReal.aemeasurable hfg rw [fDiv, derivAtTop_congr hfg'] congr 2 · exact eq_iff_iff.mpr ⟨fun hf ↦ hf.congr h, fun hf ↦ hf.congr h.symm⟩ @@ -155,7 +155,7 @@ lemma fDiv_eq_zero_of_forall_nonneg (μ ν : Measure α) (hf : ∀ x ≥ 0, f x @[simp] lemma fDiv_zero_measure (ν : Measure α) [IsFiniteMeasure ν] : fDiv f 0 ν = f 0 * ν .univ := by have : (fun x ↦ f ((∂0/∂ν) x).toReal) =ᵐ[ν] fun _ ↦ f 0 := by - filter_upwards [Measure.rnDeriv_zero ν] with x hx + filter_upwards [ν.rnDeriv_zero] with x hx rw [hx] simp rw [fDiv_of_integrable] @@ -200,7 +200,7 @@ lemma fDiv_const' {c : ℝ} (hc : 0 ≤ c) (μ ν : Measure α) : lemma fDiv_self (hf_one : f 1 = 0) (μ : Measure α) [SigmaFinite μ] : fDiv f μ μ = 0 := by have h : (fun x ↦ f (μ.rnDeriv μ x).toReal) =ᵐ[μ] 0 := by - filter_upwards [Measure.rnDeriv_self μ] with x hx + filter_upwards [μ.rnDeriv_self] with x hx rw [hx, ENNReal.one_toReal, hf_one] rfl rw [fDiv_of_integrable] @@ -217,7 +217,7 @@ lemma fDiv_id (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] : · rw [fDiv_of_integrable h_int] simp only [id_eq, derivAtTop_id, one_mul] rw [← integral_univ, Measure.setIntegral_toReal_rnDeriv_eq_withDensity] - have h_ne_top : (Measure.withDensity ν (∂μ/∂ν)) .univ ≠ ∞ := by + have h_ne_top : (ν.withDensity (∂μ/∂ν)) .univ ≠ ∞ := by rw [withDensity_apply _ .univ, setLIntegral_univ] rwa [integrable_toReal_iff] at h_int · exact (μ.measurable_rnDeriv ν).aemeasurable @@ -231,9 +231,8 @@ lemma fDiv_id (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] : by_contra h_ne_top have : IsFiniteMeasure μ := ⟨Ne.lt_top ?_⟩ swap; · rw [← EReal.coe_ennreal_top] at h_ne_top; exact mod_cast h_ne_top - refine h_int ?_ - refine integrable_toReal_of_lintegral_ne_top (μ.measurable_rnDeriv ν).aemeasurable ?_ - exact (Measure.lintegral_rnDeriv_lt_top _ _).ne + refine h_int <| integrable_toReal_of_lintegral_ne_top (μ.measurable_rnDeriv ν).aemeasurable ?_ + exact (μ.lintegral_rnDeriv_lt_top _).ne @[simp] lemma fDiv_id' (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] : @@ -414,10 +413,10 @@ lemma fDiv_eq_add_withDensity_singularPart have h_int_iff : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν ↔ Integrable (fun x ↦ f ((∂(ν.withDensity (∂μ/∂ν))/∂ν) x).toReal) ν := by refine integrable_congr ?_ - filter_upwards [Measure.rnDeriv_withDensity ν (μ.measurable_rnDeriv ν)] with x hx + filter_upwards [ν.rnDeriv_withDensity (μ.measurable_rnDeriv ν)] with x hx rw [hx] classical - rw [fDiv_of_mutuallySingular (Measure.mutuallySingular_singularPart _ _)] + rw [fDiv_of_mutuallySingular (μ.mutuallySingular_singularPart _)] by_cases hf : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν · rw [fDiv_of_absolutelyContinuous (withDensity_absolutelyContinuous _ _), if_pos, fDiv_of_integrable hf] @@ -426,7 +425,7 @@ lemma fDiv_eq_add_withDensity_singularPart rw [add_sub_assoc] congr 2 · refine integral_congr_ae ?_ - filter_upwards [Measure.rnDeriv_withDensity ν (μ.measurable_rnDeriv ν)] with x hx + filter_upwards [ν.rnDeriv_withDensity (μ.measurable_rnDeriv ν)] with x hx rw [hx] rw [← EReal.coe_ennreal_toReal (measure_ne_top ν _), ← EReal.coe_mul, EReal.add_sub_cancel'] · rw [fDiv_of_not_integrable hf, fDiv_of_not_integrable] @@ -465,8 +464,7 @@ lemma fDiv_eq_add_withDensity_derivAtTop (hf_cvx : ConvexOn ℝ (Ici 0) f) : fDiv f μ ν = fDiv f (ν.withDensity (∂μ/∂ν)) ν + derivAtTop f * μ.singularPart ν .univ := by rw [fDiv_eq_add_withDensity_singularPart'' μ ν hf_cvx, - fDiv_of_mutuallySingular (Measure.mutuallySingular_singularPart _ _), - derivAtTop_sub_const hf_cvx] + fDiv_of_mutuallySingular (μ.mutuallySingular_singularPart _), derivAtTop_sub_const hf_cvx] simp lemma fDiv_lt_top_of_ac (h : μ ≪ ν) (h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) : @@ -494,7 +492,7 @@ lemma fDiv_add_measure_le_of_ac {μ₁ μ₂ ν : Measure α} [IsFiniteMeasure integrable_f_rnDeriv_of_derivAtTop_ne_top _ _ hf hf_cvx h_top have h_le : ∀ᵐ x ∂ν, f ((∂μ₁ + μ₂/∂ν) x).toReal ≤ f ((∂μ₁/∂ν) x).toReal + (derivAtTop f).toReal * ((∂μ₂/∂ν) x).toReal := by - have h_add := Measure.rnDeriv_add' μ₁ μ₂ ν + have h_add := μ₁.rnDeriv_add' μ₂ ν filter_upwards [h_add, μ₁.rnDeriv_lt_top ν, μ₂.rnDeriv_lt_top ν] with x hx hx₁ hx₂ rw [hx, Pi.add_apply, ENNReal.toReal_add hx₁.ne hx₂.ne] exact le_add_derivAtTop'' hf_cvx h_top ENNReal.toReal_nonneg ENNReal.toReal_nonneg @@ -518,9 +516,9 @@ lemma fDiv_absolutelyContinuous_add_mutuallySingular {μ₁ μ₂ ν : Measure rw [fDiv_eq_add_withDensity_derivAtTop _ _ hf_cvx, Measure.singularPart_add, Measure.singularPart_eq_zero_of_ac h₁, Measure.singularPart_eq_self.mpr h₂, zero_add] congr - conv_rhs => rw [← Measure.withDensity_rnDeriv_eq μ₁ ν h₁] + conv_rhs => rw [← μ₁.withDensity_rnDeriv_eq ν h₁] refine withDensity_congr_ae ?_ - refine (Measure.rnDeriv_add' _ _ _).trans ?_ + refine (μ₁.rnDeriv_add' _ _).trans ?_ filter_upwards [Measure.rnDeriv_eq_zero_of_mutuallySingular h₂ Measure.AbsolutelyContinuous.rfl] with x hx simp [hx] @@ -535,12 +533,11 @@ lemma fDiv_add_measure_le (μ₁ μ₂ ν : Measure α) [IsFiniteMeasure μ₁] abel rw [this, fDiv_absolutelyContinuous_add_mutuallySingular ((withDensity_absolutelyContinuous _ _).add_left (withDensity_absolutelyContinuous _ _)) - ((Measure.mutuallySingular_singularPart _ _).add_left - (Measure.mutuallySingular_singularPart _ _)) hf_cvx] + ((μ₁.mutuallySingular_singularPart _).add_left (μ₂.mutuallySingular_singularPart _)) hf_cvx] simp only [Measure.coe_add, Pi.add_apply, EReal.coe_ennreal_add] conv_rhs => rw [add_comm (μ₁.singularPart ν)] rw [fDiv_absolutelyContinuous_add_mutuallySingular (withDensity_absolutelyContinuous _ _) - (Measure.mutuallySingular_singularPart _ _) hf_cvx] + (μ₁.mutuallySingular_singularPart _) hf_cvx] calc fDiv f (ν.withDensity (∂μ₁/∂ν) + ν.withDensity (∂μ₂/∂ν)) ν + derivAtTop f * (↑(μ₁.singularPart ν .univ) + ↑(μ₂.singularPart ν .univ)) = fDiv f (ν.withDensity (∂μ₁/∂ν) + ν.withDensity (∂μ₂/∂ν)) ν @@ -613,7 +610,7 @@ lemma fDiv_of_not_ac [SigmaFinite μ] [SigmaFinite ν] (hf : derivAtTop f = ⊤) rw [fDiv] split_ifs with h_int · rw [hf] - suffices Measure.singularPart μ ν .univ ≠ 0 by + suffices μ.singularPart ν .univ ≠ 0 by rw [EReal.top_mul_of_pos, EReal.coe_add_top] refine lt_of_le_of_ne (EReal.coe_ennreal_nonneg _) ?_ exact mod_cast this.symm @@ -722,9 +719,9 @@ lemma toReal_fDiv_of_integrable [IsFiniteMeasure μ] (hf_cvx : ConvexOn ℝ (Ici rotate_left · simp · simp - · simp only [ne_eq, EReal.mul_eq_top, hf_cvx.derivAtTop_ne_bot, false_and, EReal.coe_ennreal_ne_bot, - and_false, EReal.coe_ennreal_pos, Measure.measure_univ_pos, EReal.coe_ennreal_eq_top_iff, - measure_ne_top, or_false, false_or, not_and, not_not] + · simp only [ne_eq, EReal.mul_eq_top, hf_cvx.derivAtTop_ne_bot, false_and, + EReal.coe_ennreal_ne_bot, and_false, EReal.coe_ennreal_pos, Measure.measure_univ_pos, + EReal.coe_ennreal_eq_top_iff, measure_ne_top, or_false, false_or, not_and, not_not] intro h_top simp [h_top, Measure.singularPart_eq_zero_of_ac (h_deriv h_top)] · simp only [ne_eq, EReal.mul_eq_bot, hf_cvx.derivAtTop_ne_bot, EReal.coe_ennreal_pos, @@ -764,8 +761,7 @@ lemma le_fDiv [IsFiniteMeasure μ] [IsProbabilityMeasure ν] f (μ .univ).toReal ≤ fDiv f μ ν := by refine (f_measure_univ_le_add μ ν hf_cvx).trans ?_ rw [fDiv_eq_add_withDensity_singularPart'' μ _ hf_cvx, - fDiv_of_mutuallySingular (Measure.mutuallySingular_singularPart μ ν), - derivAtTop_sub_const hf_cvx] + fDiv_of_mutuallySingular (μ.mutuallySingular_singularPart ν), derivAtTop_sub_const hf_cvx] simp only [MeasurableSet.univ, withDensity_apply, Measure.restrict_univ, sub_self, EReal.coe_zero, measure_univ, EReal.coe_ennreal_one, mul_one, zero_add] gcongr @@ -790,7 +786,7 @@ lemma fDiv_mono'' (hf_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν swap; · simp gcongr · exact EReal.coe_le_coe_iff.mpr <| integral_mono_ae hf_int hg_int <| - ae_of_ae_map (Measure.measurable_rnDeriv μ ν).ennreal_toReal.aemeasurable hfg + ae_of_ae_map (μ.measurable_rnDeriv ν).ennreal_toReal.aemeasurable hfg · exact EReal.coe_ennreal_nonneg _ /- The hypothesis `hfg'` can probably be removed if we ask for the functions to be convex, since then it is true that `derivAtTop` is monotone, but we still don't have the result formalized. Moreover in the convex case we can also relax `hf_int` and only ask for a.e. strong measurability of `f` (at least when `μ` and `ν` are finite), because then the negative part of the function is always integrable, hence if `f` is not integrable `g` is also not integrable. -/ @@ -824,7 +820,7 @@ lemma fDiv_eq_zero_iff [IsFiniteMeasure μ] [IsFiniteMeasure ν] (h_mass : μ .u simp only [ENNReal.one_toReal, Function.const_one, log_one, mul_zero, lt_self_iff_false, or_false, hf_one] at h_eq exact (Measure.rnDeriv_eq_one_iff_eq hμν).mp <| ENNReal.eventuallyEq_of_toReal_eventuallyEq - (Measure.rnDeriv_ne_top _ _) (.of_forall fun _ ↦ ENNReal.one_ne_top) h_eq + (μ.rnDeriv_ne_top _) (.of_forall fun _ ↦ ENNReal.one_ne_top) h_eq lemma fDiv_eq_zero_iff' [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] (hf_deriv : derivAtTop f = ⊤) (hf_cvx : StrictConvexOn ℝ (Ici 0) f) @@ -862,7 +858,7 @@ lemma fDiv_restrict_of_integrable (μ ν : Measure α) [IsFiniteMeasure μ] [IsF classical have h : (fun x ↦ f ((∂μ.restrict s/∂ν) x).toReal) =ᵐ[ν] s.piecewise (fun x ↦ f ((∂μ/∂ν) x).toReal) (fun _ ↦ f 0) := by - filter_upwards [Measure.rnDeriv_restrict μ ν hs] with a ha + filter_upwards [μ.rnDeriv_restrict ν hs] with a ha rw [ha] by_cases has : a ∈ s <;> simp [has] rw [fDiv_of_integrable, μ.singularPart_restrict ν hs, Measure.restrict_apply_univ] diff --git a/TestingLowerBounds/FDiv/CompProd.lean b/TestingLowerBounds/FDiv/CompProd.lean index 9b11e8d2..b8d75053 100644 --- a/TestingLowerBounds/FDiv/CompProd.lean +++ b/TestingLowerBounds/FDiv/CompProd.lean @@ -155,7 +155,7 @@ lemma fDiv_compProd_left_ne_top_iff [IsFiniteMeasure μ] [IsFiniteMeasure ν] fDiv f (μ ⊗ₘ κ) (ν ⊗ₘ κ) ≠ ⊤ ↔ Integrable (fun a ↦ f ((∂μ/∂ν) a).toReal) ν ∧ (derivAtTop f = ⊤ → μ ≪ ν) := by rw [fDiv_compProd_ne_top_iff hf h_cvx] - have h_one : ∀ a, ∂(κ a)/∂(κ a) =ᵐ[κ a] 1 := fun a ↦ Measure.rnDeriv_self (κ a) + have h_one : ∀ a, ∂(κ a)/∂(κ a) =ᵐ[κ a] 1 := fun a ↦ (κ a).rnDeriv_self simp only [ENNReal.toReal_mul, Measure.AbsolutelyContinuous.rfl, eventually_true, and_true] have : ∀ a, ∫ b, f (((∂μ/∂ν) a).toReal * ((∂κ a/∂κ a) b).toReal) ∂κ a = ∫ _, f (((∂μ/∂ν) a).toReal) ∂κ a := by @@ -244,7 +244,7 @@ lemma f_rnDeriv_ae_le_integral [CountableOrCountablyGenerated α β] (fun a ↦ f ((∂μ/∂ν) a * κ a .univ).toReal) ≤ᵐ[ν] fun a ↦ ∫ b, f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) (a, b)).toReal ∂(η a) := by have h_compProd := Kernel.rnDeriv_measure_compProd' μ ν κ η - have h_lt_top := Measure.ae_ae_of_ae_compProd <| Measure.rnDeriv_lt_top (μ ⊗ₘ κ) (ν ⊗ₘ η) + have h_lt_top := Measure.ae_ae_of_ae_compProd <| (μ ⊗ₘ κ).rnDeriv_lt_top (ν ⊗ₘ η) have := Measure.integrable_toReal_rnDeriv (μ := μ ⊗ₘ κ) (ν := ν ⊗ₘ η) rw [Measure.integrable_compProd_iff] at this swap @@ -259,7 +259,7 @@ lemma f_rnDeriv_ae_le_integral [CountableOrCountablyGenerated α β] · simp [h0] · rw [Measure.lintegral_rnDeriv (h_ac h0)] _ = f (∫⁻ b,(∂μ/∂ν) a * (∂κ a/∂η a) b ∂η a).toReal := by - rw [lintegral_const_mul _ (Measure.measurable_rnDeriv _ _)] + rw [lintegral_const_mul _ ((κ a).measurable_rnDeriv _)] _ = f (∫⁻ b, (∂μ ⊗ₘ κ/∂ν ⊗ₘ η) (a, b) ∂η a).toReal := by rw [lintegral_congr_ae h_eq] _ = f (∫ b, ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) (a, b)).toReal ∂η a) := by rw [integral_toReal _ h_lt_top] @@ -410,7 +410,7 @@ lemma integrable_f_rnDeriv_of_integrable_compProd' [CountableOrCountablyGenerate (g₂ := fun a ↦ f ((∂μ/∂ν) a * η.withDensity (κ.rnDeriv η) a .univ).toReal + (derivAtTop f).toReal * ((∂μ/∂ν) a).toReal * (κ.singularPart η a .univ).toReal) ?_ ?_ ?_ ?_ ?_ - · exact (hf.comp_measurable (Measure.measurable_rnDeriv _ _).ennreal_toReal).aestronglyMeasurable + · exact (hf.comp_measurable (μ.measurable_rnDeriv _).ennreal_toReal).aestronglyMeasurable · exact ae_of_all _ (fun x ↦ h _ ENNReal.toReal_nonneg) · exact f_rnDeriv_le_add μ ν κ η hf_cvx h_deriv · exact (Measure.integrable_toReal_rnDeriv.const_mul _).add (integrable_const _) @@ -489,14 +489,13 @@ lemma le_fDiv_compProd [CountableOrCountablyGenerated α β] (μ ν : Measure α calc ∫ x, f ((∂μ/∂ν) x).toReal ∂ν + derivAtTop f * μ.singularPart ν .univ ≤ ∫ x, f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) x).toReal ∂(ν ⊗ₘ η) + (derivAtTop f).toReal * ∫ a, ((∂μ/∂ν) a).toReal * (κ.singularPart η a .univ).toReal ∂ν - + derivAtTop f * Measure.singularPart μ ν .univ := by + + derivAtTop f * μ.singularPart ν .univ := by gcongr norm_cast exact integral_f_rnDeriv_le_integral_add μ ν κ η hf hf_cvx hf_cont h_int (fun h ↦ (h3 h).2) _ = ∫ x, f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) x).toReal ∂(ν ⊗ₘ η) - + (derivAtTop f).toReal - * (((ν.withDensity (∂μ/∂ν)) ⊗ₘ κ).singularPart (ν ⊗ₘ η) .univ).toReal - + derivAtTop f * Measure.singularPart μ ν .univ := by + + (derivAtTop f).toReal * (((ν.withDensity (∂μ/∂ν)) ⊗ₘ κ).singularPart (ν ⊗ₘ η) .univ).toReal + + derivAtTop f * μ.singularPart ν .univ := by simp_rw [Kernel.singularPart_eq_singularPart_measure] rw [integral_rnDeriv_mul_singularPart _ _ _ _ .univ, Set.univ_prod_univ] _ = ∫ p, f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal ∂ν ⊗ₘ η @@ -505,8 +504,7 @@ lemma le_fDiv_compProd [CountableOrCountablyGenerated α β] (μ ν : Measure α congr by_cases h_top : derivAtTop f = ⊤ · simp only [h_top, EReal.toReal_top, EReal.coe_zero, zero_mul, zero_add] - rw [Measure.singularPart_eq_zero_of_ac (h3 h_top).1, - Measure.singularPart_eq_zero_of_ac] + rw [Measure.singularPart_eq_zero_of_ac (h3 h_top).1, Measure.singularPart_eq_zero_of_ac] · simp · rw [Kernel.Measure.absolutelyContinuous_compProd_iff] exact h3 h_top @@ -514,7 +512,7 @@ lemma le_fDiv_compProd [CountableOrCountablyGenerated α β] (μ ν : Measure α simp only [EReal.toReal_coe] rw [← EReal.coe_ennreal_toReal (measure_ne_top _ _), ← EReal.coe_ennreal_toReal (measure_ne_top _ _)] - conv_rhs => rw [Measure.haveLebesgueDecomposition_add μ ν] + conv_rhs => rw [μ.haveLebesgueDecomposition_add ν] rw [Measure.compProd_add_left, add_comm, Measure.singularPart_add] simp only [Measure.coe_add, Pi.add_apply] rw [ENNReal.toReal_add (measure_ne_top _ _) (measure_ne_top _ _)] @@ -541,8 +539,8 @@ lemma fDiv_fst_le [Nonempty β] [StandardBorelSpace β] (hf : StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) : fDiv f μ.fst ν.fst ≤ fDiv f μ ν := by - rw [← Measure.disintegrate μ μ.condKernel, ← Measure.disintegrate ν ν.condKernel, - Measure.fst_compProd, Measure.fst_compProd] + rw [← μ.disintegrate μ.condKernel, ← ν.disintegrate ν.condKernel, Measure.fst_compProd, + Measure.fst_compProd] exact le_fDiv_compProd μ.fst ν.fst μ.condKernel ν.condKernel hf hf_cvx hf_cont lemma fDiv_snd_le [Nonempty α] [StandardBorelSpace α] diff --git a/TestingLowerBounds/FDiv/CondFDiv.lean b/TestingLowerBounds/FDiv/CondFDiv.lean index 6e461c78..220bee9b 100644 --- a/TestingLowerBounds/FDiv/CondFDiv.lean +++ b/TestingLowerBounds/FDiv/CondFDiv.lean @@ -156,11 +156,11 @@ lemma condFDiv_eq_add [IsFiniteMeasure μ] [IsFiniteKernel κ] [IsFiniteKernel (hf : Integrable (fun a ↦ ∫ b, f ((∂κ a/∂η a) b).toReal ∂η a) μ) (h_deriv : derivAtTop f = ⊤ → ∀ᵐ a ∂μ, κ a ≪ η a) : condFDiv f κ η μ = (μ[fun a ↦ ∫ y, f ((∂κ a/∂η a) y).toReal ∂η a] : ℝ) - + (derivAtTop f).toReal * (μ[fun a ↦ ((κ a).singularPart (η a) Set.univ).toReal] : ℝ) := by + + (derivAtTop f).toReal * (μ[fun a ↦ ((κ a).singularPart (η a) .univ).toReal] : ℝ) := by rw [condFDiv_eq h_cvx hf_ae hf h_deriv] have : (fun x ↦ (fDiv f (κ x) (η x)).toReal) =ᵐ[μ] fun x ↦ ∫ y, f ((∂(κ x)/∂(η x)) y).toReal ∂(η x) - + (derivAtTop f * (κ x).singularPart (η x) Set.univ).toReal := by + + (derivAtTop f * (κ x).singularPart (η x) .univ).toReal := by have h_deriv' : ∀ᵐ a ∂μ, derivAtTop f = ⊤ → κ a ≪ η a := by simpa only [eventually_all] using h_deriv filter_upwards [hf_ae, h_deriv'] with x hx hx_deriv @@ -197,19 +197,17 @@ lemma condFDiv_self (κ : Kernel α β) (μ : Measure α) (hf_one : f 1 = 0) [Is @[simp] lemma condFDiv_zero_left [IsFiniteMeasure μ] [IsFiniteKernel η] : - condFDiv f 0 η μ = f 0 * ∫ a, ((η a) Set.univ).toReal ∂μ := by + condFDiv f 0 η μ = f 0 * ∫ a, ((η a) .univ).toReal ∂μ := by rw [condFDiv_eq' _ _] <;> simp_rw [Kernel.zero_apply, fDiv_zero_measure] · simp_rw [EReal.toReal_mul, EReal.toReal_coe, EReal.toReal_coe_ennreal] norm_cast exact integral_mul_left (f 0) _ · filter_upwards with _ - simp only [ne_eq, EReal.mul_eq_top, EReal.coe_ne_bot, false_and, EReal.coe_neg', - EReal.coe_ennreal_ne_bot, and_false, EReal.coe_ne_top, EReal.coe_ennreal_pos, - Measure.measure_univ_pos, EReal.coe_pos, EReal.coe_ennreal_eq_top_iff, measure_ne_top, - or_self, not_false_eq_true] + simp only [ne_eq, EReal.mul_eq_top, EReal.coe_ne_bot, false_and, EReal.coe_neg', and_false, + EReal.coe_ennreal_ne_bot, EReal.coe_ne_top, EReal.coe_ennreal_pos, Measure.measure_univ_pos, + EReal.coe_pos, EReal.coe_ennreal_eq_top_iff, measure_ne_top, or_self, not_false_eq_true] · simp_rw [EReal.toReal_mul, EReal.toReal_coe, EReal.toReal_coe_ennreal] - apply MeasureTheory.Integrable.const_mul - exact Kernel.IsFiniteKernel.integrable μ η MeasurableSet.univ + exact (Kernel.IsFiniteKernel.integrable μ η .univ).const_mul _ lemma condFDiv_zero_left' [IsProbabilityMeasure μ] [IsMarkovKernel η] : condFDiv f 0 η μ = f 0 := by @@ -229,14 +227,14 @@ lemma condFDiv_zero_measure : condFDiv f κ η 0 = 0 := by lemma condFDiv_of_isEmpty_left [IsEmpty α] : condFDiv f κ η μ = 0 := by suffices μ = 0 from this ▸ condFDiv_zero_measure ext s - exact Set.eq_empty_of_isEmpty s ▸ measure_empty + exact s.eq_empty_of_isEmpty ▸ measure_empty @[simp] lemma condFDiv_of_isEmpty_right [IsEmpty β] [IsFiniteKernel κ] (hf_one : f 1 = 0) : condFDiv f κ η μ = 0 := by suffices κ = η from by exact this ▸ condFDiv_self κ _ hf_one ext x s _ - simp [Set.eq_empty_of_isEmpty s] + simp [s.eq_empty_of_isEmpty] lemma condFDiv_ne_bot (κ η : Kernel α β) (μ : Measure α) : condFDiv f κ η μ ≠ ⊥ := by rw [condFDiv] @@ -259,7 +257,7 @@ lemma condFDiv_nonneg [IsMarkovKernel κ] [IsMarkovKernel η] simp [EReal.toReal_nonneg, h] lemma condFDiv_const' {ξ : Measure β} [IsFiniteMeasure ξ] (h_ne_bot : fDiv f μ ν ≠ ⊥) : - condFDiv f (Kernel.const β μ) (Kernel.const β ν) ξ = (fDiv f μ ν) * ξ Set.univ := by + condFDiv f (Kernel.const β μ) (Kernel.const β ν) ξ = (fDiv f μ ν) * ξ .univ := by by_cases hξ_zero : ξ = 0 · simp only [hξ_zero, condFDiv_zero_measure, Measure.coe_zero, Pi.zero_apply, EReal.coe_ennreal_zero, mul_zero] @@ -272,8 +270,7 @@ lemma condFDiv_const' {ξ : Measure β} [IsFiniteMeasure ξ] (h_ne_bot : fDiv f · rw [h_top, EReal.top_mul_of_pos _] · simp only [condFDiv_of_not_ae_finite, Kernel.const_apply, h_top, ne_eq, not_true_eq_false, eventually_false_iff_eq_bot, ae_eq_bot, hξ_zero, not_false_eq_true] - · simp only [EReal.coe_ennreal_pos, Measure.measure_univ_pos, ne_eq, hξ_zero, - not_false_eq_true] + · simp only [EReal.coe_ennreal_pos, Measure.measure_univ_pos, ne_eq, hξ_zero, not_false_eq_true] rw [condFDiv_eq' (by simp [h_top]) _] swap; simp [integrable_const_iff, lt_top_iff_ne_top] simp only [Kernel.const_apply, integral_const, smul_eq_mul, mul_comm, EReal.coe_mul] @@ -284,7 +281,7 @@ lemma condFDiv_const' {ξ : Measure β} [IsFiniteMeasure ξ] (h_ne_bot : fDiv f @[simp] lemma condFDiv_const {ξ : Measure β} [IsFiniteMeasure ξ] [IsFiniteMeasure μ] (h_cvx : ConvexOn ℝ (Ici 0) f) : - condFDiv f (Kernel.const β μ) (Kernel.const β ν) ξ = (fDiv f μ ν) * ξ Set.univ := + condFDiv f (Kernel.const β μ) (Kernel.const β ν) ξ = (fDiv f μ ν) * ξ .univ := condFDiv_const' (fDiv_ne_bot h_cvx) section CompProd @@ -330,7 +327,7 @@ lemma fDiv_compProd_left (μ : Measure α) [IsFiniteMeasure μ] rw [Measure.singularPart_eq_zero, Kernel.Measure.absolutelyContinuous_compProd_right_iff] exact h3 h_deriv · congr 1 - rw [EReal.coe_toReal h_deriv h_cvx.derivAtTop_ne_bot, integral_singularPart _ _ _ MeasurableSet.univ, + rw [EReal.coe_toReal h_deriv h_cvx.derivAtTop_ne_bot, integral_singularPart _ _ _ .univ, EReal.coe_ennreal_toReal, Set.univ_prod_univ] exact measure_ne_top _ _ @@ -345,7 +342,7 @@ lemma condFDiv_snd'_toReal_eq_ae [CountableOrCountablyGenerated β γ] {ξ : Ker (h_int : ∀ᵐ a ∂μ, ∀ᵐ b ∂ξ a, Integrable (fun x ↦ f ((∂κ (a, b)/∂η (a, b)) x).toReal) (η (a, b))) (h_int2 : ∀ᵐ a ∂μ, Integrable (fun b ↦ ∫ x, f ((∂κ (a, b)/∂η (a, b)) x).toReal ∂η (a, b)) (ξ a)) : - ∀ᵐ a ∂μ, (condFDiv f (Kernel.snd' κ a) (Kernel.snd' η a) (ξ a)).toReal = + ∀ᵐ a ∂μ, (condFDiv f (κ.snd' a) (η.snd' a) (ξ a)).toReal = ∫ b, (fDiv f (κ (a, b)) (η (a, b))).toReal ∂ξ a := by simp_rw [← Kernel.snd'_apply] at h_int2 h_int h_ac ⊢ rw [← eventually_all] at h_ac @@ -360,7 +357,7 @@ lemma condFDiv_kernel_snd'_integrable_iff [CountableOrCountablyGenerated (α × (h_int2 : ∀ᵐ a ∂μ, Integrable (fun b ↦ ∫ x, f ((∂κ (a, b)/∂η (a, b)) x).toReal ∂η (a, b)) (ξ a)) (hf_meas : StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) (hf_one : f 1 = 0) : - Integrable (fun a ↦ (condFDiv f (Kernel.snd' κ a) (Kernel.snd' η a) (ξ a)).toReal) μ ↔ + Integrable (fun a ↦ (condFDiv f (κ.snd' a) (η.snd' a) (ξ a)).toReal) μ ↔ Integrable (fun a ↦ ∫ b, |∫ x, f ((∂κ (a, b)/∂η (a, b)) x).toReal ∂η (a, b)| ∂ξ a) μ := by by_cases h_empty : Nonempty α swap; simp only [not_nonempty_iff.mp h_empty, Integrable.of_isEmpty] @@ -379,13 +376,13 @@ lemma condFDiv_kernel_snd'_integrable_iff [CountableOrCountablyGenerated (α × _ ≤ |∫ (x : γ), f ((∂κ (a, b)/∂η (a, b)) x).toReal ∂η (a, b) - (fDiv f (κ (a, b)) (η (a, b))).toReal| := by exact abs_abs_sub_abs_le_abs_sub _ _ - _ = |(derivAtTop f).toReal| * ((κ (a, b)).singularPart (η (a, b)) Set.univ).toReal := by + _ = |(derivAtTop f).toReal| * ((κ (a, b)).singularPart (η (a, b)) .univ).toReal := by rw [hb_ereal_add, sub_add_cancel_left, abs_neg, abs_mul, ENNReal.abs_toReal] - _ ≤ |(derivAtTop f).toReal| * ((κ (a, b)) Set.univ).toReal := by + _ ≤ |(derivAtTop f).toReal| * ((κ (a, b)) .univ).toReal := by apply mul_le_mul_of_nonneg_left _ (abs_nonneg _) gcongr - · exact measure_ne_top (κ (a, b)) Set.univ - · exact Measure.singularPart_le (κ (a, b)) (η (a, b)) Set.univ + · exact measure_ne_top (κ (a, b)) .univ + · exact (κ (a, b)).singularPart_le (η (a, b)) .univ _ = _ := by rw [measure_univ, ENNReal.one_toReal, mul_one] have h_int2' : ∀ᵐ a ∂μ, Integrable (fun b ↦ (fDiv f (κ (a, b)) (η (a, b))).toReal) (ξ a) := by filter_upwards [eventually_all.mpr h_ac, h_int, h_int2] with a ha_ae ha_int ha_int2 @@ -406,14 +403,14 @@ lemma condFDiv_kernel_snd'_integrable_iff [CountableOrCountablyGenerated (α × refine integral_mono_ae ha_int2.abs (integrable_add_const_iff.mpr ha_int2') ?_ filter_upwards [ha_le] with a hb_le using by linarith apply Integrable.congr (f := fun a ↦ ∫ b, (fDiv f (κ (a, b)) (η (a, b))).toReal ∂ξ a - + ((ξ a) Set.univ).toReal * |(derivAtTop f).toReal|) + + ((ξ a) .univ).toReal * |(derivAtTop f).toReal|) swap · filter_upwards [h_int2'] with a ha_int2' rw [integral_add ha_int2' (integrable_const _), integral_const, smul_eq_mul] -- we already know the integrability of the integral (hp `h`) and the other part is just a -- constant times a finite Kernel applied to a fixed set, so it's easy to show that -- it's integrable - exact h.add (Integrable.Kernel _ MeasurableSet.univ |>.mul_const _) + exact h.add (Integrable.Kernel _ .univ |>.mul_const _) · -- using `h_le'` we reduce the problem to the integrability of a sum of an integral and -- `f'(∞) * (ξ x) (univ)` apply Integrable.mono' (g := fun a ↦ ∫ b, @@ -427,12 +424,12 @@ lemma condFDiv_kernel_snd'_integrable_iff [CountableOrCountablyGenerated (α × refine integral_mono_ae ha_int2' (integrable_add_const_iff.mpr <| ha_int2.abs) ?_ filter_upwards [ha_le] with a hb_le using by linarith apply Integrable.congr (f := fun a ↦ ∫ b, |∫ x, f ((∂κ (a, b)/∂η (a, b)) x).toReal ∂η (a, b)| - ∂ξ a + ((ξ a) Set.univ).toReal * |(derivAtTop f).toReal|) + ∂ξ a + ((ξ a) .univ).toReal * |(derivAtTop f).toReal|) swap · filter_upwards [h_int2] with a ha_int2 rw [integral_add ha_int2.abs (integrable_const _), integral_const, smul_eq_mul] -- same as above - exact h.add (Integrable.Kernel _ MeasurableSet.univ |>.mul_const _) + exact h.add (Integrable.Kernel _ .univ |>.mul_const _) lemma condFDiv_kernel_fst'_integrable_iff [CountableOrCountablyGenerated (α × β) γ] {μ : Measure β} [IsFiniteMeasure μ] {ξ : Kernel β α} [IsFiniteKernel ξ] @@ -442,7 +439,7 @@ lemma condFDiv_kernel_fst'_integrable_iff [CountableOrCountablyGenerated (α × (h_int2 : ∀ᵐ b ∂μ, Integrable (fun a ↦ ∫ x, f ((∂κ (a, b)/∂η (a, b)) x).toReal ∂η (a, b)) (ξ b)) (hf_meas : StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) (hf_one : f 1 = 0) : - Integrable (fun b ↦ (condFDiv f (Kernel.fst' κ b) (Kernel.fst' η b) (ξ b)).toReal) μ ↔ + Integrable (fun b ↦ (condFDiv f (κ.fst' b) (η.fst' b) (ξ b)).toReal) μ ↔ Integrable (fun b ↦ ∫ a, |∫ x, f ((∂κ (a, b)/∂η (a, b)) x).toReal ∂η (a, b)| ∂ξ b) μ := by simp_rw [← Kernel.snd'_swapRight] exact condFDiv_kernel_snd'_integrable_iff h_ac h_int h_int2 hf_meas hf_cvx hf_cont hf_one @@ -453,8 +450,8 @@ lemma condFDiv_compProd_meas_eq_top [CountableOrCountablyGenerated (α × β) γ (hf_meas : StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) (hf_one : f 1 = 0) : condFDiv f κ η (μ ⊗ₘ ξ) = ⊤ - ↔ ¬ (∀ᵐ a ∂μ, condFDiv f (Kernel.snd' κ a) (Kernel.snd' η a) (ξ a) ≠ ⊤) ∨ - ¬ Integrable (fun x ↦ (condFDiv f (Kernel.snd' κ x) (Kernel.snd' η x) (ξ x)).toReal) μ := by + ↔ ¬ (∀ᵐ a ∂μ, condFDiv f (κ.snd' a) (η.snd' a) (ξ a) ≠ ⊤) ∨ + ¬ Integrable (fun x ↦ (condFDiv f (κ.snd' x) (η.snd' x) (ξ x)).toReal) μ := by by_cases h_empty : Nonempty α swap; simp only [isEmpty_prod, not_nonempty_iff.mp h_empty, true_or, condFDiv_of_isEmpty_left, EReal.zero_ne_top, IsEmpty.forall_iff, Eventually.of_forall, not_true_eq_false, @@ -464,13 +461,13 @@ lemma condFDiv_compProd_meas_eq_top [CountableOrCountablyGenerated (α × β) γ constructor · by_cases h_ac : derivAtTop f = ⊤ → ∀ᵐ x ∂(μ ⊗ₘ ξ), κ x ≪ η x swap - · rw [Measure.ae_compProd_iff (Kernel.measurableSet_absolutelyContinuous _ _)] at h_ac + · rw [Measure.ae_compProd_iff (κ.measurableSet_absolutelyContinuous _)] at h_ac simp_rw [condFDiv_ne_top_iff hf_cvx, Kernel.snd'_apply, eventually_and, not_and_or, eventually_all] intro; left; right; right exact h_ac have h_ac' := h_ac - rw [Measure.ae_compProd_iff (Kernel.measurableSet_absolutelyContinuous _ _)] at h_ac + rw [Measure.ae_compProd_iff (κ.measurableSet_absolutelyContinuous _)] at h_ac by_cases h_int : ∀ᵐ a ∂μ, ∀ᵐ b ∂ξ a, Integrable (fun y ↦ f ((∂κ (a, b)/∂η (a, b)) y).toReal) (η (a, b)) swap; · simp only [not_eventually, ne_eq, condFDiv_ne_top_iff hf_cvx, Kernel.snd'_apply, @@ -499,7 +496,7 @@ lemma condFDiv_compProd_meas_eq_top [CountableOrCountablyGenerated (α × β) γ contrapose! h rcases h with ⟨h_int1, ⟨h_int2, h_ac⟩⟩ rw [Measure.ae_compProd_iff (measurableSet_integrable_f_rnDeriv κ η hf_meas)] at h_int1 - rw [Measure.ae_compProd_iff (Kernel.measurableSet_absolutelyContinuous _ _)] at h_ac + rw [Measure.ae_compProd_iff (κ.measurableSet_absolutelyContinuous _)] at h_ac rw [Measure.integrable_compProd_iff h_int2.aestronglyMeasurable] at h_int2 simp_all only [implies_true, forall_true_left, norm_eq_abs] refine ⟨?_, condFDiv_kernel_snd'_integrable_iff h_ac h_int1 h_int2.1 hf_meas hf_cvx hf_cont @@ -516,7 +513,7 @@ lemma condFDiv_compProd_meas [CountableOrCountablyGenerated (α × β) γ] [IsFi (hf_cont : ContinuousOn f (Ici 0)) (hf_one : f 1 = 0) (h_top : condFDiv f κ η (μ ⊗ₘ ξ) ≠ ⊤) : condFDiv f κ η (μ ⊗ₘ ξ) - = ∫ x, (condFDiv f (Kernel.snd' κ x) (Kernel.snd' η x) (ξ x)).toReal ∂μ := by + = ∫ x, (condFDiv f (κ.snd' x) (η.snd' x) (ξ x)).toReal ∂μ := by by_cases h_empty : Nonempty α swap; simp only [isEmpty_prod, not_nonempty_iff.mp h_empty, true_or, condFDiv_of_isEmpty_left, integral_of_isEmpty, EReal.coe_zero] diff --git a/TestingLowerBounds/FDiv/IntegralRnDerivSingularPart.lean b/TestingLowerBounds/FDiv/IntegralRnDerivSingularPart.lean index 47cfaf1d..bb6ec8ee 100644 --- a/TestingLowerBounds/FDiv/IntegralRnDerivSingularPart.lean +++ b/TestingLowerBounds/FDiv/IntegralRnDerivSingularPart.lean @@ -50,29 +50,28 @@ lemma setLIntegral_rnDeriv_mul_withDensity (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] {s : Set α} (hs : MeasurableSet s) {t : Set β} (ht : MeasurableSet t) : - ∫⁻ a in s, (∂μ/∂ν) a * Kernel.withDensity η (Kernel.rnDeriv κ η) a t ∂ν + ∫⁻ a in s, (∂μ/∂ν) a * η.withDensity (κ.rnDeriv η) a t ∂ν = (ν ⊗ₘ η).withDensity (∂(μ ⊗ₘ κ)/∂(ν ⊗ₘ η)) (s ×ˢ t) := by - have : ∀ a, Kernel.withDensity η (Kernel.rnDeriv κ η) a t - = ∫⁻ y in t, Kernel.rnDeriv κ η a y ∂(η a) := by + have : ∀ a, η.withDensity (κ.rnDeriv η) a t = ∫⁻ y in t, κ.rnDeriv η a y ∂(η a) := by intro a rw [Kernel.withDensity_apply'] - exact Kernel.measurable_rnDeriv _ _ + exact κ.measurable_rnDeriv _ simp_rw [this] rw [withDensity_apply _ (hs.prod ht), Measure.setLIntegral_compProd (Measure.measurable_rnDeriv _ _) hs ht] refine setLIntegral_congr_fun hs ?_ - filter_upwards [Kernel.rnDeriv_measure_compProd' μ ν κ η] with a ha _ - rw [← lintegral_const_mul _ (Kernel.measurable_rnDeriv_right _ _ _)] + filter_upwards [κ.rnDeriv_measure_compProd' μ ν η] with a ha _ + rw [← lintegral_const_mul _ (κ.measurable_rnDeriv_right _ _)] refine setLIntegral_congr_fun ht ?_ - filter_upwards [ha, Kernel.rnDeriv_eq_rnDeriv_measure κ η a] with b hb hb' _ + filter_upwards [ha, κ.rnDeriv_eq_rnDeriv_measure η a] with b hb hb' _ rw [hb, hb'] lemma lintegral_rnDeriv_mul_withDensity (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] {t : Set β} (ht : MeasurableSet t) : - ∫⁻ a, (∂μ/∂ν) a * Kernel.withDensity η (Kernel.rnDeriv κ η) a t ∂ν - = (ν ⊗ₘ η).withDensity (∂(μ ⊗ₘ κ)/∂(ν ⊗ₘ η)) (Set.univ ×ˢ t) := by - rw [← setLIntegral_rnDeriv_mul_withDensity _ _ _ _ MeasurableSet.univ ht, setLIntegral_univ] + ∫⁻ a, (∂μ/∂ν) a * η.withDensity (κ.rnDeriv η) a t ∂ν + = (ν ⊗ₘ η).withDensity (∂(μ ⊗ₘ κ)/∂(ν ⊗ₘ η)) (.univ ×ˢ t) := by + rw [← setLIntegral_rnDeriv_mul_withDensity _ _ _ _ .univ ht, setLIntegral_univ] lemma setLIntegral_rnDeriv_mul_singularPart (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] @@ -82,28 +81,27 @@ lemma setLIntegral_rnDeriv_mul_singularPart = ((ν.withDensity (∂μ/∂ν)) ⊗ₘ κ).singularPart (ν ⊗ₘ η) (s ×ˢ t) := by rw [singularPart_compProd', Measure.coe_add, Pi.add_apply, Measure.compProd_apply (hs.prod ht), Measure.compProd_apply (hs.prod ht), lintegral_measure_prod_mk_left (by simp) hs, - lintegral_measure_prod_mk_left (by simp) hs, Measure.singularPart_withDensity ν] + lintegral_measure_prod_mk_left (by simp) hs, ν.singularPart_withDensity] simp only [Measure.restrict_zero, lintegral_zero_measure, zero_add] - have : Measure.withDensity ν (∂Measure.withDensity ν (∂μ/∂ν)/∂ν) - = Measure.withDensity ν (∂μ/∂ν) := - withDensity_congr_ae (Measure.rnDeriv_withDensity _ (Measure.measurable_rnDeriv _ _)) + have : ν.withDensity (∂ν.withDensity (∂μ/∂ν)/∂ν) = ν.withDensity (∂μ/∂ν) := + withDensity_congr_ae (ν.rnDeriv_withDensity (μ.measurable_rnDeriv _)) rw [this, ← setLIntegral_rnDeriv_mul (μ := ν.withDensity (∂μ/∂ν)) (ν := ν) (withDensity_absolutelyContinuous _ _) (Kernel.measurable_coe _ ht).aemeasurable hs] refine setLIntegral_congr_fun hs ?_ - filter_upwards [Measure.rnDeriv_withDensity _ (Measure.measurable_rnDeriv μ ν)] with x hx _ + filter_upwards [ν.rnDeriv_withDensity (μ.measurable_rnDeriv ν)] with x hx _ rw [hx, Kernel.singularPart_eq_singularPart_measure] lemma lintegral_rnDeriv_mul_singularPart (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] {t : Set β} (ht : MeasurableSet t) : ∫⁻ a, (∂μ/∂ν) a * (κ a).singularPart (η a) t ∂ν - = ((ν.withDensity (∂μ/∂ν)) ⊗ₘ κ).singularPart (ν ⊗ₘ η) (Set.univ ×ˢ t) := by - rw [← setLIntegral_rnDeriv_mul_singularPart _ _ _ _ MeasurableSet.univ ht, setLIntegral_univ] + = ((ν.withDensity (∂μ/∂ν)) ⊗ₘ κ).singularPart (ν ⊗ₘ η) (.univ ×ˢ t) := by + rw [← setLIntegral_rnDeriv_mul_singularPart _ _ _ _ .univ ht, setLIntegral_univ] lemma setLIntegral_withDensity (μ : Measure α) [IsFiniteMeasure μ] (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] {s : Set α} (hs : MeasurableSet s) {t : Set β} (ht : MeasurableSet t) : - ∫⁻ a in s, Kernel.withDensity η (Kernel.rnDeriv κ η) a t ∂μ + ∫⁻ a in s, η.withDensity (κ.rnDeriv η) a t ∂μ = (μ ⊗ₘ η).withDensity (∂(μ ⊗ₘ κ)/∂(μ ⊗ₘ η)) (s ×ˢ t) := by rw [← setLIntegral_rnDeriv_mul_withDensity μ μ κ η hs ht] refine setLIntegral_congr_fun hs ?_ @@ -121,73 +119,70 @@ lemma setLIntegral_singularPart (μ : Measure α) [IsFiniteMeasure μ] lemma lintegral_withDensity (μ : Measure α) [IsFiniteMeasure μ] (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] {s : Set β} (hs : MeasurableSet s) : - ∫⁻ a, Kernel.withDensity η (Kernel.rnDeriv κ η) a s ∂μ - = (μ ⊗ₘ η).withDensity (∂(μ ⊗ₘ κ)/∂(μ ⊗ₘ η)) (Set.univ ×ˢ s) := by - rw [← setLIntegral_univ, setLIntegral_withDensity _ _ _ MeasurableSet.univ hs] + ∫⁻ a, η.withDensity (κ.rnDeriv η) a s ∂μ + = (μ ⊗ₘ η).withDensity (∂(μ ⊗ₘ κ)/∂(μ ⊗ₘ η)) (.univ ×ˢ s) := by + rw [← setLIntegral_univ, setLIntegral_withDensity _ _ _ .univ hs] lemma lintegral_singularPart (μ : Measure α) [IsFiniteMeasure μ] (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] {s : Set β} (hs : MeasurableSet s) : - ∫⁻ a, (κ a).singularPart (η a) s ∂μ = (μ ⊗ₘ κ).singularPart (μ ⊗ₘ η) (Set.univ ×ˢ s) := by - rw [← setLIntegral_univ, setLIntegral_singularPart _ _ _ MeasurableSet.univ hs] + ∫⁻ a, (κ a).singularPart (η a) s ∂μ = (μ ⊗ₘ κ).singularPart (μ ⊗ₘ η) (.univ ×ˢ s) := by + rw [← setLIntegral_univ, setLIntegral_singularPart _ _ _ .univ hs] lemma integrable_rnDeriv_mul_withDensity (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] : - Integrable (fun x ↦ - ((∂μ/∂ν) x).toReal * (Kernel.withDensity η (Kernel.rnDeriv κ η) x Set.univ).toReal) ν := by + Integrable (fun x ↦ ((∂μ/∂ν) x).toReal * (η.withDensity (κ.rnDeriv η) x .univ).toReal) ν := by simp_rw [← ENNReal.toReal_mul] refine integrable_toReal_of_lintegral_ne_top ?_ (ne_of_lt ?_) - · refine AEMeasurable.mul ?_ ?_ - · exact (Measure.measurable_rnDeriv _ _).aemeasurable - · exact (Kernel.measurable_coe _ MeasurableSet.univ).aemeasurable - rw [lintegral_rnDeriv_mul_withDensity _ _ _ _ MeasurableSet.univ] + · refine (μ.measurable_rnDeriv _).aemeasurable.mul ?_ + exact (Kernel.measurable_coe _ .univ).aemeasurable + rw [lintegral_rnDeriv_mul_withDensity _ _ _ _ .univ] exact measure_lt_top _ _ lemma integrable_rnDeriv_mul_singularPart (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] : - Integrable (fun x ↦ ((∂μ/∂ν) x).toReal * ((κ x).singularPart (η x) Set.univ).toReal) ν := by + Integrable (fun x ↦ ((∂μ/∂ν) x).toReal * ((κ x).singularPart (η x) .univ).toReal) ν := by simp_rw [← ENNReal.toReal_mul] refine integrable_toReal_of_lintegral_ne_top ?_ (ne_of_lt ?_) · simp_rw [← Kernel.singularPart_eq_singularPart_measure] - refine AEMeasurable.mul ?_ ?_ - · exact (Measure.measurable_rnDeriv _ _).aemeasurable - · exact (Kernel.measurable_coe _ MeasurableSet.univ).aemeasurable - rw [lintegral_rnDeriv_mul_singularPart _ _ _ _ MeasurableSet.univ] + refine (μ.measurable_rnDeriv _).aemeasurable.mul ?_ + exact (Kernel.measurable_coe _ .univ).aemeasurable + rw [lintegral_rnDeriv_mul_singularPart _ _ _ _ .univ] exact measure_lt_top _ _ lemma integrable_singularPart [IsFiniteMeasure μ] [IsFiniteKernel κ] [IsFiniteKernel η] : - Integrable (fun x ↦ ((κ x).singularPart (η x) Set.univ).toReal) μ := by + Integrable (fun x ↦ ((κ x).singularPart (η x) .univ).toReal) μ := by refine integrable_toReal_of_lintegral_ne_top ?_ (ne_of_lt ?_) · simp_rw [← Kernel.singularPart_eq_singularPart_measure] - exact (Kernel.measurable_coe _ MeasurableSet.univ).aemeasurable - rw [lintegral_singularPart _ _ _ MeasurableSet.univ] + exact (Kernel.measurable_coe _ .univ).aemeasurable + rw [lintegral_singularPart _ _ _ .univ] exact measure_lt_top _ _ lemma setIntegral_rnDeriv_mul_withDensity (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] {s : Set α} (hs : MeasurableSet s) {t : Set β} (ht : MeasurableSet t) : - ∫ a in s, ((∂μ/∂ν) a).toReal *(Kernel.withDensity η (Kernel.rnDeriv κ η) a t).toReal ∂ν + ∫ a in s, ((∂μ/∂ν) a).toReal *(η.withDensity (κ.rnDeriv η) a t).toReal ∂ν = ((ν ⊗ₘ η).withDensity (∂(μ ⊗ₘ κ)/∂(ν ⊗ₘ η)) (s ×ˢ t)).toReal := by rw [← setLIntegral_rnDeriv_mul_withDensity _ _ _ _ hs ht] simp_rw [← ENNReal.toReal_mul] rw [integral_toReal] · refine AEMeasurable.mul ?_ ?_ - · exact (Measure.measurable_rnDeriv _ _).aemeasurable + · exact (μ.measurable_rnDeriv _).aemeasurable · exact (Kernel.measurable_coe _ ht).aemeasurable · refine ae_restrict_of_ae ?_ - filter_upwards [Measure.rnDeriv_lt_top μ ν] with a ha + filter_upwards [μ.rnDeriv_lt_top ν] with a ha exact ENNReal.mul_lt_top ha (measure_lt_top _ _) lemma integral_rnDeriv_mul_withDensity (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] {t : Set β} (ht : MeasurableSet t) : - ∫ a, ((∂μ/∂ν) a).toReal *(Kernel.withDensity η (Kernel.rnDeriv κ η) a t).toReal ∂ν - = ((ν ⊗ₘ η).withDensity (∂(μ ⊗ₘ κ)/∂(ν ⊗ₘ η)) (Set.univ ×ˢ t)).toReal := by - rw [← setIntegral_rnDeriv_mul_withDensity μ ν κ η MeasurableSet.univ ht, integral_univ] + ∫ a, ((∂μ/∂ν) a).toReal *(η.withDensity (κ.rnDeriv η) a t).toReal ∂ν + = ((ν ⊗ₘ η).withDensity (∂(μ ⊗ₘ κ)/∂(ν ⊗ₘ η)) (.univ ×ˢ t)).toReal := by + rw [← setIntegral_rnDeriv_mul_withDensity μ ν κ η .univ ht, integral_univ] lemma setIntegral_rnDeriv_mul_singularPart (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] @@ -200,19 +195,18 @@ lemma setIntegral_rnDeriv_mul_singularPart rw [integral_toReal] · simp_rw [← Kernel.singularPart_eq_singularPart_measure] refine AEMeasurable.mul ?_ ?_ - · exact (Measure.measurable_rnDeriv _ _).aemeasurable + · exact (μ.measurable_rnDeriv _).aemeasurable · exact (Kernel.measurable_coe _ ht).aemeasurable · refine ae_restrict_of_ae ?_ - filter_upwards [Measure.rnDeriv_lt_top μ ν] with a ha - exact ENNReal.mul_lt_top ha (measure_lt_top _ _) + filter_upwards [μ.rnDeriv_lt_top ν] with a ha using ENNReal.mul_lt_top ha (measure_lt_top _ _) lemma integral_rnDeriv_mul_singularPart (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] {t : Set β} (ht : MeasurableSet t) : ∫ a, ((∂μ/∂ν) a).toReal * ((κ a).singularPart (η a) t).toReal ∂ν - = (((ν.withDensity (∂μ/∂ν)) ⊗ₘ κ).singularPart (ν ⊗ₘ η) (Set.univ ×ˢ t)).toReal := by - rw [← setIntegral_rnDeriv_mul_singularPart μ ν κ η MeasurableSet.univ ht, integral_univ] + = (((ν.withDensity (∂μ/∂ν)) ⊗ₘ κ).singularPart (ν ⊗ₘ η) (.univ ×ˢ t)).toReal := by + rw [← setIntegral_rnDeriv_mul_singularPart μ ν κ η .univ ht, integral_univ] lemma setIntegral_singularPart (μ : Measure α) [IsFiniteMeasure μ] (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] @@ -228,8 +222,8 @@ lemma integral_singularPart (μ : Measure α) [IsFiniteMeasure μ] (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] {s : Set β} (hs : MeasurableSet s) : ∫ a, ((κ a).singularPart (η a) s).toReal ∂μ - = ((μ ⊗ₘ κ).singularPart (μ ⊗ₘ η) (Set.univ ×ˢ s)).toReal := by - rw [← integral_univ, setIntegral_singularPart _ _ _ MeasurableSet.univ hs] + = ((μ ⊗ₘ κ).singularPart (μ ⊗ₘ η) (.univ ×ˢ s)).toReal := by + rw [← integral_univ, setIntegral_singularPart _ _ _ .univ hs] end IntegralRnDeriv @@ -239,25 +233,23 @@ lemma Integrable.Kernel [IsFiniteKernel κ] [IsFiniteMeasure μ] (s : Set β) (h Integrable (fun x ↦ ((κ x) s).toReal) μ := by obtain ⟨C, ⟨hC_finite, hC_le⟩⟩ := IsFiniteKernel.exists_univ_le (κ := κ) apply (integrable_const C.toReal).mono' -· exact Kernel.measurable_coe κ hs |>.ennreal_toReal.aestronglyMeasurable +· exact κ.measurable_coe hs |>.ennreal_toReal.aestronglyMeasurable simp_rw [Real.norm_eq_abs, abs_eq_self.mpr ENNReal.toReal_nonneg, ENNReal.toReal_le_toReal (measure_ne_top _ _) (lt_top_iff_ne_top.mp hC_finite)] -exact .of_forall <| fun x ↦ (κ x).mono (Set.subset_univ s) |>.trans (hC_le x) +exact .of_forall <| fun x ↦ (κ x).mono s.subset_univ |>.trans (hC_le x) lemma Measure.rnDeriv_measure_compProd_Kernel_withDensity [CountableOrCountablyGenerated α β] (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] : - (∂μ ⊗ₘ (Kernel.withDensity η (Kernel.rnDeriv κ η))/∂ν ⊗ₘ η) - =ᵐ[ν ⊗ₘ η] (∂μ ⊗ₘ κ/∂ν ⊗ₘ η) := by - let κ' := Kernel.withDensity η (Kernel.rnDeriv κ η) - have h_ae : ∀ᵐ p ∂(ν ⊗ₘ η), Kernel.rnDeriv κ' η p.1 p.2 = Kernel.rnDeriv κ η p.1 p.2 := by + (∂μ ⊗ₘ (η.withDensity (κ.rnDeriv η))/∂ν ⊗ₘ η) =ᵐ[ν ⊗ₘ η] (∂μ ⊗ₘ κ/∂ν ⊗ₘ η) := by + let κ' := η.withDensity (κ.rnDeriv η) + have h_ae : ∀ᵐ p ∂(ν ⊗ₘ η), κ'.rnDeriv η p.1 p.2 = κ.rnDeriv η p.1 p.2 := by refine Kernel.ENNReal.ae_eq_compProd_of_forall_ae_eq ν η ?_ ?_ ?_ - · exact Kernel.measurable_rnDeriv _ _ - · exact Kernel.measurable_rnDeriv _ _ - · refine fun a ↦ Kernel.rnDeriv_withDensity η ?_ a - exact Kernel.measurable_rnDeriv _ _ - filter_upwards [Kernel.rnDeriv_measure_compProd μ ν κ η, - Kernel.rnDeriv_measure_compProd μ ν κ' η, h_ae] with p h1 h2 h3 + · exact κ'.measurable_rnDeriv _ + · exact κ.measurable_rnDeriv _ + · exact fun a ↦ η.rnDeriv_withDensity (κ.measurable_rnDeriv _) a + filter_upwards [κ.rnDeriv_measure_compProd μ ν η, + κ'.rnDeriv_measure_compProd μ ν η, h_ae] with p h1 h2 h3 rw [h1, h2, h3] end ProbabilityTheory diff --git a/TestingLowerBounds/FDiv/Trim.lean b/TestingLowerBounds/FDiv/Trim.lean index c23612a9..140385ac 100644 --- a/TestingLowerBounds/FDiv/Trim.lean +++ b/TestingLowerBounds/FDiv/Trim.lean @@ -123,6 +123,6 @@ lemma fDiv_trim_le [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hm : m ≤ mα) refine (fDiv_add_measure_le _ _ _ hf hf_cvx).trans ?_ refine add_le_add ?_ ?_ · exact fDiv_trim_le_of_ac hm (withDensity_absolutelyContinuous ν (∂μ/∂ν)) hf hf_cvx hf_cont - · rw [trim_measurableSet_eq hm MeasurableSet.univ] + · rw [trim_measurableSet_eq hm .univ] end ProbabilityTheory diff --git a/TestingLowerBounds/ForMathlib/LogLikelihoodRatioCompProd.lean b/TestingLowerBounds/ForMathlib/LogLikelihoodRatioCompProd.lean index 606ce8dc..89fecf8d 100644 --- a/TestingLowerBounds/ForMathlib/LogLikelihoodRatioCompProd.lean +++ b/TestingLowerBounds/ForMathlib/LogLikelihoodRatioCompProd.lean @@ -187,7 +187,7 @@ lemma ae_compProd_integrable_llr_iff [CountableOrCountablyGenerated (α × β) Kernel.ae_compProd_iff (measurableSet_integrable_llr κ η) _ ↔ ∀ᵐ a ∂μ, ∀ᵐ b ∂ξ a, Integrable (llr (κ (a, b)) (η (a, b))) (κ (a, b)) := by apply Filter.eventually_congr - rw [Measure.ae_compProd_iff (Kernel.measurableSet_absolutelyContinuous _ _)] at h_ac + rw [Measure.ae_compProd_iff (κ.measurableSet_absolutelyContinuous _)] at h_ac filter_upwards [h_ac] with a ha apply Filter.eventually_congr filter_upwards [ha] with b hb using (integrable_rnDeriv_smul_iff hb) diff --git a/TestingLowerBounds/ForMathlib/RadonNikodym.lean b/TestingLowerBounds/ForMathlib/RadonNikodym.lean index c09e8203..9205d8b1 100644 --- a/TestingLowerBounds/ForMathlib/RadonNikodym.lean +++ b/TestingLowerBounds/ForMathlib/RadonNikodym.lean @@ -24,7 +24,7 @@ variable {α γ : Type*} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} lemma singularPart_self [CountableOrCountablyGenerated α γ] (κ : Kernel α γ) [IsFiniteKernel κ] : - Kernel.singularPart κ κ = 0 := by + κ.singularPart κ = 0 := by ext a : 1 rw [zero_apply, singularPart_eq_zero_iff_absolutelyContinuous] @@ -38,13 +38,12 @@ lemma Measure.mutuallySingular_compProd_left [SFinite μ] [SFinite ν] (hμν : μ ⟂ₘ ν) (κ η : Kernel α γ) [IsSFiniteKernel κ] [IsSFiniteKernel η] : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η := by let s := hμν.nullSet - have hs_prod : MeasurableSet (s ×ˢ (univ : Set γ)) := - hμν.measurableSet_nullSet.prod MeasurableSet.univ + have hs_prod : MeasurableSet (s ×ˢ (univ : Set γ)) := hμν.measurableSet_nullSet.prod .univ refine ⟨s ×ˢ univ, hs_prod, ?_⟩ - rw [Measure.compProd_apply_prod hμν.measurableSet_nullSet MeasurableSet.univ, compl_prod_eq_union] + rw [Measure.compProd_apply_prod hμν.measurableSet_nullSet .univ, compl_prod_eq_union] simp only [Measure.MutuallySingular.restrict_nullSet, lintegral_zero_measure, compl_univ, prod_empty, union_empty, true_and] - rw [Measure.compProd_apply_prod hμν.measurableSet_nullSet.compl MeasurableSet.univ] + rw [Measure.compProd_apply_prod hμν.measurableSet_nullSet.compl .univ] simp lemma Measure.mutuallySingular_compProd_right [CountableOrCountablyGenerated α γ] @@ -83,7 +82,7 @@ lemma Measure.mutuallySingular_of_mutuallySingular_compProd {ξ : Measure α} have hs := h.measurableSet_nullSet have hμ_zero:= h.measure_nullSet have hν_zero := h.measure_compl_nullSet - rw [Measure.compProd_apply, MeasureTheory.lintegral_eq_zero_iff'] at hμ_zero hν_zero + rw [Measure.compProd_apply, lintegral_eq_zero_iff'] at hμ_zero hν_zero rotate_left · exact measurable_kernel_prod_mk_left hs.compl |>.aemeasurable · exact measurable_kernel_prod_mk_left hs |>.aemeasurable @@ -106,7 +105,7 @@ lemma Measure.mutuallySingular_compProd_iff_of_same_right (μ ν : Measure α) [ rw [← Measure.withDensity_rnDeriv_eq_zero] have hh := mutuallySingular_of_mutuallySingular_compProd h ?_ ?_ (ξ := ν.withDensity (∂μ/∂ν)) rotate_left - · exact Measure.absolutelyContinuous_of_le (Measure.withDensity_rnDeriv_le μ ν) + · 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) @@ -156,19 +155,19 @@ section Unique variable {ξ : Kernel α γ} {f : α → γ → ℝ≥0∞} -lemma eq_rnDeriv_measure [IsFiniteKernel η] (h : κ = Kernel.withDensity η f + ξ) +lemma eq_rnDeriv_measure [IsFiniteKernel η] (h : κ = η.withDensity f + ξ) (hf : Measurable (Function.uncurry f)) (hξ : ∀ a, ξ a ⟂ₘ η a) (a : α) : f a =ᵐ[η a] ∂(κ a)/∂(η a) := by have : κ a = ξ a + (η a).withDensity (f a) := by - rw [h, coe_add, Pi.add_apply, Kernel.withDensity_apply _ hf, add_comm] + rw [h, coe_add, Pi.add_apply, η.withDensity_apply hf, add_comm] exact (κ a).eq_rnDeriv₀ (hf.comp measurable_prod_mk_left).aemeasurable (hξ a) this lemma eq_singularPart_measure [IsFiniteKernel η] - (h : κ = Kernel.withDensity η f + ξ) + (h : κ = η.withDensity f + ξ) (hf : Measurable (Function.uncurry f)) (hξ : ∀ a, ξ a ⟂ₘ η a) (a : α) : ξ a = (κ a).singularPart (η a) := by have : κ a = ξ a + (η a).withDensity (f a) := by - rw [h, coe_add, Pi.add_apply, Kernel.withDensity_apply _ hf, add_comm] + rw [h, coe_add, Pi.add_apply, η.withDensity_apply hf, add_comm] exact (κ a).eq_singularPart (hf.comp measurable_prod_mk_left) (hξ a) this variable [CountableOrCountablyGenerated α γ] @@ -183,12 +182,12 @@ lemma singularPart_eq_singularPart_measure [IsFiniteKernel κ] [IsFiniteKernel eq_singularPart_measure (rnDeriv_add_singularPart κ η).symm (measurable_rnDeriv κ η) (mutuallySingular_singularPart κ η) a -lemma eq_rnDeriv [IsFiniteKernel κ] [IsFiniteKernel η] (h : κ = Kernel.withDensity η f + ξ) +lemma eq_rnDeriv [IsFiniteKernel κ] [IsFiniteKernel η] (h : κ = η.withDensity f + ξ) (hf : Measurable (Function.uncurry f)) (hξ : ∀ a, ξ a ⟂ₘ η a) (a : α) : f a =ᵐ[η a] rnDeriv κ η a := (eq_rnDeriv_measure h hf hξ a).trans (rnDeriv_eq_rnDeriv_measure _ _ a).symm -lemma eq_singularPart [IsFiniteKernel κ] [IsFiniteKernel η] (h : κ = Kernel.withDensity η f + ξ) +lemma eq_singularPart [IsFiniteKernel κ] [IsFiniteKernel η] (h : κ = η.withDensity f + ξ) (hf : Measurable (Function.uncurry f)) (hξ : ∀ a, ξ a ⟂ₘ η a) (a : α) : ξ a = singularPart κ η a := (eq_singularPart_measure h hf hξ a).trans (singularPart_eq_singularPart_measure a).symm @@ -200,7 +199,7 @@ variable [CountableOrCountablyGenerated α γ] lemma measurable_singularPart (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η] : Measurable (fun a ↦ (κ a).singularPart (η a)) := by refine Measure.measurable_of_measurable_coe _ (fun s hs ↦ ?_) - simp_rw [← Kernel.singularPart_eq_singularPart_measure, Kernel.singularPart_def κ η] + simp_rw [← Kernel.singularPart_eq_singularPart_measure, κ.singularPart_def η] exact Kernel.measurable_coe _ hs lemma rnDeriv_pos [IsFiniteKernel κ] [IsFiniteKernel η] {a : α} (ha : κ a ≪ η a) : @@ -210,7 +209,7 @@ lemma rnDeriv_pos [IsFiniteKernel κ] [IsFiniteKernel η] {a : α} (ha : κ a lemma rnDeriv_ne_top (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η] {a : α} : ∀ᵐ x ∂(η a), rnDeriv κ η a x ≠ ⊤ := by - filter_upwards [rnDeriv_eq_rnDeriv_measure κ η a, Measure.rnDeriv_ne_top (κ a) _] + filter_upwards [rnDeriv_eq_rnDeriv_measure κ η a, (κ a).rnDeriv_ne_top _] with x heq htop using heq ▸ htop lemma rnDeriv_toReal_pos [IsFiniteKernel κ] [IsFiniteKernel η] {a : α} (h : κ a ≪ η a) : @@ -240,7 +239,7 @@ lemma rnDeriv_add (κ ν η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel (a : α) : rnDeriv (κ + ν) η a =ᵐ[η a] rnDeriv κ η a + rnDeriv ν η a := by filter_upwards [rnDeriv_eq_rnDeriv_measure (κ + ν) η a, rnDeriv_eq_rnDeriv_measure κ η a, - rnDeriv_eq_rnDeriv_measure ν η a, Measure.rnDeriv_add (κ a) (ν a) (η a)] with x h1 h2 h3 h4 + rnDeriv_eq_rnDeriv_measure ν η a, (κ a).rnDeriv_add (ν a) (η a)] with x h1 h2 h3 h4 rw [h1, Pi.add_apply, h2, h3, coe_add, Pi.add_apply, h4, Pi.add_apply] lemma rnDeriv_singularPart (κ ν : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel ν] (a : α) : @@ -251,29 +250,29 @@ lemma rnDeriv_singularPart (κ ν : Kernel α γ) [IsFiniteKernel κ] [IsFiniteK lemma withDensity_rnDeriv_eq {κ η : Kernel α γ} [IsFiniteKernel κ] [IsFiniteKernel η] {a : α} (h : κ a ≪ η a) : - Kernel.withDensity η (Kernel.rnDeriv κ η) a = κ a := by + η.withDensity (κ.rnDeriv η) a = κ a := by rw [Kernel.withDensity_apply] - swap; · exact Kernel.measurable_rnDeriv _ _ - have h_ae := Kernel.rnDeriv_eq_rnDeriv_measure κ η a - rw [MeasureTheory.withDensity_congr_ae h_ae, Measure.withDensity_rnDeriv_eq _ _ h] + swap; · exact κ.measurable_rnDeriv _ + have h_ae := κ.rnDeriv_eq_rnDeriv_measure η a + rw [MeasureTheory.withDensity_congr_ae h_ae, (κ a).withDensity_rnDeriv_eq _ h] lemma rnDeriv_withDensity (κ : Kernel α γ) [IsFiniteKernel κ] {f : α → γ → ℝ≥0∞} [IsFiniteKernel (withDensity κ f)] (hf : Measurable (Function.uncurry f)) (a : α) : - Kernel.rnDeriv (Kernel.withDensity κ f) κ a =ᵐ[κ a] f a := by - have h_ae := Kernel.rnDeriv_eq_rnDeriv_measure (Kernel.withDensity κ f) κ a + (κ.withDensity f).rnDeriv κ a =ᵐ[κ a] f a := by + have h_ae := (κ.withDensity f).rnDeriv_eq_rnDeriv_measure κ a have hf' : ∀ a, Measurable (f a) := fun _ ↦ hf.of_uncurry_left - filter_upwards [h_ae, Measure.rnDeriv_withDensity (κ a) (hf' a)] with x hx1 hx2 - rw [hx1, Kernel.withDensity_apply _ hf, hx2] + filter_upwards [h_ae, (κ a).rnDeriv_withDensity (hf' a)] with x hx1 hx2 + rw [hx1, κ.withDensity_apply hf, hx2] lemma withDensity_rnDeriv_le (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η] (a : α) : - Kernel.withDensity η (Kernel.rnDeriv κ η) a ≤ κ a := by + η.withDensity (κ.rnDeriv η) a ≤ κ a := by refine Measure.le_intro (fun s hs _ ↦ ?_) rw [Kernel.withDensity_apply'] - swap; · exact Kernel.measurable_rnDeriv _ _ - rw [setLIntegral_congr_fun hs - ((Kernel.rnDeriv_eq_rnDeriv_measure κ η a).mono (fun x hx _ ↦ hx)), ← withDensity_apply _ hs] - exact Measure.withDensity_rnDeriv_le _ _ _ + swap; · exact κ.measurable_rnDeriv _ + rw [setLIntegral_congr_fun hs ((κ.rnDeriv_eq_rnDeriv_measure η a).mono (fun x hx _ ↦ hx)), + ← withDensity_apply _ hs] + exact (κ a).withDensity_rnDeriv_le _ _ section MeasureCompProd @@ -296,16 +295,15 @@ lemma setLIntegral_prod_rnDeriv _ = (∂μ/∂ν) x * κ x t := by congr rw [Measure.setLIntegral_rnDeriv hx] - rw [lintegral_congr_ae (ae_restrict_of_ae this), - setLIntegral_rnDeriv_mul hμν (Kernel.measurable_coe _ ht).aemeasurable hs, - Measure.compProd_apply_prod hs ht] + rw [lintegral_congr_ae (ae_restrict_of_ae this), Measure.compProd_apply_prod hs ht, + setLIntegral_rnDeriv_mul hμν (κ.measurable_coe ht).aemeasurable hs] lemma rnDeriv_measure_compProd_aux [IsFiniteMeasure μ] [IsFiniteMeasure ν] [IsFiniteKernel κ] [IsFiniteKernel η] (hμν : μ ≪ ν) (hκη : ∀ᵐ a ∂ν, κ a ≪ η a) : ∂(μ ⊗ₘ κ)/∂(ν ⊗ₘ η) =ᵐ[ν ⊗ₘ η] fun p ↦ (∂μ/∂ν) p.1 * rnDeriv κ η p.1 p.2 := by have h_meas : Measurable fun p : α × γ ↦ (∂μ/∂ν) p.1 * rnDeriv κ η p.1 p.2 := - ((Measure.measurable_rnDeriv _ _).comp measurable_fst).mul (measurable_rnDeriv _ _) + ((μ.measurable_rnDeriv _).comp measurable_fst).mul (measurable_rnDeriv _ _) suffices ∀ s, MeasurableSet s → ∫⁻ p in s, (∂(μ ⊗ₘ κ)/∂(ν ⊗ₘ η)) p ∂(ν ⊗ₘ η) = ∫⁻ p in s, (∂μ/∂ν) p.1 * rnDeriv κ η p.1 p.2 ∂(ν ⊗ₘ η) from ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite (Measure.measurable_rnDeriv _ _) h_meas @@ -336,12 +334,12 @@ lemma rnDeriv_measure_compProd_aux - ∫⁻ p in t, (∂μ/∂ν) p.1 * rnDeriv κ η p.1 p.2 ∂ν ⊗ₘ η := by rw [ht_eq] _ = (μ ⊗ₘ κ) univ - ∫⁻ p in t, (∂μ/∂ν) p.1 * rnDeriv κ η p.1 p.2 ∂ν ⊗ₘ η := by - have h := h_left univ MeasurableSet.univ + have h := h_left univ .univ rw [setLIntegral_univ] at h rw [h] _ = ∫⁻ x, ∫⁻ y, (∂μ/∂ν) x * rnDeriv κ η x y ∂η x ∂ν - ∫⁻ p in t, (∂μ/∂ν) p.1 * rnDeriv κ η p.1 p.2 ∂ν ⊗ₘ η := by - have h := this univ univ MeasurableSet.univ MeasurableSet.univ + have h := this univ univ .univ .univ simp only [Measure.restrict_univ, univ_prod_univ] at h rw [← h] _ = ∫⁻ p, (∂μ/∂ν) p.1 * rnDeriv κ η p.1 p.2 ∂ν ⊗ₘ η @@ -373,10 +371,10 @@ lemma todo1 (μ ν : Measure α) (κ η : Kernel α γ) rw [h2] have h_add := Measure.rnDeriv_add (μ' ⊗ₘ κ' + μ.singularPart ν ⊗ₘ κ) (μ' ⊗ₘ (singularPart κ η)) (ν ⊗ₘ η) - have h_add' := Measure.rnDeriv_add (μ' ⊗ₘ κ') (μ.singularPart ν ⊗ₘ κ) (ν ⊗ₘ η) + have h_add' := (μ' ⊗ₘ κ').rnDeriv_add (μ.singularPart ν ⊗ₘ κ) (ν ⊗ₘ η) have h01 : ∂(μ.singularPart ν ⊗ₘ κ)/∂(ν ⊗ₘ η) =ᵐ[ν ⊗ₘ η] 0 := by rw [Measure.rnDeriv_eq_zero] - exact Measure.mutuallySingular_compProd_left (Measure.mutuallySingular_singularPart _ _) κ η + exact Measure.mutuallySingular_compProd_left (μ.mutuallySingular_singularPart _) κ η have h02 : ∂(μ' ⊗ₘ (singularPart κ η))/∂(ν ⊗ₘ η) =ᵐ[ν ⊗ₘ η] 0 := by rw [Measure.rnDeriv_eq_zero] exact Measure.mutuallySingular_compProd_right μ' ν @@ -392,10 +390,10 @@ lemma todo2 (μ ν : Measure α) (κ η : Kernel α γ) let μ' := ν.withDensity (∂μ/∂ν) let κ' := withDensity η (rnDeriv κ η) refine Filter.EventuallyEq.mul ?_ ?_ - · have h := Measure.rnDeriv_withDensity ν (Measure.measurable_rnDeriv μ ν) + · have h := ν.rnDeriv_withDensity (μ.measurable_rnDeriv ν) rw [Filter.EventuallyEq, ae_iff] at h ⊢ - exact ENNReal.ae_eq_compProd_of_ae_eq_fst ν η (Measure.measurable_rnDeriv μ' ν) - (Measure.measurable_rnDeriv μ ν) h + exact ENNReal.ae_eq_compProd_of_ae_eq_fst ν η (μ'.measurable_rnDeriv ν) + (μ.measurable_rnDeriv ν) h · have : ∀ a, rnDeriv κ' η a =ᵐ[η a] rnDeriv κ η a := by intro a rw [← rnDeriv_add_singularPart κ η] @@ -428,7 +426,7 @@ lemma rnDeriv_measure_compProd' (μ ν : Measure α) (κ η : Kernel α γ) lemma rnDeriv_self (κ : Kernel α γ) [IsFiniteKernel κ] (a : α) : rnDeriv κ κ a =ᵐ[κ a] 1 := - (rnDeriv_eq_rnDeriv_measure κ κ a).trans (Measure.rnDeriv_self _) + (rnDeriv_eq_rnDeriv_measure κ κ a).trans (κ a).rnDeriv_self lemma rnDeriv_measure_compProd_left (μ ν : Measure α) (κ : Kernel α γ) [IsFiniteMeasure μ] [IsFiniteMeasure ν] [IsFiniteKernel κ] : @@ -444,8 +442,7 @@ lemma rnDeriv_measure_compProd_right (μ : Measure α) (κ η : Kernel α γ) [IsFiniteMeasure μ] [IsFiniteKernel κ] [IsFiniteKernel η] : ∂(μ ⊗ₘ κ)/∂(μ ⊗ₘ η) =ᵐ[μ ⊗ₘ η] fun p ↦ rnDeriv κ η p.1 p.2 := by have h : (fun p ↦ (∂μ/∂μ) p.1) =ᵐ[μ ⊗ₘ η] (fun p ↦ (1 : α → ℝ≥0∞) p.1) := - ENNReal.ae_eq_compProd_of_ae_eq_fst μ η (Measure.measurable_rnDeriv _ _) - measurable_const (Measure.rnDeriv_self _) + ENNReal.ae_eq_compProd_of_ae_eq_fst μ η (μ.measurable_rnDeriv _) measurable_const μ.rnDeriv_self filter_upwards [rnDeriv_measure_compProd μ μ κ η, h] with p hp1 hp2 rw [hp1, hp2] simp @@ -464,7 +461,7 @@ lemma Measure.absolutelyContinuous_Kernel_of_compProd [SFinite μ] [SFinite ν] [IsFiniteKernel κ] [IsFiniteKernel η] (h : μ ⊗ₘ κ ≪ ν ⊗ₘ η) : ∀ᵐ a ∂μ, κ a ≪ η a := by - suffices ∀ᵐ a ∂μ, Kernel.singularPart κ η a = 0 by + suffices ∀ᵐ a ∂μ, κ.singularPart η a = 0 by filter_upwards [this] with a ha rwa [singularPart_eq_zero_iff_absolutelyContinuous] at ha rw [← rnDeriv_add_singularPart κ η, Measure.compProd_add_right, @@ -474,16 +471,14 @@ lemma Measure.absolutelyContinuous_Kernel_of_compProd have h_zero : μ ⊗ₘ singularPart κ η = 0 := Measure.eq_zero_of_absolutelyContinuous_of_mutuallySingular h.2 this simp_rw [← Measure.measure_univ_eq_zero] - refine (lintegral_eq_zero_iff (Kernel.measurable_coe _ MeasurableSet.univ)).mp ?_ - rw [← setLIntegral_univ, ← Measure.compProd_apply_prod MeasurableSet.univ MeasurableSet.univ, - h_zero] + refine (lintegral_eq_zero_iff (Kernel.measurable_coe _ .univ)).mp ?_ + rw [← setLIntegral_univ, ← Measure.compProd_apply_prod .univ .univ, h_zero] simp lemma Measure.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_of_compProd h, absolutelyContinuous_Kernel_of_compProd h⟩, fun h ↦ Measure.absolutelyContinuous_compProd h.1 h.2⟩ lemma Measure.absolutelyContinuous_compProd_right_iff diff --git a/TestingLowerBounds/ForMathlib/RnDeriv.lean b/TestingLowerBounds/ForMathlib/RnDeriv.lean index ba74ac12..762b9108 100644 --- a/TestingLowerBounds/ForMathlib/RnDeriv.lean +++ b/TestingLowerBounds/ForMathlib/RnDeriv.lean @@ -37,16 +37,15 @@ variable {α β : Type*} {m mα : MeasurableSpace α} {mβ : MeasurableSpace β} lemma rnDeriv_add_self_right (ν μ : Measure α) [SigmaFinite μ] [SigmaFinite ν] : ν.rnDeriv (μ + ν) =ᵐ[ν] fun x ↦ (μ.rnDeriv ν x + 1)⁻¹ := by have hν_ac : ν ≪ μ + ν := by rw [add_comm]; exact rfl.absolutelyContinuous.add_right _ - filter_upwards [Measure.rnDeriv_add' μ ν ν, Measure.rnDeriv_self ν, - Measure.inv_rnDeriv hν_ac] with a h1 h2 h3 + filter_upwards [μ.rnDeriv_add' ν ν, ν.rnDeriv_self, Measure.inv_rnDeriv hν_ac] with a h1 h2 h3 rw [Pi.inv_apply, h1, Pi.add_apply, h2, inv_eq_iff_eq_inv] at h3 rw [h3] lemma rnDeriv_add_self_left (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] : μ.rnDeriv (μ + ν) =ᵐ[ν] fun x ↦ μ.rnDeriv ν x / (μ.rnDeriv ν x + 1) := by have h_add : (μ + ν).rnDeriv (μ + ν) =ᵐ[ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν) := - (ae_add_measure_iff.mp (Measure.rnDeriv_add' μ ν (μ + ν))).2 - have h_one_add := (ae_add_measure_iff.mp (Measure.rnDeriv_self (μ + ν))).2 + (ae_add_measure_iff.mp (μ.rnDeriv_add' ν (μ + ν))).2 + have h_one_add := (ae_add_measure_iff.mp (μ + ν).rnDeriv_self).2 have : (μ.rnDeriv (μ + ν)) =ᵐ[ν] fun x ↦ 1 - (μ.rnDeriv ν x + 1)⁻¹ := by filter_upwards [h_add, h_one_add, rnDeriv_add_self_right ν μ] with a h4 h5 h6 rw [h5, Pi.add_apply] at h4 @@ -54,7 +53,7 @@ lemma rnDeriv_add_self_left (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite rw [h6] simp only [ne_eq, ENNReal.inv_eq_top, add_eq_zero, one_ne_zero, and_false, not_false_eq_true, ENNReal.add_sub_cancel_right] - filter_upwards [this, Measure.rnDeriv_lt_top μ ν] with a ha ha_lt_top + filter_upwards [this, μ.rnDeriv_lt_top ν] with a ha ha_lt_top rw [ha, div_eq_mul_inv] refine ENNReal.sub_eq_of_eq_add (by simp) ?_ nth_rewrite 2 [← one_mul (μ.rnDeriv ν a + 1)⁻¹] @@ -66,7 +65,7 @@ lemma rnDeriv_add_self_left (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite lemma rnDeriv_eq_div (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] : μ.rnDeriv ν =ᵐ[ν] fun x ↦ μ.rnDeriv (μ + ν) x / ν.rnDeriv (μ + ν) x := by - filter_upwards [rnDeriv_add_self_right ν μ, rnDeriv_add_self_left μ ν, Measure.rnDeriv_lt_top μ ν] + filter_upwards [rnDeriv_add_self_right ν μ, rnDeriv_add_self_left μ ν, μ.rnDeriv_lt_top ν] with a ha1 ha2 ha_lt_top rw [ha1, ha2, ENNReal.div_eq_inv_mul, inv_inv, ENNReal.div_eq_inv_mul, ← mul_assoc, ENNReal.mul_inv_cancel, one_mul] @@ -90,9 +89,8 @@ lemma rnDeriv_div_rnDeriv {ξ : Measure α} [SigmaFinite μ] [SigmaFinite ν] [S rw [two_mul] rw [this] exact Measure.absolutelyContinuous_of_le_smul le_rfl - filter_upwards [h_ac h1, h_ac h2, h_ac <| Measure.rnDeriv_lt_top (μ + ν) ξ, - Measure.rnDeriv_lt_top ν (μ + ν), Measure.rnDeriv_pos h_ac] - with a h1 h2 h_lt_top1 h_lt_top2 h_pos + filter_upwards [h_ac h1, h_ac h2, h_ac <| (μ + ν).rnDeriv_lt_top ξ, ν.rnDeriv_lt_top (μ + ν), + Measure.rnDeriv_pos h_ac] with a h1 h2 h_lt_top1 h_lt_top2 h_pos rw [← h1, ← h2, Pi.mul_apply, Pi.mul_apply, div_eq_mul_inv, ENNReal.mul_inv (Or.inr h_lt_top1.ne) (Or.inl h_lt_top2.ne), div_eq_mul_inv, mul_assoc, mul_comm ((μ + ν).rnDeriv ξ a), mul_assoc, ENNReal.inv_mul_cancel h_pos.ne' h_lt_top1.ne, @@ -107,7 +105,7 @@ lemma rnDeriv_eq_div' {ξ : Measure α} [SigmaFinite μ] [SigmaFinite ν] [Sigma lemma rnDeriv_eq_zero_ae_of_zero_measure (ν : Measure α) {s : Set α} (hs : MeasurableSet s) (hμ : μ s = 0) : ∀ᵐ x ∂ν, x ∈ s → (μ.rnDeriv ν) x = 0 := by - rw [← MeasureTheory.setLIntegral_eq_zero_iff hs (Measure.measurable_rnDeriv μ ν)] + rw [← setLIntegral_eq_zero_iff hs (μ.measurable_rnDeriv ν)] exact le_antisymm (hμ ▸ Measure.setLIntegral_rnDeriv_le s) (zero_le _) /--Singular part set of μ with respect to ν.-/ @@ -141,19 +139,17 @@ lemma measure_inter_compl_singularPartSet' (μ ν : Measure α) [SigmaFinite μ] ν.rnDeriv (μ + ν) x * (μ.rnDeriv (μ + ν) x / ν.rnDeriv (μ + ν) x) ∂(μ + ν) = ∫⁻ x in t ∩ sᶜ, μ.rnDeriv (μ + ν) x ∂(μ + ν) := by refine setLIntegral_congr_fun (ht.inter hs.compl) ?_ - filter_upwards [Measure.rnDeriv_lt_top ν (μ + ν)] with x hx_top hx + filter_upwards [ν.rnDeriv_lt_top (μ + ν)] with x hx_top hx rw [div_eq_mul_inv, mul_comm, mul_assoc, ENNReal.inv_mul_cancel, mul_one] · simp only [Set.mem_inter_iff, Set.mem_compl_iff, Set.mem_setOf_eq, s] at hx exact hx.2 · exact hx_top.ne rw [this, Measure.setLIntegral_rnDeriv (rfl.absolutelyContinuous.add_right _)] rw [this, setLIntegral_rnDeriv_mul hν_ac _ (ht.inter hs.compl)] - swap - · exact ((Measure.measurable_rnDeriv _ _).div (Measure.measurable_rnDeriv _ _)).aemeasurable + swap; · exact ((μ.measurable_rnDeriv _).div (ν.measurable_rnDeriv _)).aemeasurable refine setLIntegral_congr_fun (ht.inter hs.compl) ?_ - filter_upwards [Measure.rnDeriv_eq_div μ ν] with x hx - rw [hx] - exact fun _ ↦ rfl + filter_upwards [μ.rnDeriv_eq_div ν] with x hx + exact hx ▸ fun _ ↦ rfl lemma measure_inter_compl_singularPartSet (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] {t : Set α} (ht : MeasurableSet t) : @@ -193,14 +189,14 @@ lemma absolutelyContinuous_restrict_compl_singularPartSet exact withDensity_absolutelyContinuous _ _ example [SigmaFinite μ] [SigmaFinite ν] : - μ (singularPartSet μ ν) = μ.singularPart ν Set.univ := by + μ (singularPartSet μ ν) = μ.singularPart ν .univ := by rw [← restrict_singularPartSet_eq_singularPart] simp only [MeasurableSet.univ, restrict_apply, Set.univ_inter] lemma rnDeriv_eq_zero_ae_of_singularPartSet (μ ν ξ : Measure α) [SigmaFinite μ] [SigmaFinite ν] : - ∀ᵐ x ∂ξ, x ∈ Measure.singularPartSet μ ν → (ν.rnDeriv ξ) x = 0 := - Measure.rnDeriv_eq_zero_ae_of_zero_measure _ Measure.measurableSet_singularPartSet - (Measure.measure_singularPartSet μ ν) + ∀ᵐ x ∂ξ, x ∈ μ.singularPartSet ν → (ν.rnDeriv ξ) x = 0 := + ν.rnDeriv_eq_zero_ae_of_zero_measure ξ Measure.measurableSet_singularPartSet + (μ.measure_singularPartSet ν) section Trim @@ -237,20 +233,19 @@ lemma rnDeriv_toReal_pos [SigmaFinite μ] [SigmaFinite ν] (hμν : μ ≪ ν) : lemma ae_rnDeriv_ne_zero_imp_of_ae_aux [SigmaFinite μ] [SigmaFinite ν] {p : α → Prop} (h : ∀ᵐ a ∂μ, p a) (hμν : μ ≪ ν) : ∀ᵐ a ∂ν, μ.rnDeriv ν a ≠ 0 → p a := by - rw [Measure.haveLebesgueDecomposition_add ν μ, ae_add_measure_iff] + rw [ν.haveLebesgueDecomposition_add μ, ae_add_measure_iff] constructor - · rw [← Measure.haveLebesgueDecomposition_add ν μ] + · rw [← ν.haveLebesgueDecomposition_add μ] have : ∀ᵐ x ∂(ν.singularPart μ), μ.rnDeriv ν x = 0 := by - refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite (Measure.measurable_rnDeriv _ _) + refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite (μ.measurable_rnDeriv _) measurable_const (fun s hs _ ↦ ?_) - simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter, - zero_mul] + simp only [lintegral_const, Measure.restrict_apply .univ, Set.univ_inter, zero_mul] rw [← Measure.restrict_singularPartSet_eq_singularPart, Measure.restrict_restrict hs, Measure.setLIntegral_rnDeriv hμν] - exact measure_mono_null Set.inter_subset_right (Measure.measure_singularPartSet _ _) + exact measure_mono_null Set.inter_subset_right (ν.measure_singularPartSet _) filter_upwards [this] with x hx h_absurd using absurd hx h_absurd · have h_ac : μ.withDensity (ν.rnDeriv μ) ≪ μ := withDensity_absolutelyContinuous _ _ - rw [← Measure.haveLebesgueDecomposition_add ν μ] + rw [← ν.haveLebesgueDecomposition_add μ] suffices ∀ᵐx ∂μ, μ.rnDeriv ν x ≠ 0 → p x from h_ac this filter_upwards [h] with _ h _ using h @@ -258,7 +253,7 @@ lemma ae_rnDeriv_ne_zero_imp_of_ae [SigmaFinite μ] [SigmaFinite ν] {p : α → (h : ∀ᵐ a ∂μ, p a) : ∀ᵐ a ∂ν, μ.rnDeriv ν a ≠ 0 → p a := by suffices ∀ᵐ a ∂ν, (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν a ≠ 0 → p a by - have h := Measure.rnDeriv_withDensity ν (Measure.measurable_rnDeriv μ ν) + have h := ν.rnDeriv_withDensity (μ.measurable_rnDeriv ν) filter_upwards [this, h] with x hx1 hx2 rwa [hx2] at hx1 refine ae_rnDeriv_ne_zero_imp_of_ae_aux ?_ (withDensity_absolutelyContinuous _ _) @@ -267,7 +262,7 @@ lemma ae_rnDeriv_ne_zero_imp_of_ae [SigmaFinite μ] [SigmaFinite ν] {p : α → lemma ae_integrable_mul_rnDeriv_of_ae_integrable {κ : α → Measure β} [SigmaFinite μ] [SigmaFinite ν] (g : α → β → ℝ) (h : ∀ᵐ a ∂μ, Integrable (fun x ↦ g a x) (κ a)) : ∀ᵐ a ∂ν, Integrable (fun x ↦ (μ.rnDeriv ν a).toReal * g a x) (κ a) := by - apply @Measure.ae_rnDeriv_ne_zero_imp_of_ae _ _ _ ν at h + apply μ.ae_rnDeriv_ne_zero_imp_of_ae (ν := ν) at h filter_upwards [h] with a ha by_cases h_zero : μ.rnDeriv ν a = 0 · rw [h_zero] @@ -288,9 +283,9 @@ lemma ae_integrable_of_ae_integrable_mul_rnDeriv {κ : α → Measure β} [Sigma lemma _root_.MeasureTheory.Measure.integral_toReal_rnDeriv' {α : Type*} {m : MeasurableSpace α} {μ : Measure α} {ν : Measure α} [IsFiniteMeasure μ] [SigmaFinite ν] : ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν - = (μ Set.univ).toReal - ((μ.singularPart ν) Set.univ).toReal := by - rw [← ENNReal.toReal_sub_of_le (μ.singularPart_le ν Set.univ) (measure_ne_top _ _), - ← Measure.sub_apply .univ (Measure.singularPart_le μ ν), Measure.measure_sub_singularPart, + = (μ .univ).toReal - ((μ.singularPart ν) .univ).toReal := by + rw [← ENNReal.toReal_sub_of_le (μ.singularPart_le ν .univ) (measure_ne_top _ _), + ← Measure.sub_apply .univ (μ.singularPart_le ν), Measure.measure_sub_singularPart, ← Measure.setIntegral_toReal_rnDeriv_eq_withDensity, integral_univ] end MeasureTheory.Measure diff --git a/TestingLowerBounds/Kernel/Basic.lean b/TestingLowerBounds/Kernel/Basic.lean index 6c17873c..113c0577 100644 --- a/TestingLowerBounds/Kernel/Basic.lean +++ b/TestingLowerBounds/Kernel/Basic.lean @@ -35,10 +35,10 @@ lemma map_comp (κ : Kernel α β) (η : Kernel β γ) {f : γ → δ} (hf : Mea · exact hf hs lemma fst_comp (κ : Kernel α β) (η : Kernel β (γ × δ)) : (η ∘ₖ κ).fst = η.fst ∘ₖ κ := - Kernel.map_comp κ η measurable_fst + κ.map_comp η measurable_fst lemma snd_comp (κ : Kernel α β) (η : Kernel β (γ × δ)) : (η ∘ₖ κ).snd = η.snd ∘ₖ κ := - Kernel.map_comp κ η measurable_snd + κ.map_comp η measurable_snd lemma deterministic_prod_deterministic {f : α → β} {g : α → γ} (hf : Measurable f) (hg : Measurable g) : diff --git a/TestingLowerBounds/Kernel/BayesInv.lean b/TestingLowerBounds/Kernel/BayesInv.lean index 07cec032..b8c5173f 100644 --- a/TestingLowerBounds/Kernel/BayesInv.lean +++ b/TestingLowerBounds/Kernel/BayesInv.lean @@ -51,7 +51,7 @@ instance : IsMarkovKernel (κ†μ) := by rw [bayesInv]; infer_instance /-- The main property of the Bayesian inverse. -/ lemma compProd_bayesInv (κ : Kernel α β) (μ : Measure α) [IsFiniteMeasure μ] [IsFiniteKernel κ] : (κ ∘ₘ μ) ⊗ₘ (κ†μ) = (μ ⊗ₘ κ).map Prod.swap := by - have h := Measure.disintegrate ((μ ⊗ₘ κ).map Prod.swap) ((μ ⊗ₘ κ).map Prod.swap).condKernel + have h := ((μ ⊗ₘ κ).map Prod.swap).disintegrate ((μ ⊗ₘ κ).map Prod.swap).condKernel rwa [Measure.fst_swap_compProd] at h lemma compProd_bayesInv' (κ : Kernel α β) (μ : Measure α) [IsFiniteMeasure μ] [IsFiniteKernel κ] : diff --git a/TestingLowerBounds/Kernel/Monoidal.lean b/TestingLowerBounds/Kernel/Monoidal.lean index 020cbacf..b541e9f0 100644 --- a/TestingLowerBounds/Kernel/Monoidal.lean +++ b/TestingLowerBounds/Kernel/Monoidal.lean @@ -84,7 +84,7 @@ lemma comp_discard (κ : Kernel α β) [IsMarkovKernel κ] : discard β ∘ₖ @[simp] lemma _root_.MeasureTheory.Measure.comp_discard (μ : Measure α) : - μ.bind (discard α) = μ Set.univ • (Measure.dirac ()) := by + μ.bind (discard α) = μ .univ • (Measure.dirac ()) := by ext s hs; simp [Measure.bind_apply hs (Kernel.measurable _), mul_comm] end Discard @@ -172,13 +172,13 @@ lemma measurable_Kernel_prod_mk_left'' {κ : Kernel α β} [IsSFiniteKernel κ] {t : Set (γ × β)} (ht : MeasurableSet t) : Measurable (Function.uncurry fun a y ↦ (κ a) (Prod.mk y ⁻¹' t)) := by have h1 (p : α × γ) : (Prod.mk p.2 ⁻¹' t) - = (Prod.mk p ⁻¹' (MeasurableEquiv.prodAssoc ⁻¹' (Set.univ ×ˢ t))) := by + = (Prod.mk p ⁻¹' (MeasurableEquiv.prodAssoc ⁻¹' (.univ ×ˢ t))) := by ext x; simp [MeasurableEquiv.prodAssoc] have h2 (p : α × γ) : κ p.1 = (κ ∘ₖ (deterministic (fun (p : α × γ) ↦ p.1) measurable_fst (mα := inferInstance))) p := by ext s hs - rw [comp_apply, deterministic_apply, Measure.bind_apply hs (Kernel.measurable _), - lintegral_dirac' _ (Kernel.measurable_coe κ hs)] + rw [comp_apply, deterministic_apply, Measure.bind_apply hs κ.measurable, + lintegral_dirac' _ (κ.measurable_coe hs)] simp_rw [Function.uncurry_def, h1, h2] exact Kernel.measurable_kernel_prod_mk_left <| (MeasurableEquiv.measurableSet_preimage _).mpr (MeasurableSet.univ.prod ht) @@ -194,9 +194,8 @@ lemma parallelComp_comp_parallelComp {α' β' γ' : Type*} {mα' : MeasurableSpa lintegral_prod_of_measurable _ (Kernel.measurable_coe _ hs)] simp_rw [parallelComp_apply, comp_apply] have : SFinite ((κ' a.2).bind ⇑η') := by sorry --this instance is in MeasureCompProd, which imports this file, we may have to move some lemmas around or create a new file - rw [Measure.lintegral_bind (Kernel.measurable η) (measurable_measure_prod_mk_left hs)] - simp_rw [Measure.bind_apply (measurable_prod_mk_left hs) (Kernel.measurable η'), - Measure.prod_apply hs, + rw [Measure.lintegral_bind η.measurable (measurable_measure_prod_mk_left hs)] + simp_rw [Measure.bind_apply (measurable_prod_mk_left hs) η'.measurable, Measure.prod_apply hs, lintegral_lintegral_swap (measurable_Kernel_prod_mk_left'' hs).aemeasurable] lemma parallelComp_comp_prod {β' γ' : Type*} diff --git a/TestingLowerBounds/MeasureCompProd.lean b/TestingLowerBounds/MeasureCompProd.lean index af91676e..934f19aa 100644 --- a/TestingLowerBounds/MeasureCompProd.lean +++ b/TestingLowerBounds/MeasureCompProd.lean @@ -40,7 +40,7 @@ variable {α β γ : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β Defined using `MeasureTheory.Measure.bind` -/ --scoped[ProbabilityTheory] infixl:100 " ∘ₘ " => fun μ κ ↦ MeasureTheory.Measure.bind κ μ -scoped[ProbabilityTheory] notation3 κ " ∘ₘ " μ:100 => MeasureTheory.Measure.bind μ κ +scoped[ProbabilityTheory] notation3 κ " ∘ₘ " μ:100 => Measure.bind μ κ lemma Measure.map_comp (μ : Measure α) (κ : Kernel α β) {f : β → γ} (hf : Measurable f) : (κ ∘ₘ μ).map f = (κ.map f hf) ∘ₘ μ := by @@ -51,7 +51,7 @@ lemma Measure.map_comp (μ : Measure α) (κ : Kernel α β) {f : β → γ} (hf lemma Measure.comp_assoc {μ : Measure α} {κ : Kernel α β} {η : Kernel β γ} : η ∘ₘ (κ ∘ₘ μ) = (η ∘ₖ κ) ∘ₘ μ := - Measure.bind_bind (Kernel.measurable _) (Kernel.measurable _) + Measure.bind_bind κ.measurable η.measurable lemma Measure.comp_deterministic_eq_map {f : α → β} (hf : Measurable f) : Kernel.deterministic f hf ∘ₘ μ = μ.map f := by @@ -67,8 +67,7 @@ lemma Measure.comp_eq_snd_compProd (μ : Measure α) [SFinite μ] (κ : Kernel α β) [IsSFiniteKernel κ] : κ ∘ₘ μ = (μ ⊗ₘ κ).snd := by ext s hs - rw [Measure.bind_apply hs (Kernel.measurable _), Measure.snd_apply hs, - Measure.compProd_apply] + rw [Measure.bind_apply hs κ.measurable, Measure.snd_apply hs, Measure.compProd_apply] · rfl · exact measurable_snd hs @@ -100,8 +99,7 @@ lemma Measure.compProd_const {ν : Measure β} [SFinite μ] [SFinite ν] : simp_rw [Kernel.const_apply] @[simp] -lemma Measure.comp_const {ν : Measure β} : - (Kernel.const α ν) ∘ₘ μ = μ Set.univ • ν := by +lemma Measure.comp_const {ν : Measure β} : (Kernel.const α ν) ∘ₘ μ = μ .univ • ν := by ext s hs simp_rw [Measure.bind_apply hs (Kernel.measurable _), Kernel.const_apply, lintegral_const] simp [mul_comm] @@ -123,8 +121,8 @@ lemma Measure.compProd_apply_toReal [SFinite μ] [IsFiniteKernel κ] rw [ENNReal.ofReal_toReal (measure_ne_top _ _)] lemma Measure.compProd_univ_toReal [SFinite μ] [IsFiniteKernel κ] : - ((μ ⊗ₘ κ) Set.univ).toReal = ∫ x, (κ x Set.univ).toReal ∂μ := - compProd_apply_toReal MeasurableSet.univ + ((μ ⊗ₘ κ) .univ).toReal = ∫ x, (κ x .univ).toReal ∂μ := + compProd_apply_toReal .univ lemma Measure.fst_sum {ι : Type*} (μ : ι → Measure (α × β)) : (Measure.sum μ).fst = Measure.sum (fun n ↦ (μ n).fst) := by @@ -255,38 +253,35 @@ lemma singularPart_compProd'' [MeasurableSpace.CountableOrCountablyGenerated α (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] : (μ ⊗ₘ κ).singularPart (ν ⊗ₘ η) - = μ.singularPart ν ⊗ₘ Kernel.withDensity η (Kernel.rnDeriv κ η) - + μ.singularPart ν ⊗ₘ Kernel.singularPart κ η - + ν.withDensity (∂μ/∂ν) ⊗ₘ Kernel.singularPart κ η := by - conv_lhs => rw [← Kernel.rnDeriv_add_singularPart κ η, Measure.compProd_add_right, + = μ.singularPart ν ⊗ₘ η.withDensity (κ.rnDeriv η) + μ.singularPart ν ⊗ₘ κ.singularPart η + + ν.withDensity (∂μ/∂ν) ⊗ₘ κ.singularPart η := by + conv_lhs => rw [← κ.rnDeriv_add_singularPart η, Measure.compProd_add_right, μ.haveLebesgueDecomposition_add ν] simp_rw [Measure.compProd_add_left, Measure.singularPart_add] - have : (ν.withDensity (∂μ/∂ν) ⊗ₘ Kernel.withDensity η (Kernel.rnDeriv κ η)).singularPart - (ν ⊗ₘ η) = 0 := by + have : (ν.withDensity (∂μ/∂ν) ⊗ₘ η.withDensity (κ.rnDeriv η)).singularPart (ν ⊗ₘ η) = 0 := by refine Measure.singularPart_eq_zero_of_ac (Measure.absolutelyContinuous_compProd ?_ ?_) · exact withDensity_absolutelyContinuous _ _ · exact ae_of_all _ (Kernel.withDensity_absolutelyContinuous _) rw [this, add_zero, ← add_assoc] congr · rw [Measure.singularPart_eq_self] - exact Kernel.Measure.mutuallySingular_compProd_left (Measure.mutuallySingular_singularPart μ ν) - (Kernel.withDensity η (Kernel.rnDeriv κ η)) η + exact Kernel.Measure.mutuallySingular_compProd_left (μ.mutuallySingular_singularPart ν) + (η.withDensity (κ.rnDeriv η)) η · rw [Measure.singularPart_eq_self] - exact Kernel.Measure.mutuallySingular_compProd_left (Measure.mutuallySingular_singularPart μ ν) - (Kernel.singularPart κ η) η + exact Kernel.Measure.mutuallySingular_compProd_left (μ.mutuallySingular_singularPart ν) + (κ.singularPart η) η · rw [Measure.singularPart_eq_self] exact Kernel.Measure.mutuallySingular_compProd_right (ν.withDensity (∂μ/∂ν)) ν - (.of_forall <| Kernel.mutuallySingular_singularPart _ _) + (.of_forall <| κ.mutuallySingular_singularPart _) lemma singularPart_compProd [MeasurableSpace.CountableOrCountablyGenerated α β] (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] : (μ ⊗ₘ κ).singularPart (ν ⊗ₘ η) - = μ.singularPart ν ⊗ₘ Kernel.withDensity η (Kernel.rnDeriv κ η) - + μ ⊗ₘ Kernel.singularPart κ η := by + = μ.singularPart ν ⊗ₘ η.withDensity (κ.rnDeriv η) + μ ⊗ₘ κ.singularPart η := by rw [singularPart_compProd''] - have : (μ ⊗ₘ Kernel.singularPart κ η) = (μ.singularPart ν ⊗ₘ Kernel.singularPart κ η) - + (ν.withDensity (∂μ/∂ν) ⊗ₘ Kernel.singularPart κ η) := by + have : (μ ⊗ₘ κ.singularPart η) = (μ.singularPart ν ⊗ₘ κ.singularPart η) + + (ν.withDensity (∂μ/∂ν) ⊗ₘ κ.singularPart η) := by rw [← Measure.compProd_add_left, ← μ.haveLebesgueDecomposition_add ν] rw [this] abel @@ -295,29 +290,24 @@ lemma singularPart_compProd' [MeasurableSpace.CountableOrCountablyGenerated α (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] : (μ ⊗ₘ κ).singularPart (ν ⊗ₘ η) - = μ.singularPart ν ⊗ₘ κ + ν.withDensity (∂μ/∂ν) ⊗ₘ Kernel.singularPart κ η := by + = μ.singularPart ν ⊗ₘ κ + ν.withDensity (∂μ/∂ν) ⊗ₘ κ.singularPart η := by rw [singularPart_compProd''] have : μ.singularPart ν ⊗ₘ κ - = μ.singularPart ν ⊗ₘ Kernel.withDensity η (Kernel.rnDeriv κ η) - + μ.singularPart ν ⊗ₘ Kernel.singularPart κ η := by - rw [← Measure.compProd_add_right] - congr - exact (Kernel.rnDeriv_add_singularPart κ η).symm + = μ.singularPart ν ⊗ₘ η.withDensity (κ.rnDeriv η) + μ.singularPart ν ⊗ₘ κ.singularPart η := by + rw [← Measure.compProd_add_right, (κ.rnDeriv_add_singularPart η)] rw [this] lemma singularPart_compProd_left [MeasurableSpace.CountableOrCountablyGenerated α β] (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (κ : Kernel α β) [IsFiniteKernel κ] : (μ ⊗ₘ κ).singularPart (ν ⊗ₘ κ) = μ.singularPart ν ⊗ₘ κ := by - rw [singularPart_compProd', Kernel.singularPart_self] - simp [Measure.singularPart_zero] + rw [singularPart_compProd', κ.singularPart_self, Measure.compProd_zero_right, add_zero] lemma singularPart_compProd_right [MeasurableSpace.CountableOrCountablyGenerated α β] (μ : Measure α) [IsFiniteMeasure μ] (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] : - (μ ⊗ₘ κ).singularPart (μ ⊗ₘ η) = μ ⊗ₘ Kernel.singularPart κ η := by - rw [singularPart_compProd, Measure.singularPart_self] - simp [Measure.singularPart_zero] + (μ ⊗ₘ κ).singularPart (μ ⊗ₘ η) = μ ⊗ₘ κ.singularPart η := by + rw [singularPart_compProd, Measure.singularPart_self, Measure.compProd_zero_left, zero_add] end SingularPart @@ -365,14 +355,14 @@ lemma integral_f_compProd_right_congr (μ : Measure α) [IsFiniteMeasure μ] (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] : (fun a ↦ ∫ b, f ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) (a, b)).toReal ∂(η a)) =ᵐ[μ] fun a ↦ ∫ b, f ((∂κ a/∂η a) b).toReal ∂(η a) := by - filter_upwards [integral_f_compProd_congr μ μ κ η, Measure.rnDeriv_self μ] with a ha h_eq_one + filter_upwards [integral_f_compProd_congr μ μ κ η, μ.rnDeriv_self] with a ha h_eq_one rw [ha] simp_rw [h_eq_one, one_mul] lemma integral_f_compProd_left_congr (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (κ : Kernel α β) [IsFiniteKernel κ] : (fun a ↦ ∫ b, f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ κ) (a, b)).toReal ∂(κ a)) - =ᵐ[ν] fun a ↦ (κ a Set.univ).toReal * f ((∂μ/∂ν) a).toReal := by + =ᵐ[ν] fun a ↦ (κ a .univ).toReal * f ((∂μ/∂ν) a).toReal := by filter_upwards [integral_f_compProd_congr (f := f) μ ν κ κ] with a ha have h_one := (κ a).rnDeriv_self rw [ha, ← smul_eq_mul, ← integral_const] @@ -460,17 +450,16 @@ lemma compProd_apply_toReal [SFinite μ] [IsFiniteKernel κ] rw [ENNReal.ofReal_toReal (measure_ne_top _ _)] lemma compProd_univ_toReal [SFinite μ] [IsFiniteKernel κ] : - ((μ ⊗ₘ κ) Set.univ).toReal = ∫ x, (κ x Set.univ).toReal ∂μ := - compProd_apply_toReal MeasurableSet.univ + ((μ ⊗ₘ κ) .univ).toReal = ∫ x, (κ x .univ).toReal ∂μ := + compProd_apply_toReal .univ lemma Measure.compProd_apply_univ [SFinite μ] [IsMarkovKernel κ] : - (μ ⊗ₘ κ) Set.univ = μ (Set.univ) := by - rw [Measure.compProd_apply MeasurableSet.univ] + (μ ⊗ₘ κ) .univ = μ .univ := by + rw [Measure.compProd_apply .univ] simp -lemma Measure.comp_apply_univ [IsMarkovKernel κ] : - (κ ∘ₘ μ) Set.univ = μ (Set.univ) := by - rw [Measure.bind_apply MeasurableSet.univ (Kernel.measurable κ)] +lemma Measure.comp_apply_univ [IsMarkovKernel κ] : (κ ∘ₘ μ) .univ = μ .univ := by + rw [Measure.bind_apply .univ κ.measurable] simp instance [SFinite μ] [IsSFiniteKernel κ] : SFinite (κ ∘ₘ μ) := by @@ -492,7 +481,7 @@ lemma Measure.compProd_smul_left (a : ℝ≥0∞) [SFinite μ] [IsSFiniteKernel lemma Measure.comp_smul_left (a : ℝ≥0∞) : κ ∘ₘ (a • μ) = a • (κ ∘ₘ μ) := by ext s hs - simp only [Measure.bind_apply hs (Kernel.measurable _), lintegral_smul_measure, - Measure.smul_apply, smul_eq_mul] + simp only [Measure.bind_apply hs κ.measurable, lintegral_smul_measure, Measure.smul_apply, + smul_eq_mul] end ProbabilityTheory diff --git a/TestingLowerBounds/Testing/Binary.lean b/TestingLowerBounds/Testing/Binary.lean index e065e468..f2dbe713 100644 --- a/TestingLowerBounds/Testing/Binary.lean +++ b/TestingLowerBounds/Testing/Binary.lean @@ -49,7 +49,7 @@ def twoHypKernel (μ ν : Measure 𝒳) : Kernel Bool 𝒳 where @[simp] lemma twoHypKernel_apply (b : Bool) : twoHypKernel μ ν b = bif b then ν else μ := rfl instance [IsFiniteMeasure μ] [IsFiniteMeasure ν] : IsFiniteKernel (twoHypKernel μ ν) := - ⟨max (μ Set.univ) (ν Set.univ), max_lt (measure_lt_top _ _) (measure_lt_top _ _), + ⟨max (μ .univ) (ν .univ), max_lt (measure_lt_top _ _) (measure_lt_top _ _), fun b ↦ by cases b <;> simp⟩ instance [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] : @@ -99,14 +99,14 @@ lemma sum_smul_rnDeriv_twoHypKernel (μ ν : Measure 𝒳) [IsFiniteMeasure μ] (π : Measure Bool) [IsFiniteMeasure π] : (π {true} • ν.rnDeriv (twoHypKernel μ ν ∘ₘ π) + π {false} • (μ.rnDeriv (twoHypKernel μ ν ∘ₘ π))) =ᵐ[twoHypKernel μ ν ∘ₘ π] 1 := by - have h1 := Measure.rnDeriv_smul_left_of_ne_top ν (twoHypKernel μ ν ∘ₘ π) + have h1 := ν.rnDeriv_smul_left_of_ne_top (twoHypKernel μ ν ∘ₘ π) (measure_ne_top π {true}) - have h2 := Measure.rnDeriv_smul_left_of_ne_top μ (twoHypKernel μ ν ∘ₘ π) + have h2 := μ.rnDeriv_smul_left_of_ne_top (twoHypKernel μ ν ∘ₘ π) (measure_ne_top π {false}) have : IsFiniteMeasure (π {true} • ν) := ν.smul_finite (measure_ne_top _ _) have : IsFiniteMeasure (π {false} • μ) := μ.smul_finite (measure_ne_top _ _) - have h3 := Measure.rnDeriv_add (π {true} • ν) (π {false} • μ) (twoHypKernel μ ν ∘ₘ π) - have h4 := Measure.rnDeriv_self (twoHypKernel μ ν ∘ₘ π) + have h3 := (π {true} • ν).rnDeriv_add (π {false} • μ) (twoHypKernel μ ν ∘ₘ π) + have h4 := (twoHypKernel μ ν ∘ₘ π).rnDeriv_self filter_upwards [h1, h2, h3, h4] with a h1 h2 h3 h4 simp only [Pi.add_apply, Pi.smul_apply, smul_eq_mul, Pi.one_apply] at h1 h2 h3 h4 ⊢ rw [← h1, ← h2, ← h3, ← measure_comp_twoHypKernel, h4] @@ -133,13 +133,12 @@ def twoHypKernelInv (μ ν : Measure 𝒳) (π : Measure Bool) : Kernel 𝒳 Boo measurable' := by refine Measurable.ite ?_ ?_ measurable_const · refine measurableSet_preimage ?_ (measurableSet_singleton _) - exact ((Measure.measurable_rnDeriv _ _).const_mul _).add - ((Measure.measurable_rnDeriv _ _).const_mul _) + exact ((ν.measurable_rnDeriv _).const_mul _).add ((μ.measurable_rnDeriv _).const_mul _) refine Measure.measurable_of_measurable_coe _ (fun s _ ↦ ?_) simp only [Measure.coe_add, Measure.coe_smul, Pi.add_apply, Pi.smul_apply, MeasurableSpace.measurableSet_top, Measure.dirac_apply', smul_eq_mul] - exact ((measurable_const.mul (Measure.measurable_rnDeriv _ _)).mul measurable_const).add - ((measurable_const.mul (Measure.measurable_rnDeriv _ _)).mul measurable_const) + exact ((measurable_const.mul (ν.measurable_rnDeriv _)).mul measurable_const).add + ((measurable_const.mul (μ.measurable_rnDeriv _)).mul measurable_const) lemma twoHypKernelInv_apply (μ ν : Measure 𝒳) (π : Measure Bool) (x : 𝒳) : twoHypKernelInv μ ν π x @@ -211,7 +210,7 @@ lemma measure_prod_ext {μ ν : Measure (𝒳 × 𝒴)} [IsFiniteMeasure μ] · exact fun t ⟨A, hA, B, hB, ht⟩ ↦ ht ▸ h A hA B hB · intro t ht h_eq rw [measure_compl ht (measure_ne_top μ t), measure_compl ht (h_eq ▸ measure_ne_top μ t), h_eq, - ← Set.univ_prod_univ, ← h Set.univ MeasurableSet.univ Set.univ MeasurableSet.univ] + ← Set.univ_prod_univ, ← h _ .univ _ .univ] · intro A h_disj h_meas h_eq simp_rw [measure_iUnion h_disj h_meas, h_eq] @@ -403,7 +402,7 @@ lemma nonempty_subtype_isMarkovKernel_of_nonempty {𝒳 : Type*} {m𝒳 : Measur @[simp] lemma bayesBinaryRisk_self (μ : Measure 𝒳) (π : Measure Bool) : - bayesBinaryRisk μ μ π = min (π {false}) (π {true}) * μ Set.univ := by + bayesBinaryRisk μ μ π = min (π {false}) (π {true}) * μ .univ := by rw [bayesBinaryRisk_eq] refine le_antisymm ?_ ?_ · let η : Kernel 𝒳 Bool := @@ -418,7 +417,7 @@ lemma bayesBinaryRisk_self (μ : Measure 𝒳) (π : Measure Bool) : _ ≥ ⨅ κ, ⨅ (_ : IsMarkovKernel κ), min (π {false}) (π {true}) * (κ ∘ₘ μ) {false} + min (π {false}) (π {true}) * (κ ∘ₘ μ) {true} := by gcongr <;> simp - _ = ⨅ κ, ⨅ (_ : IsMarkovKernel κ), min (π {false}) (π {true}) * μ Set.univ := by + _ = ⨅ κ, ⨅ (_ : IsMarkovKernel κ), min (π {false}) (π {true}) * μ .univ := by simp_rw [← mul_add, ← measure_union (show Disjoint {false} {true} from by simp) (by trivial), (set_fintype_card_eq_univ_iff ({false} ∪ {true})).mp rfl, Measure.comp_apply_univ] @@ -435,7 +434,7 @@ lemma bayesBinaryRisk_dirac (a b : ℝ≥0∞) (x : 𝒳) (π : Measure Bool) : simp [lintegral_dirac] lemma bayesBinaryRisk_le_min (μ ν : Measure 𝒳) (π : Measure Bool) : - bayesBinaryRisk μ ν π ≤ min (π {false} * μ Set.univ) (π {true} * ν Set.univ) := by + bayesBinaryRisk μ ν π ≤ min (π {false} * μ .univ) (π {true} * ν .univ) := by convert bayesBinaryRisk_le_bayesBinaryRisk_comp μ ν π (Kernel.discard 𝒳) simp_rw [Measure.comp_discard, bayesBinaryRisk_dirac] @@ -469,10 +468,10 @@ lemma bayesBinaryRisk_of_measure_false_eq_zero (μ ν : Measure 𝒳) (hπ : π lemma bayesBinaryRisk_symm (μ ν : Measure 𝒳) (π : Measure Bool) : bayesBinaryRisk μ ν π = bayesBinaryRisk ν μ (π.map Bool.not) := by have : (Bool.not ⁻¹' {true}) = {false} := by ext x; simp - have h1 : (Measure.map Bool.not π) {true} = π {false} := by + have h1 : (π.map Bool.not) {true} = π {false} := by rw [Measure.map_apply (by exact fun _ a ↦ a) (by trivial), this] have : (Bool.not ⁻¹' {false}) = {true} := by ext x; simp - have h2 : (Measure.map Bool.not π) {false} = π {true} := by + have h2 : (π.map Bool.not) {false} = π {true} := by rw [Measure.map_apply (by exact fun _ a ↦ a) (by trivial), this] simp_rw [bayesBinaryRisk_eq, h1, h2, add_comm, iInf_subtype'] -- from this point on the proof is basically a change of variable inside the iInf, @@ -480,7 +479,7 @@ lemma bayesBinaryRisk_symm (μ ν : Measure 𝒳) (π : Measure Bool) : -- the `Bool.not` operation, maybe it can be shortened or something can be separated as -- a different lemma, but I'm not sure how useful this would be let e : (Kernel 𝒳 Bool) ≃ (Kernel 𝒳 Bool) := by - have h_id : Kernel.comap (Kernel.deterministic Bool.not (fun _ a ↦ a)) Bool.not (fun _ a ↦ a) + have h_id : (Kernel.deterministic Bool.not (fun _ a ↦ a)).comap Bool.not (fun _ a ↦ a) = Kernel.id := by ext x : 1 simp_rw [Kernel.comap_apply, Kernel.deterministic_apply, Kernel.id_apply, Bool.not_not] @@ -561,7 +560,7 @@ lemma toReal_bayesBinaryRisk_eq_integral_min (μ ν : Measure 𝒳) [IsFiniteMea <;> exact Measure.measurable_rnDeriv _ _ |>.const_mul _ |>.ennreal_toNNReal |>.coe_nnreal_real congr 1 apply lintegral_congr_ae - filter_upwards [Measure.rnDeriv_ne_top μ _, Measure.rnDeriv_ne_top ν _] with x hxμ hxν + filter_upwards [μ.rnDeriv_ne_top _, ν.rnDeriv_ne_top _] with x hxμ hxν have : (π {false} * μ.rnDeriv (twoHypKernel μ ν ∘ₘ π) x) ≠ ⊤ := (ENNReal.mul_ne_top (measure_ne_top _ _) hxμ) have : (π {true} * ν.rnDeriv (twoHypKernel μ ν ∘ₘ π) x) ≠ ⊤ := @@ -576,7 +575,7 @@ lemma toReal_bayesBinaryRisk_eq_integral_min (μ ν : Measure 𝒳) [IsFiniteMea lemma toReal_bayesBinaryRisk_eq_integral_abs (μ ν : Measure 𝒳) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (π : Measure Bool) [IsFiniteMeasure π] : (bayesBinaryRisk μ ν π).toReal - = 2⁻¹ * (((twoHypKernel μ ν ∘ₘ π) Set.univ).toReal + = 2⁻¹ * (((twoHypKernel μ ν ∘ₘ π) .univ).toReal - ∫ x, |(π {false} * μ.rnDeriv (twoHypKernel μ ν ∘ₘ π) x).toReal - (π {true} * ν.rnDeriv (twoHypKernel μ ν ∘ₘ π) x).toReal| ∂(twoHypKernel μ ν ∘ₘ π)) := by simp_rw [toReal_bayesBinaryRisk_eq_integral_min, min_eq_add_sub_abs_sub, integral_mul_left] @@ -596,13 +595,13 @@ lemma toReal_bayesBinaryRisk_eq_integral_abs (μ ν : Measure 𝒳) [IsFiniteMea simp only [ENNReal.toReal_mul, MeasurableSet.univ, sub_left_inj, integral_mul_left] nth_rw 5 [measure_comp_twoHypKernel] calc - _ = (π {false}).toReal * (μ Set.univ).toReal + (π {true}).toReal + _ = (π {false}).toReal * (μ .univ).toReal + (π {true}).toReal * ∫ (a : 𝒳), ((∂ν/∂twoHypKernel μ ν ∘ₘ π) a).toReal ∂(twoHypKernel μ ν ∘ₘ π) := by by_cases hπ_false : π {false} = 0 · simp [hπ_false, bayesBinaryRisk_of_measure_false_eq_zero] rw [Measure.integral_toReal_rnDeriv (absolutelyContinuous_measure_comp_twoHypKernel_left μ ν hπ_false)] - _ = (π {false}).toReal * (μ Set.univ).toReal + (π {true}).toReal * (ν Set.univ).toReal := by + _ = (π {false}).toReal * (μ .univ).toReal + (π {true}).toReal * (ν .univ).toReal := by by_cases hπ_true : π {true} = 0 · simp [hπ_true, bayesBinaryRisk_of_measure_true_eq_zero] rw [Measure.integral_toReal_rnDeriv @@ -615,15 +614,14 @@ lemma toReal_bayesBinaryRisk_eq_integral_abs (μ ν : Measure 𝒳) [IsFiniteMea lemma bayesBinaryRisk_eq_lintegral_ennnorm (μ ν : Measure 𝒳) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (π : Measure Bool) [IsFiniteMeasure π] : - bayesBinaryRisk μ ν π = 2⁻¹ * (((twoHypKernel μ ν ∘ₘ π) Set.univ) + bayesBinaryRisk μ ν π = 2⁻¹ * (((twoHypKernel μ ν ∘ₘ π) .univ) - ∫⁻ x, ‖(π {false} * (∂μ/∂(twoHypKernel μ ν ∘ₘ π)) x).toReal - (π {true} * (∂ν/∂(twoHypKernel μ ν ∘ₘ π)) x).toReal‖₊ ∂(twoHypKernel μ ν ∘ₘ π)) := by rw [← ENNReal.ofReal_toReal (bayesBinaryRisk_ne_top μ ν π), toReal_bayesBinaryRisk_eq_integral_abs, ENNReal.ofReal_mul (inv_nonneg.mpr zero_le_two), ENNReal.ofReal_inv_of_pos zero_lt_two, ENNReal.ofReal_ofNat, ENNReal.ofReal_sub _ (by positivity), ENNReal.ofReal_toReal (measure_ne_top _ _), - MeasureTheory.ofReal_integral_eq_lintegral_ofReal _ - (.of_forall fun _ ↦ by positivity)] + ofReal_integral_eq_lintegral_ofReal _ (.of_forall fun _ ↦ by positivity)] swap · refine ⟨Measurable.aestronglyMeasurable (by fun_prop), ?_⟩ simp_rw [HasFiniteIntegral, Real.nnnorm_abs] @@ -647,7 +645,7 @@ lemma bayesBinaryRisk_eq_lintegral_ennnorm (μ ν : Measure 𝒳) [IsFiniteMeasu gcongr <;> · rw [Real.ennnorm_eq_ofReal_abs, ENNReal.abs_toReal] exact ENNReal.ofReal_toReal_le - _ = π {false} * μ Set.univ + π {true} * ν Set.univ := by + _ = π {false} * μ .univ + π {true} * ν .univ := by congr 1 · by_cases h_false : π {false} = 0 · rw [h_false, zero_mul, zero_mul] diff --git a/TestingLowerBounds/Testing/ChangeMeasure.lean b/TestingLowerBounds/Testing/ChangeMeasure.lean index 8eee8f4d..492795dd 100644 --- a/TestingLowerBounds/Testing/ChangeMeasure.lean +++ b/TestingLowerBounds/Testing/ChangeMeasure.lean @@ -44,7 +44,7 @@ lemma setLIntegral_nnnorm_exp_neg_llr_le [SigmaFinite ν] [SigmaFinite μ] rw [hx] _ = ∫⁻ a in t, ν.rnDeriv μ a ∂μ := by refine setLIntegral_congr_fun ht ?_ - filter_upwards [Measure.rnDeriv_ne_top ν μ] with x hx _ + filter_upwards [ν.rnDeriv_ne_top μ] with x hx _ rw [← ofReal_norm_eq_coe_nnnorm] simp [hx] _ ≤ ν t := Measure.setLIntegral_rnDeriv_le t diff --git a/TestingLowerBounds/Testing/Risk.lean b/TestingLowerBounds/Testing/Risk.lean index 1a38a1a9..2b018a38 100644 --- a/TestingLowerBounds/Testing/Risk.lean +++ b/TestingLowerBounds/Testing/Risk.lean @@ -92,7 +92,7 @@ lemma bayesianRisk_le_iSup_risk (E : estimationProblem Θ 𝒴 𝒵) (P : Kernel lemma bayesianRisk_comap_measurableEquiv (E : estimationProblem Θ 𝒴 𝒵) (P : Kernel Θ 𝒳) [IsSFiniteKernel P] (κ : Kernel 𝒳 𝒵) [IsSFiniteKernel κ] (π : Measure Θ) (e : Θ ≃ᵐ Θ') : - bayesianRisk (E.comap e.symm e.symm.measurable) (Kernel.comap P e.symm e.symm.measurable) + bayesianRisk (E.comap e.symm e.symm.measurable) (P.comap e.symm e.symm.measurable) κ (π.map e) = bayesianRisk E P κ π := by simp only [bayesianRisk, risk, estimationProblem.comap_y, Function.comp_apply, estimationProblem.comap_ℓ] @@ -100,7 +100,7 @@ lemma bayesianRisk_comap_measurableEquiv (E : estimationProblem Θ 𝒴 𝒵) (P · congr with θ congr -- todo: `congr with z hz` gives a warning. bug. ext z hz - · rw [Kernel.comp_apply' _ _ _ hz, Kernel.comp_apply' _ _ _ hz, Kernel.comap_apply] + · rw [κ.comp_apply' _ _ hz, κ.comp_apply' _ _ hz, Kernel.comap_apply] simp · simp · refine Measurable.lintegral_kernel_prod_right ?_ @@ -119,7 +119,7 @@ lemma bayesRiskPrior_le_bayesRiskPrior_comp (E : estimationProblem Θ 𝒴 𝒵) bayesRiskPrior E P π ≤ bayesRiskPrior E (η ∘ₖ P) π := by simp only [bayesRiskPrior, bayesianRisk, risk, le_iInf_iff] intro κ hκ - rw [← Kernel.comp_assoc κ η] + rw [← κ.comp_assoc η] exact iInf_le_of_le (κ ∘ₖ η) (iInf_le_of_le inferInstance le_rfl) /-- An estimator is a Bayes estimator for a prior `π` if it attains the Bayes risk for `π`. -/ @@ -160,7 +160,7 @@ lemma bayesRiskPrior_compProd_le_bayesRiskPrior (E : estimationProblem Θ 𝒴 exact bayesRiskPrior_le_bayesRiskPrior_comp _ _ _ _ -- Do we also need a version without the `IsMarkovKernel` assumption? it would be of the form: --- `bayesRiskPrior E π ≤ ⨅ z : 𝒵, ∫⁻ θ, E.ℓ (E.y θ, z) * (E.P θ) Set.univ ∂π` +-- `bayesRiskPrior E π ≤ ⨅ z : 𝒵, ∫⁻ θ, E.ℓ (E.y θ, z) * (E.P θ) .univ ∂π` lemma bayesRiskPrior_le_inf (E : estimationProblem Θ 𝒴 𝒵) (P : Kernel Θ 𝒳) (π : Measure Θ) [IsMarkovKernel P] : bayesRiskPrior E P π ≤ ⨅ z : 𝒵, ∫⁻ θ, E.ℓ (E.y θ, z) ∂π := by @@ -183,7 +183,7 @@ lemma bayesianRisk_eq_lintegral_bayesInv_prod [StandardBorelSpace Θ] [Nonempty have := E.ℓ_meas have := E.y_meas simp only [bayesianRisk, risk] - rw [← MeasureTheory.Measure.lintegral_compProd (f := fun θz ↦ E.ℓ (E.y θz.1, θz.2)) (by fun_prop)] + rw [← Measure.lintegral_compProd (f := fun θz ↦ E.ℓ (E.y θz.1, θz.2)) (by fun_prop)] congr calc π ⊗ₘ (κ ∘ₖ P) = (Kernel.id ∥ₖ κ) ∘ₘ (π ⊗ₘ P) := Measure.parallelComp_comp_compProd.symm _ = (Kernel.id ∥ₖ κ) ∘ₘ ((P†π) ×ₖ Kernel.id) ∘ₘ P ∘ₘ π := by rw [bayesInv_prod_id_comp] @@ -197,7 +197,7 @@ lemma bayesianRisk_eq_integral_integral_integral [StandardBorelSpace Θ] [Nonemp have := E.ℓ_meas have := E.y_meas rw [bayesianRisk_eq_lintegral_bayesInv_prod, - Measure.lintegral_bind (Kernel.measurable ((P†π) ×ₖ κ)) (by fun_prop)] + Measure.lintegral_bind ((P†π) ×ₖ κ).measurable (by fun_prop)] congr with x rw [Kernel.prod_apply, lintegral_prod_symm' _ (by fun_prop)]