diff --git a/TestingLowerBounds.lean b/TestingLowerBounds.lean index 4bf08a5d..e226cd72 100644 --- a/TestingLowerBounds.lean +++ b/TestingLowerBounds.lean @@ -29,6 +29,7 @@ import TestingLowerBounds.ForMathlib.Measure import TestingLowerBounds.ForMathlib.MonotoneOnTendsto import TestingLowerBounds.ForMathlib.RadonNikodym import TestingLowerBounds.ForMathlib.RnDeriv +import TestingLowerBounds.ForMathlib.SetIntegral import TestingLowerBounds.Kernel.Basic import TestingLowerBounds.Kernel.BayesInv import TestingLowerBounds.Kernel.Monoidal diff --git a/TestingLowerBounds/DerivAtTop.lean b/TestingLowerBounds/DerivAtTop.lean index f46d16dc..a59213b8 100644 --- a/TestingLowerBounds/DerivAtTop.lean +++ b/TestingLowerBounds/DerivAtTop.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Rémy Degenne -/ import TestingLowerBounds.Convex +import TestingLowerBounds.ForMathlib.LeftRightDeriv +import TestingLowerBounds.ForMathlib.EReal /-! @@ -23,156 +25,236 @@ import TestingLowerBounds.Convex -/ -open Real MeasureTheory Filter +open Real MeasureTheory Filter Set open scoped ENNReal NNReal Topology -namespace ProbabilityTheory +lemma EReal.tendsto_of_monotone {ι : Type*} [Preorder ι] {f : ι → EReal} (hf : Monotone f) : + ∃ y, Tendsto f atTop (𝓝 y) := + ⟨_, tendsto_atTop_ciSup hf (OrderTop.bddAbove _)⟩ + +lemma EReal.tendsto_of_monotoneOn {ι : Type*} [SemilatticeSup ι] [Nonempty ι] {x : ι} + {f : ι → EReal} (hf : MonotoneOn f (Ici x)) : + ∃ y, Tendsto f atTop (𝓝 y) := by + classical + suffices ∃ y, Tendsto (fun z ↦ if x ≤ z then f z else f x) atTop (𝓝 y) by + obtain ⟨y, hy⟩ := this + refine ⟨y, ?_⟩ + refine (tendsto_congr' ?_).mp hy + rw [EventuallyEq, eventually_atTop] + exact ⟨x, fun z hz ↦ if_pos hz⟩ + refine EReal.tendsto_of_monotone (fun y z hyz ↦ ?_) + split_ifs with hxy hxz hxz + · exact hf hxy hxz hyz + · exact absurd (hxy.trans hyz) hxz + · exact hf le_rfl hxz hxz + · exact le_rfl + +lemma Real.monotone_toEReal : Monotone toEReal := Monotone.of_map_inf fun _ ↦ congrFun rfl variable {α β : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} - {μ ν : Measure α} {f g : ℝ → ℝ} + {μ ν : Measure α} {f g : ℝ → ℝ} {x : ℝ} + +lemma ite_bot_ae_eq_atTop (f : ℝ → EReal) : + (fun x ↦ if 1 ≤ x then f x else ⊥) =ᶠ[atTop] f := by + rw [Filter.EventuallyEq, eventually_atTop] + exact ⟨1, fun x hx ↦ by simp [hx]⟩ + +-- The constant 1 chosen here is an arbitrary number greater than 0. +lemma MonotoneOn.monotone_ite_bot (hf : MonotoneOn (rightDeriv f) (Ioi 0)) : + Monotone (fun x ↦ if 1 ≤ x then (rightDeriv f x : EReal) else ⊥) := by + intro x y hxy + cases le_or_lt 1 x with + | inl hx => + simp only [hx, hx.trans hxy, ↓reduceIte] + norm_cast + exact (hf.mono (Ici_subset_Ioi.mpr zero_lt_one)) hx (hx.trans hxy) hxy + | inr hx => + simp only [not_le.mpr hx, ↓reduceIte, bot_le] --- we put the coe outside the limsup to ensure it's not ⊥ -open Classical in noncomputable -def derivAtTop (f : ℝ → ℝ) : EReal := - if Tendsto (fun x ↦ f x / x) atTop atTop then ⊤ else ↑(limsup (fun x ↦ f x / x) atTop) - -lemma bot_lt_derivAtTop : ⊥ < derivAtTop f := by - rw [derivAtTop] - split_ifs with h <;> simp - -lemma derivAtTop_ne_bot : derivAtTop f ≠ ⊥ := bot_lt_derivAtTop.ne' - -lemma derivAtTop_eq_top_iff : derivAtTop f = ⊤ ↔ Tendsto (fun x ↦ f x / x) atTop atTop := by - rw [derivAtTop] - split_ifs with h <;> simp [h] - -lemma derivAtTop_of_tendsto {y : ℝ} (h : Tendsto (fun x ↦ f x / x) atTop (𝓝 y)) : - derivAtTop f = y := by - rw [derivAtTop, if_neg] - · rw [h.limsup_eq] - · exact h.not_tendsto (disjoint_nhds_atTop _) - -@[simp] -lemma derivAtTop_const (c : ℝ) : derivAtTop (fun _ ↦ c) = 0 := by - refine derivAtTop_of_tendsto (Tendsto.div_atTop (tendsto_const_nhds) tendsto_id) +def derivAtTop (f : ℝ → ℝ) : EReal := limsup (fun x ↦ (rightDeriv f x : EReal)) atTop + +lemma derivAtTop_congr (h : f =ᶠ[atTop] g) : derivAtTop f = derivAtTop g := by + simp_rw [derivAtTop] + refine limsup_congr ?_ + filter_upwards [rightDeriv_congr_atTop h] with x hx + rw [hx] + +lemma derivAtTop_congr_nonneg (h : ∀ x, 0 ≤ x → f x = g x) : derivAtTop f = derivAtTop g := by + refine derivAtTop_congr ?_ + rw [Filter.EventuallyEq, eventually_atTop] + exact ⟨0, h⟩ + +lemma derivAtTop_eq_limsup_extendBotLtOne : + derivAtTop f = limsup (fun x ↦ if 1 ≤ x then (rightDeriv f x : EReal) else ⊥) atTop := by + refine limsup_congr ?_ + filter_upwards [ite_bot_ae_eq_atTop (fun x ↦ (rightDeriv f x : EReal))] with x hx + rw [hx] + +lemma tendsto_extendBotLtOne_rightDeriv_iff {y : EReal} : + Tendsto (fun x ↦ if 1 ≤ x then (rightDeriv f x : EReal) else ⊥) atTop (𝓝 y) + ↔ Tendsto (fun x ↦ (rightDeriv f x : EReal)) atTop (𝓝 y) := by + refine tendsto_congr' ?_ + filter_upwards [ite_bot_ae_eq_atTop (fun x ↦ (rightDeriv f x : EReal))] with x hx + rw [hx] + +lemma derivAtTop_of_tendsto {y : EReal} + (h : Tendsto (fun x ↦ (rightDeriv f x : EReal)) atTop (𝓝 y)) : + derivAtTop f = y := h.limsup_eq + +lemma derivAtTop_of_tendsto_nhds {y : ℝ} (h : Tendsto (rightDeriv f) atTop (𝓝 y)) : + derivAtTop f = y := + derivAtTop_of_tendsto ((continuous_coe_real_ereal.tendsto _).comp h) + +lemma derivAtTop_of_tendsto_atTop (h : Tendsto (rightDeriv f) atTop atTop) : + derivAtTop f = ⊤ := by + refine derivAtTop_of_tendsto ?_ + rw [EReal.tendsto_nhds_top_iff_real] + simp only [EReal.coe_lt_coe_iff, eventually_atTop, ge_iff_le] + rw [tendsto_atTop_atTop] at h + intro x + obtain ⟨a, ha⟩ := h (x + 1) + exact ⟨a, fun b hab ↦ (lt_add_one _).trans_le (ha b hab)⟩ @[simp] -lemma derivAtTop_id : derivAtTop id = 1 := by - refine derivAtTop_of_tendsto ?_ - refine (tendsto_congr' ?_).mp tendsto_const_nhds - simp only [EventuallyEq, id_eq, eventually_atTop, ge_iff_le] - refine ⟨1, fun x hx ↦ (div_self ?_).symm⟩ - linarith +lemma derivAtTop_zero : derivAtTop 0 = 0 := by + refine derivAtTop_of_tendsto_nhds ?_ + simp only [rightDeriv_zero] + exact tendsto_const_nhds @[simp] -lemma derivAtTop_id' : derivAtTop (fun x ↦ x) = 1 := derivAtTop_id - -lemma tendsto_derivAtTop (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (h : derivAtTop f ≠ ⊤) : - Tendsto (fun x ↦ f x / x) atTop (𝓝 (derivAtTop f).toReal) := by - rw [ne_eq, derivAtTop_eq_top_iff] at h - obtain ⟨l, h'⟩ : ∃ l, Tendsto (fun x ↦ f x / x) atTop (𝓝 l) := - hf_cvx.slope_tendsto_atTop.resolve_left h - rw [derivAtTop, if_neg h, h'.limsup_eq, EReal.toReal_coe] - exact h' - -lemma tendsto_slope_derivAtTop (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (h : derivAtTop f ≠ ⊤) (y : ℝ) : - Tendsto (fun x ↦ (f x - f y) / (x - y)) atTop (𝓝 (derivAtTop f).toReal) := by - sorry - -lemma toReal_derivAtTop_eq_limsup_slope (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (h : derivAtTop f ≠ ⊤) - (y : ℝ) : - (derivAtTop f).toReal = limsup (fun x ↦ (f x - f y) / (x - y)) atTop := by - rw [(tendsto_slope_derivAtTop hf_cvx h y).limsup_eq] - -lemma derivAtTop_eq_limsup_slope (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (h : derivAtTop f ≠ ⊤) - (y : ℝ) : - derivAtTop f = limsup (fun x ↦ (f x - f y) / (x - y)) atTop := by - rw [← toReal_derivAtTop_eq_limsup_slope hf_cvx h y, EReal.coe_toReal h derivAtTop_ne_bot] - -lemma derivAtTop_add (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hg_cvx : ConvexOn ℝ (Set.Ici 0) g) : - derivAtTop (fun x ↦ f x + g x) = derivAtTop f + derivAtTop g := by - by_cases hf :derivAtTop f = ⊤ - · rw [hf, EReal.top_add_of_ne_bot derivAtTop_ne_bot, derivAtTop_eq_top_iff] - simp_rw [add_div] - by_cases hg : derivAtTop g = ⊤ - · rw [derivAtTop_eq_top_iff] at hg - exact tendsto_atTop_add (derivAtTop_eq_top_iff.mp hf) hg - · exact Tendsto.atTop_add (derivAtTop_eq_top_iff.mp hf) (tendsto_derivAtTop hg_cvx hg) - · by_cases hg : derivAtTop g = ⊤ - · rw [hg, EReal.add_top_of_ne_bot derivAtTop_ne_bot, derivAtTop_eq_top_iff] - simp_rw [add_div] - exact Tendsto.add_atTop (tendsto_derivAtTop hf_cvx hf) (derivAtTop_eq_top_iff.mp hg) - · have hf' := tendsto_derivAtTop hf_cvx hf - have hg' := tendsto_derivAtTop hg_cvx hg - lift derivAtTop f to ℝ using ⟨hf, derivAtTop_ne_bot⟩ with df - lift derivAtTop g to ℝ using ⟨hg, derivAtTop_ne_bot⟩ with dg - refine derivAtTop_of_tendsto ?_ - simp_rw [add_div] - exact hf'.add hg' - -lemma derivAtTop_add' (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hg_cvx : ConvexOn ℝ (Set.Ici 0) g) : +lemma derivAtTop_const (c : ℝ) : derivAtTop (fun _ ↦ c) = 0 := by + refine derivAtTop_of_tendsto_nhds ?_ + simp only [rightDeriv_const] + exact tendsto_const_nhds + +@[simp] lemma derivAtTop_id : derivAtTop id = 1 := derivAtTop_of_tendsto_nhds (by simp) + +@[simp] lemma derivAtTop_id' : derivAtTop (fun x ↦ x) = 1 := derivAtTop_id + +lemma MonotoneOn.tendsto_derivAtTop (hf : MonotoneOn (rightDeriv f) (Ioi 0)) : + Tendsto (fun x ↦ (rightDeriv f x : EReal)) atTop (𝓝 (derivAtTop f)) := by + have hf_coe : MonotoneOn (fun x ↦ (rightDeriv f x : EReal)) (Ici 1) := + Real.monotone_toEReal.comp_monotoneOn (hf.mono (Ici_subset_Ioi.mpr zero_lt_one)) + obtain ⟨z, hz⟩ : ∃ z, Tendsto (fun x ↦ (rightDeriv f x : EReal)) atTop (𝓝 z) := + EReal.tendsto_of_monotoneOn hf_coe + rwa [derivAtTop_of_tendsto hz] + +lemma ConvexOn.tendsto_derivAtTop (hf : ConvexOn ℝ (Ici 0) f) : + Tendsto (fun x ↦ (rightDeriv f x : EReal)) atTop (𝓝 (derivAtTop f)) := + hf.rightDeriv_mono'.tendsto_derivAtTop + +lemma MonotoneOn.derivAtTop_eq_iff {y : EReal} (hf : MonotoneOn (rightDeriv f) (Ioi 0)) : + derivAtTop f = y ↔ Tendsto (fun x ↦ (rightDeriv f x : EReal)) atTop (𝓝 y) := by + refine ⟨fun h ↦ ?_, fun h ↦ derivAtTop_of_tendsto h⟩ + have h_tendsto := hf.tendsto_derivAtTop + rwa [h] at h_tendsto + +lemma ConvexOn.derivAtTop_eq_iff {y : EReal} (hf : ConvexOn ℝ (Ici 0) f) : + derivAtTop f = y ↔ Tendsto (fun x ↦ (rightDeriv f x : EReal)) atTop (𝓝 y) := + hf.rightDeriv_mono'.derivAtTop_eq_iff + +lemma MonotoneOn.derivAtTop_ne_bot (hf : MonotoneOn (rightDeriv f) (Ioi 0)) : derivAtTop f ≠ ⊥ := by + intro h_eq + rw [hf.derivAtTop_eq_iff, ← tendsto_extendBotLtOne_rightDeriv_iff] at h_eq + have h_le := hf.monotone_ite_bot.ge_of_tendsto h_eq 1 + simp at h_le + +lemma ConvexOn.derivAtTop_ne_bot (hf : ConvexOn ℝ (Ici 0) f) : derivAtTop f ≠ ⊥ := + hf.rightDeriv_mono'.derivAtTop_ne_bot + +lemma MonotoneOn.tendsto_toReal_derivAtTop (hf : MonotoneOn (rightDeriv f) (Ioi 0)) + (h_top : derivAtTop f ≠ ⊤) : + Tendsto (rightDeriv f) atTop (𝓝 (derivAtTop f).toReal) := by + have h_tendsto : Tendsto (fun x ↦ (rightDeriv f x : EReal)) atTop (𝓝 (derivAtTop f)) := + hf.tendsto_derivAtTop + have h_toReal : rightDeriv f = fun x ↦ (rightDeriv f x : EReal).toReal := by ext; simp + rw [h_toReal] + exact (EReal.tendsto_toReal h_top hf.derivAtTop_ne_bot).comp h_tendsto + +lemma ConvexOn.tendsto_toReal_derivAtTop (hf : ConvexOn ℝ (Ici 0) f) (h_top : derivAtTop f ≠ ⊤) : + Tendsto (rightDeriv f) atTop (𝓝 (derivAtTop f).toReal) := + hf.rightDeriv_mono'.tendsto_toReal_derivAtTop h_top + +lemma derivAtTop_add' (hf_cvx : ConvexOn ℝ (Ici 0) f) (hg_cvx : ConvexOn ℝ (Ici 0) g) : derivAtTop (f + g) = derivAtTop f + derivAtTop g := by - rw [← derivAtTop_add hf_cvx hg_cvx] - rfl - -lemma derivAtTop_add_const (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (c : ℝ) : - derivAtTop (fun x ↦ f x + c) = derivAtTop f := by - by_cases hf : derivAtTop f = ⊤ - · rw [hf, derivAtTop_eq_top_iff] - simp_rw [add_div] - refine Tendsto.atTop_add (derivAtTop_eq_top_iff.mp hf) (C := 0) ?_ - exact Tendsto.div_atTop tendsto_const_nhds tendsto_id - · have h_tendsto := tendsto_derivAtTop hf_cvx hf - lift derivAtTop f to ℝ using ⟨hf, derivAtTop_ne_bot⟩ with df - refine derivAtTop_of_tendsto ?_ - simp_rw [add_div] - rw [← add_zero df] - exact h_tendsto.add (Tendsto.div_atTop tendsto_const_nhds tendsto_id) - -lemma derivAtTop_sub_const (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (c : ℝ) : + rw [(hf_cvx.add hg_cvx).derivAtTop_eq_iff] + suffices Tendsto (fun x ↦ (rightDeriv f x : EReal) + ↑(rightDeriv g x)) atTop + (𝓝 (derivAtTop f + derivAtTop g)) by + refine (tendsto_congr' ?_).mp this + rw [EventuallyEq, eventually_atTop] + refine ⟨1, fun x hx ↦ ?_⟩ + change _ = ↑(rightDeriv (fun x ↦ f x + g x) x) + rw [rightDeriv_add_apply' (hf_cvx.differentiableWithinAt_Ioi' (zero_lt_one.trans_le hx)) + (hg_cvx.differentiableWithinAt_Ioi' (zero_lt_one.trans_le hx))] + simp only [EReal.coe_add] + have h_cont : ContinuousAt (fun p : (EReal × EReal) ↦ p.1 + p.2) (derivAtTop f, derivAtTop g) := + EReal.continuousAt_add (p := (derivAtTop f, derivAtTop g)) (Or.inr hg_cvx.derivAtTop_ne_bot) + (Or.inl hf_cvx.derivAtTop_ne_bot) + change Tendsto ((fun p : (EReal × EReal) ↦ p.1 + p.2) + ∘ (fun x ↦ (↑(rightDeriv f x), ↑(rightDeriv g x)))) + atTop (𝓝 (derivAtTop f + derivAtTop g)) + exact h_cont.tendsto.comp (hf_cvx.tendsto_derivAtTop.prod_mk_nhds hg_cvx.tendsto_derivAtTop) + +lemma derivAtTop_add (hf_cvx : ConvexOn ℝ (Ici 0) f) (hg_cvx : ConvexOn ℝ (Ici 0) g) : + derivAtTop (fun x ↦ f x + g x) = derivAtTop f + derivAtTop g := derivAtTop_add' hf_cvx hg_cvx + +lemma derivAtTop_add_const (hf_cvx : ConvexOn ℝ (Ici 0) f) (c : ℝ) : + derivAtTop (fun x ↦ f x + c) = derivAtTop f := + (derivAtTop_add' hf_cvx (convexOn_const _ (convex_Ici 0))).trans (by simp) + +lemma derivAtTop_const_add (hf_cvx : ConvexOn ℝ (Ici 0) f) (c : ℝ) : + derivAtTop (fun x ↦ c + f x) = derivAtTop f := + (derivAtTop_add' (convexOn_const _ (convex_Ici 0)) hf_cvx).trans (by simp) + +lemma derivAtTop_sub_const (hf_cvx : ConvexOn ℝ (Ici 0) f) (c : ℝ) : derivAtTop (fun x ↦ f x - c) = derivAtTop f := by simp_rw [sub_eq_add_neg] exact derivAtTop_add_const hf_cvx _ -lemma derivAtTop_const_mul (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) {c : ℝ} (hc : 0 < c) : - derivAtTop (fun x ↦ c * f x) = c * derivAtTop f := by - by_cases h : Tendsto (fun x ↦ f x / x) atTop atTop - · rw [derivAtTop_eq_top_iff.mpr h, derivAtTop_eq_top_iff.mpr, EReal.mul_top_of_pos] - · exact mod_cast hc - · simp_rw [mul_div_assoc] - exact Tendsto.const_mul_atTop hc h - · have h_top : derivAtTop f ≠ ⊤ := by - refine fun h_eq ↦ h ?_ - rwa [← derivAtTop_eq_top_iff] - have : derivAtTop f = ↑(derivAtTop f).toReal := by - rw [EReal.coe_toReal h_top derivAtTop_ne_bot] - rw [this, ← EReal.coe_mul] - refine derivAtTop_of_tendsto ?_ - simp_rw [mul_div_assoc] - exact (tendsto_derivAtTop hf_cvx h_top).const_mul _ - -lemma derivAtTop_const_mul_of_ne_top (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) - (h_deriv : derivAtTop f ≠ ⊤) (c : ℝ) : +lemma derivAtTop_const_mul (hf_cvx : ConvexOn ℝ (Ici 0) f) {c : ℝ} (hc : c ≠ 0) : derivAtTop (fun x ↦ c * f x) = c * derivAtTop f := by - have h_tendsto := tendsto_derivAtTop hf_cvx h_deriv - lift derivAtTop f to ℝ using ⟨h_deriv, derivAtTop_ne_bot⟩ with df - rw [← EReal.coe_mul] refine derivAtTop_of_tendsto ?_ - simp_rw [mul_div_assoc] - exact h_tendsto.const_mul c - -lemma slope_le_derivAtTop (h_cvx : ConvexOn ℝ (Set.Ici 0) f) + simp only [rightDeriv_const_mul, EReal.coe_mul] + have h_cont : ContinuousAt (fun p : (EReal × EReal) ↦ p.1 * p.2) (↑c, derivAtTop f) := + EReal.continuousAt_mul (p := (c, derivAtTop f)) (Or.inr hf_cvx.derivAtTop_ne_bot) + (Or.inl ?_) (Or.inl (by simp)) (Or.inl (by simp)) + swap; · simp only [ne_eq, EReal.coe_eq_zero]; exact hc + change Tendsto ((fun p : (EReal × EReal) ↦ p.1 * p.2) ∘ (fun x ↦ (↑c, ↑(rightDeriv f x)))) + atTop (𝓝 (↑c * derivAtTop f)) + exact h_cont.tendsto.comp (tendsto_const_nhds.prod_mk_nhds hf_cvx.tendsto_derivAtTop) + +lemma slope_le_rightDeriv (h_cvx : ConvexOn ℝ (Ici 0) f) {x y : ℝ} (hx : 0 ≤ x) (hxy : x < y) : + (f y - f x) / (y - x) ≤ rightDeriv f y := by + rw [h_cvx.rightDeriv_eq_sInf_slope' (hx.trans_lt hxy)] + refine le_csInf nonempty_of_nonempty_subtype (fun b hb ↦ ?_) + obtain ⟨z, hyz, rfl⟩ := hb + simp only [mem_Ioi] at hyz + rw [← slope_def_field, slope_comm] + refine h_cvx.slope_mono (hx.trans hxy.le) ?_ ?_ (hxy.trans hyz).le + · simp only [mem_diff, mem_Ici, mem_singleton_iff] + exact ⟨hx, hxy.ne⟩ + · simp only [mem_diff, mem_Ici, mem_singleton_iff] + exact ⟨(hx.trans hxy.le).trans hyz.le, hyz.ne'⟩ + +lemma rightDeriv_le_toReal_derivAtTop (h_cvx : ConvexOn ℝ (Ici 0) f) (h : derivAtTop f ≠ ⊤) + (hx : 0 < x) : + rightDeriv f x ≤ (derivAtTop f).toReal := by + have h_tendsto := h_cvx.tendsto_toReal_derivAtTop h + refine ge_of_tendsto h_tendsto ?_ + rw [eventually_atTop] + refine ⟨max 1 x, fun y hy ↦ h_cvx.rightDeriv_mono' hx ?_ ?_⟩ + · exact mem_Ioi.mpr (hx.trans_le ((le_max_right _ _).trans hy)) + · exact (le_max_right _ _).trans hy + +lemma slope_le_derivAtTop (h_cvx : ConvexOn ℝ (Ici 0) f) (h : derivAtTop f ≠ ⊤) {x y : ℝ} (hx : 0 ≤ x) (hxy : x < y) : - (f y - f x) / (y - x) ≤ (derivAtTop f).toReal := by - refine Monotone.ge_of_tendsto (f := fun y ↦ (f y - f x) / (y - x)) ?_ ?_ y - · have h_mono : ∀ z, y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y) := - fun z hyz ↦ ConvexOn.slope_mono_adjacent h_cvx hx (hx.trans (hxy.trans hyz).le) hxy hyz - sorry -- not true. Need to restrict to (x, ∞) - · exact tendsto_slope_derivAtTop h_cvx h x - -lemma le_add_derivAtTop (h_cvx : ConvexOn ℝ (Set.Ici 0) f) + (f y - f x) / (y - x) ≤ (derivAtTop f).toReal := + (slope_le_rightDeriv h_cvx hx hxy).trans + (rightDeriv_le_toReal_derivAtTop h_cvx h (hx.trans_lt hxy)) + +lemma le_add_derivAtTop (h_cvx : ConvexOn ℝ (Ici 0) f) (h : derivAtTop f ≠ ⊤) {x y : ℝ} (hy : 0 ≤ y) (hyx : y ≤ x) : f x ≤ f y + (derivAtTop f).toReal * (x - y) := by cases eq_or_lt_of_le hyx with @@ -182,14 +264,14 @@ lemma le_add_derivAtTop (h_cvx : ConvexOn ℝ (Set.Ici 0) f) rwa [div_le_iff, sub_le_iff_le_add'] at h_le simp [h_lt] -lemma le_add_derivAtTop'' (h_cvx : ConvexOn ℝ (Set.Ici 0) f) +lemma le_add_derivAtTop'' (h_cvx : ConvexOn ℝ (Ici 0) f) (h : derivAtTop f ≠ ⊤) {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) : f (x + y) ≤ f x + (derivAtTop f).toReal * y := by have h_le := le_add_derivAtTop h_cvx h hx (x := x + y) ?_ · simpa using h_le · linarith -lemma le_add_derivAtTop' (h_cvx : ConvexOn ℝ (Set.Ici 0) f) +lemma le_add_derivAtTop' (h_cvx : ConvexOn ℝ (Ici 0) f) (h : derivAtTop f ≠ ⊤) {x u : ℝ} (hx : 0 ≤ x) (hu : 0 ≤ u) (hu' : u ≤ 1) : f x ≤ f (x * u) + (derivAtTop f).toReal * x * (1 - u) := by by_cases hx0 : x = 0 @@ -200,7 +282,7 @@ lemma le_add_derivAtTop' (h_cvx : ConvexOn ℝ (Set.Ici 0) f) exact hx.lt_of_ne' hx0 rwa [mul_assoc, mul_sub, mul_one] -lemma toReal_le_add_derivAtTop (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) {a b : ENNReal} +lemma toReal_le_add_derivAtTop (hf_cvx : ConvexOn ℝ (Ici 0) f) {a b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) : f ((a + b).toReal) ≤ f a.toReal + derivAtTop f * b := by by_cases hf_top : derivAtTop f = ⊤ @@ -214,11 +296,9 @@ lemma toReal_le_add_derivAtTop (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) {a b : ENNR · simp [ha, hb] · simp have h := le_add_derivAtTop hf_cvx hf_top (ENNReal.toReal_nonneg : 0 ≤ a.toReal) h_le - lift derivAtTop f to ℝ using ⟨hf_top, derivAtTop_ne_bot⟩ with df + lift derivAtTop f to ℝ using ⟨hf_top, hf_cvx.derivAtTop_ne_bot⟩ with df rw [← EReal.coe_ennreal_toReal hb] norm_cast refine h.trans_eq ?_ congr rw [sub_eq_iff_eq_add, ← ENNReal.toReal_add hb ha, add_comm] - -end ProbabilityTheory diff --git a/TestingLowerBounds/Divergences/Hellinger.lean b/TestingLowerBounds/Divergences/Hellinger.lean index e2e01782..e144f945 100644 --- a/TestingLowerBounds/Divergences/Hellinger.lean +++ b/TestingLowerBounds/Divergences/Hellinger.lean @@ -222,17 +222,16 @@ lemma convexOn_hellingerFun (ha_pos : 0 ≤ a) : ConvexOn ℝ (Set.Ici 0) (helli refine ConvexOn.smul (by simp [ha.le]) ?_ exact h.sub (concaveOn_const _ (convex_Ici 0)) -lemma tendsto_hellingerFun_div_atTop_of_one_lt (ha : 1 < a) : - Tendsto (fun x ↦ hellingerFun a x / x) atTop atTop := by +lemma tendsto_rightDeriv_hellingerFun_atTop_of_one_lt (ha : 1 < a) : + Tendsto (rightDeriv (hellingerFun a)) atTop atTop := by sorry -lemma tendsto_hellingerFun_div_atTop_of_lt_one (ha : a < 1) : - Tendsto (fun x ↦ hellingerFun a x / x) atTop (𝓝 0) := by +lemma tendsto_rightDeriv_hellingerFun_atTop_of_lt_one (ha : a < 1) : + Tendsto (rightDeriv (hellingerFun a)) atTop (𝓝 0) := by sorry -lemma derivAtTop_hellingerFun_of_one_lt (ha : 1 < a) : derivAtTop (hellingerFun a) = ⊤ := by - rw [derivAtTop, if_pos] - exact tendsto_hellingerFun_div_atTop_of_one_lt ha +lemma derivAtTop_hellingerFun_of_one_lt (ha : 1 < a) : derivAtTop (hellingerFun a) = ⊤ := + derivAtTop_of_tendsto_atTop <| tendsto_rightDeriv_hellingerFun_atTop_of_one_lt ha lemma derivAtTop_hellingerFun_of_one_le (ha : 1 ≤ a) : derivAtTop (hellingerFun a) = ⊤ := by @@ -243,7 +242,7 @@ lemma derivAtTop_hellingerFun_of_one_le (ha : 1 ≤ a) : lemma derivAtTop_hellingerFun_of_lt_one (ha : a < 1) : derivAtTop (hellingerFun a) = 0 := - derivAtTop_of_tendsto (tendsto_hellingerFun_div_atTop_of_lt_one ha) + derivAtTop_of_tendsto_nhds <| tendsto_rightDeriv_hellingerFun_atTop_of_lt_one ha lemma integrable_hellingerFun_iff_integrable_rpow (ha_one : a ≠ 1) [IsFiniteMeasure ν] : Integrable (fun x ↦ hellingerFun a ((∂μ/∂ν) x).toReal) ν diff --git a/TestingLowerBounds/Divergences/KullbackLeibler.lean b/TestingLowerBounds/Divergences/KullbackLeibler.lean index e6160dbb..544e0f6b 100644 --- a/TestingLowerBounds/Divergences/KullbackLeibler.lean +++ b/TestingLowerBounds/Divergences/KullbackLeibler.lean @@ -61,12 +61,16 @@ lemma kl_toReal_of_ac (h : μ ≪ ν) : (kl μ ν).toReal = ∫ a, llr μ ν a · rw [kl_of_ac_of_integrable h h_int, EReal.toReal_coe] · rw [kl_of_not_integrable h_int, integral_undef h_int, EReal.toReal_top] +lemma rightDeriv_mul_log {x : ℝ} (hx : 0 ≤ x) : rightDeriv (fun x ↦ x * log x) x = log x + 1 := by + sorry + lemma derivAtTop_mul_log : derivAtTop (fun x ↦ x * log x) = ⊤ := by - rw [derivAtTop_eq_top_iff] - refine (tendsto_congr' ?_).mp tendsto_log_atTop - simp only [EventuallyEq, eventually_atTop, ge_iff_le] - refine ⟨1, fun x hx ↦ ?_⟩ - rw [mul_div_cancel_left₀ _ (zero_lt_one.trans_le hx).ne'] + refine derivAtTop_of_tendsto_atTop ?_ + have h_tendsto : Tendsto (fun x ↦ log x + 1) atTop atTop := + tendsto_log_atTop.atTop_add tendsto_const_nhds + refine (tendsto_congr' ?_).mpr h_tendsto + rw [EventuallyEq, eventually_atTop] + exact ⟨0, fun _ ↦ rightDeriv_mul_log⟩ lemma fDiv_mul_log_eq_top_iff [IsFiniteMeasure μ] [SigmaFinite ν] : fDiv (fun x ↦ x * log x) μ ν = ⊤ ↔ μ ≪ ν → ¬ Integrable (llr μ ν) μ := by @@ -405,7 +409,7 @@ lemma condKL_nonneg (κ η : Kernel α β) [IsMarkovKernel κ] [IsMarkovKernel lemma condKL_const {ξ : Measure β} [IsFiniteMeasure ξ] [IsFiniteMeasure μ] [IsFiniteMeasure ν] : condKL (Kernel.const β μ) (Kernel.const β ν) ξ = (kl μ ν) * ξ Set.univ := by rw [condKL_eq_condFDiv, kl_eq_fDiv] - exact condFDiv_const + exact condFDiv_const convexOn_mul_log lemma kl_fst_le [Nonempty β] [StandardBorelSpace β] (μ ν : Measure (α × β)) [IsFiniteMeasure μ] [IsFiniteMeasure ν] : diff --git a/TestingLowerBounds/FDiv/Basic.lean b/TestingLowerBounds/FDiv/Basic.lean index db95dfcc..5b42950d 100644 --- a/TestingLowerBounds/FDiv/Basic.lean +++ b/TestingLowerBounds/FDiv/Basic.lean @@ -23,7 +23,7 @@ import TestingLowerBounds.ForMathlib.RnDeriv ## Implementation details -The most natural type for `f` is `ℝ≥0∞ → EReal` since we apply it to an `ℝ≥0∞`-values RN derivative, +The most natural type for `f` is `ℝ≥0∞ → EReal` since we apply it to an `ℝ≥0∞`-valued RN derivative, and its value can be in general both positive or negative, and potentially +∞. However, we use `ℝ → ℝ` instead, for the following reasons: * domain: convexity results like `ConvexOn.map_average_le` don't work for `ℝ≥0∞` because they @@ -33,7 +33,7 @@ However, we use `ℝ → ℝ` instead, for the following reasons: * codomain: `EReal` is underdeveloped, and all functions we will actually use are finite anyway. Most results will require these conditions on `f`: -`(hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0)) (hf_one : f 1 = 0)` +`(hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) (hf_one : f 1 = 0)` ## References @@ -44,7 +44,7 @@ Most results will require these conditions on `f`: Foobars, barfoos -/ -open Real MeasureTheory Filter +open Real MeasureTheory Filter Set open scoped ENNReal NNReal Topology @@ -65,9 +65,9 @@ lemma integrable_toReal_iff {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) (hf lemma integrable_f_rnDeriv_of_derivAtTop_ne_top (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hf : StronglyMeasurable f) - (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_deriv : derivAtTop f ≠ ⊤) : + (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_deriv : derivAtTop f ≠ ⊤) : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν := by - obtain ⟨c, c', h⟩ : ∃ c c', ∀ x, 0 ≤ x → c * x + c' ≤ f x := + obtain ⟨c, c', h⟩ : ∃ c c', ∀ x, _ → c * x + c' ≤ f x := hf_cvx.exists_affine_le (convex_Ici 0) refine integrable_of_le_of_le (f := fun x ↦ f ((∂μ/∂ν) x).toReal) (g₁ := fun x ↦ c * ((∂μ/∂ν) x).toReal + c') @@ -104,12 +104,12 @@ lemma fDiv_of_mul_eq_top (h : derivAtTop f * μ.singularPart ν Set.univ = ⊤) · rw [fDiv, if_neg (not_not.mpr hf), h, EReal.coe_add_top] · exact fDiv_of_not_integrable hf -lemma fDiv_ne_bot [IsFiniteMeasure μ] : fDiv f μ ν ≠ ⊥ := by +lemma fDiv_ne_bot [IsFiniteMeasure μ] (hf_cvx : ConvexOn ℝ (Ici 0) f) : fDiv f μ ν ≠ ⊥ := by rw [fDiv] split_ifs with h · simp only [ne_eq, EReal.add_eq_bot_iff, EReal.coe_ne_bot, false_or] rw [EReal.mul_eq_bot] - simp [derivAtTop_ne_bot, not_lt.mpr (EReal.coe_ennreal_nonneg _), measure_ne_top] + simp [hf_cvx.derivAtTop_ne_bot, not_lt.mpr (EReal.coe_ennreal_nonneg _), measure_ne_top] · simp lemma fDiv_ne_bot_of_derivAtTop_nonneg (hf : 0 ≤ derivAtTop f) : fDiv f μ ν ≠ ⊥ := by @@ -117,20 +117,31 @@ lemma fDiv_ne_bot_of_derivAtTop_nonneg (hf : 0 ≤ derivAtTop f) : fDiv f μ ν split_ifs with h · simp only [ne_eq, EReal.add_eq_bot_iff, EReal.coe_ne_bot, false_or] rw [EReal.mul_eq_bot] - simp [derivAtTop_ne_bot, not_lt.mpr (EReal.coe_ennreal_nonneg _), not_lt.mpr hf] + have h_ne_bot : derivAtTop f ≠ ⊥ := fun h_eq ↦ by + rw [h_eq] at hf + simp at hf + simp [h_ne_bot, not_lt.mpr (EReal.coe_ennreal_nonneg _), not_lt.mpr hf] · simp @[simp] lemma fDiv_zero (μ ν : Measure α) : fDiv (fun _ ↦ 0) μ ν = 0 := by simp [fDiv] -lemma fDiv_of_eq_on_nonneg (μ ν : Measure α) (h : ∀ x ≥ 0, f x = g x) : +lemma fDiv_congr' (μ ν : Measure α) (hfg : ∀ᵐ x ∂ν.map (fun x ↦ ((∂μ/∂ν) x).toReal), f x = g 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 + rw [fDiv, derivAtTop_congr hfg'] + congr 2 + · exact eq_iff_iff.mpr ⟨fun hf ↦ hf.congr h, fun hf ↦ hf.congr h.symm⟩ + · exact EReal.coe_eq_coe_iff.mpr (integral_congr_ae h) + +lemma fDiv_congr (μ ν : Measure α) (h : ∀ x ≥ 0, f x = g x) : fDiv f μ ν = fDiv g μ ν := by have (x : α) : f ((∂μ/∂ν) x).toReal = g ((∂μ/∂ν) x).toReal := h _ ENNReal.toReal_nonneg - rw [fDiv] - congr 3 - · simp_rw [this] - · simp_rw [this] - sorry --we should add a lemma for derivAtTop saying that if f = g eventually then derivAtTop f = derivAtTop g + simp_rw [fDiv, this, derivAtTop_congr_nonneg h] + congr + simp_rw [this] -- TODO: finish the proof of `fDiv_of_eq_on_nonneg` and use it to shorten the proof of `fDiv_of_zero_on_nonneg`. --the name feels a bit wrong, what could I write instead of `on_nonneg`? @@ -140,7 +151,8 @@ lemma fDiv_of_zero_on_nonneg (μ ν : Measure α) (hf : ∀ x ≥ 0, f x = 0) : rw [fDiv_of_integrable (by simp [this])] simp_rw [this, integral_zero, EReal.coe_zero, zero_add] convert zero_mul _ - exact derivAtTop_of_tendsto (tendsto_atTop_of_eventually_const fun i hi ↦ hf i hi ▸ zero_div _) + rw [derivAtTop_congr_nonneg, derivAtTop_zero] + exact fun x hx ↦ hf x hx @[simp] lemma fDiv_zero_measure (ν : Measure α) [IsFiniteMeasure ν] : fDiv f 0 ν = f 0 * ν Set.univ := by @@ -229,7 +241,7 @@ lemma fDiv_id (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] : lemma fDiv_id' (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν] : fDiv (fun x ↦ x) μ ν = μ Set.univ := fDiv_id μ ν -lemma fDiv_mul {c : ℝ} (hc : 0 ≤ c) (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) +lemma fDiv_mul {c : ℝ} (hc : 0 ≤ c) (hf_cvx : ConvexOn ℝ (Ici 0) f) (μ ν : Measure α) : fDiv (fun x ↦ c * f x) μ ν = c * fDiv f μ ν := by by_cases hc0 : c = 0 @@ -237,7 +249,7 @@ lemma fDiv_mul {c : ℝ} (hc : 0 ≤ c) (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) by_cases h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν · rw [fDiv_of_integrable h_int, fDiv_of_integrable] swap; · exact h_int.const_mul _ - rw [integral_mul_left, derivAtTop_const_mul hf_cvx (lt_of_le_of_ne hc (Ne.symm hc0)), + rw [integral_mul_left, derivAtTop_const_mul hf_cvx hc0, EReal.coe_mul, EReal.coe_mul_add_of_nonneg hc, mul_assoc] · rw [fDiv_of_not_integrable h_int, fDiv_of_not_integrable] · rw [EReal.mul_top_of_pos] @@ -249,15 +261,15 @@ lemma fDiv_mul {c : ℝ} (hc : 0 ≤ c) (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) rw [this] exact h.const_mul _ -lemma fDiv_mul_of_ne_top (c : ℝ) (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (h_top : derivAtTop f ≠ ⊤) +lemma fDiv_mul_of_ne_top (c : ℝ) (hf_cvx : ConvexOn ℝ (Ici 0) f) (h_top : derivAtTop f ≠ ⊤) (μ ν : Measure α) [IsFiniteMeasure μ] (h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) : fDiv (fun x ↦ c * f x) μ ν = c * fDiv f μ ν := by by_cases hc0 : c = 0 · simp [hc0] rw [fDiv_of_integrable h_int, fDiv_of_integrable] swap; · exact h_int.const_mul _ - rw [integral_mul_left, derivAtTop_const_mul_of_ne_top hf_cvx h_top c] - lift derivAtTop f to ℝ using ⟨h_top, derivAtTop_ne_bot⟩ with df + rw [integral_mul_left, derivAtTop_const_mul hf_cvx hc0] + lift derivAtTop f to ℝ using ⟨h_top, hf_cvx.derivAtTop_ne_bot⟩ with df rw [← EReal.coe_ennreal_toReal (measure_ne_top _ _)] norm_cast ring @@ -269,7 +281,7 @@ lemma fDiv_mul_of_ne_top (c : ℝ) (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (h_top -- additional hypothesis it's true. lemma fDiv_add [IsFiniteMeasure μ] (hf : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) (hg : Integrable (fun x ↦ g ((∂μ/∂ν) x).toReal) ν) - (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hg_cvx : ConvexOn ℝ (Set.Ici 0) g) : + (hf_cvx : ConvexOn ℝ (Ici 0) f) (hg_cvx : ConvexOn ℝ (Ici 0) g) : fDiv (fun x ↦ f x + g x) μ ν = fDiv f μ ν + fDiv g μ ν := by rw [fDiv_of_integrable (hf.add hg), integral_add hf hg, fDiv_of_integrable hf, fDiv_of_integrable hg, derivAtTop_add hf_cvx hg_cvx] @@ -378,7 +390,7 @@ lemma fDiv_of_absolutelyContinuous · rw [fDiv_of_not_integrable h_int] lemma fDiv_eq_add_withDensity_singularPart - (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] : + (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hf_cvx : ConvexOn ℝ (Ici 0) f) : fDiv f μ ν = fDiv f (ν.withDensity (∂μ/∂ν)) ν + fDiv f (μ.singularPart ν) ν - f 0 * ν Set.univ := by have h_int_iff : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν @@ -406,16 +418,16 @@ lemma fDiv_eq_add_withDensity_singularPart · simp [h0] · by_cases h_top : derivAtTop f = ⊤ · rw [h_top, EReal.top_mul_ennreal_coe h0, EReal.top_add_top] - · lift derivAtTop f to ℝ using ⟨h_top, derivAtTop_ne_bot⟩ with x + · lift derivAtTop f to ℝ using ⟨h_top, hf_cvx.derivAtTop_ne_bot⟩ with x rw [← EReal.coe_ennreal_toReal (measure_ne_top _ _), ← EReal.coe_mul, EReal.top_add_coe] · rwa [← h_int_iff] lemma fDiv_eq_add_withDensity_singularPart' (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] - (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) : + (hf_cvx : ConvexOn ℝ (Ici 0) f) : fDiv f μ ν = fDiv (fun x ↦ f x - f 0) (ν.withDensity (∂μ/∂ν)) ν + fDiv f (μ.singularPart ν) ν := by - rw [fDiv_eq_add_withDensity_singularPart _ _, fDiv_sub_const, add_sub_assoc, + rw [fDiv_eq_add_withDensity_singularPart _ _ hf_cvx, fDiv_sub_const, add_sub_assoc, sub_eq_add_neg, sub_eq_add_neg, add_assoc] · congr 1 rw [add_comm] @@ -423,16 +435,16 @@ lemma fDiv_eq_add_withDensity_singularPart' lemma fDiv_eq_add_withDensity_singularPart'' (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] - (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) : + (hf_cvx : ConvexOn ℝ (Ici 0) f) : fDiv f μ ν = fDiv f (ν.withDensity (∂μ/∂ν)) ν + fDiv (fun x ↦ f x - f 0) (μ.singularPart ν) ν := by - rw [fDiv_eq_add_withDensity_singularPart _ _, fDiv_sub_const, add_sub_assoc, + rw [fDiv_eq_add_withDensity_singularPart _ _ hf_cvx, fDiv_sub_const, add_sub_assoc, sub_eq_add_neg] exact hf_cvx lemma fDiv_eq_add_withDensity_derivAtTop (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] - (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) : + (hf_cvx : ConvexOn ℝ (Ici 0) f) : fDiv f μ ν = fDiv f (ν.withDensity (∂μ/∂ν)) ν + derivAtTop f * μ.singularPart ν Set.univ := by rw [fDiv_eq_add_withDensity_singularPart'' μ ν hf_cvx, fDiv_of_mutuallySingular (Measure.mutuallySingular_singularPart _ _), @@ -447,7 +459,7 @@ lemma fDiv_lt_top_of_ac (h : μ ≪ ν) (h_int : Integrable (fun x ↦ f ((∂μ lemma fDiv_add_measure_le_of_ac {μ₁ μ₂ ν : Measure α} [IsFiniteMeasure μ₁] [IsFiniteMeasure μ₂] [IsFiniteMeasure ν] (h₁ : μ₁ ≪ ν) (h₂ : μ₂ ≪ ν) - (hf : StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) : + (hf : StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Ici 0) f) : fDiv f (μ₁ + μ₂) ν ≤ fDiv f μ₁ ν + derivAtTop f * μ₂ Set.univ := by classical by_cases hμ₂0 : μ₂ = 0 @@ -470,7 +482,7 @@ lemma fDiv_add_measure_le_of_ac {μ₁ μ₂ ν : Measure α} [IsFiniteMeasure exact le_add_derivAtTop'' hf_cvx h_top ENNReal.toReal_nonneg ENNReal.toReal_nonneg rw [fDiv_of_absolutelyContinuous (Measure.AbsolutelyContinuous.add_left_iff.mpr ⟨h₁, h₂⟩), if_pos h_int_add, fDiv_of_absolutelyContinuous h₁, if_pos h_int] - lift derivAtTop f to ℝ using ⟨h_top, derivAtTop_ne_bot⟩ with df + lift derivAtTop f to ℝ using ⟨h_top, hf_cvx.derivAtTop_ne_bot⟩ with df rw [← EReal.coe_ennreal_toReal (measure_ne_top _ _)] norm_cast calc ∫ x, f ((∂μ₁ + μ₂/∂ν) x).toReal ∂ν @@ -483,7 +495,7 @@ lemma fDiv_add_measure_le_of_ac {μ₁ μ₂ ν : Measure α} [IsFiniteMeasure lemma fDiv_absolutelyContinuous_add_mutuallySingular {μ₁ μ₂ ν : Measure α} [IsFiniteMeasure μ₁] [IsFiniteMeasure μ₂] [IsFiniteMeasure ν] (h₁ : μ₁ ≪ ν) (h₂ : μ₂ ⟂ₘ ν) - (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) : + (hf_cvx : ConvexOn ℝ (Ici 0) f) : fDiv f (μ₁ + μ₂) ν = fDiv f μ₁ ν + derivAtTop f * μ₂ Set.univ := by 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] @@ -496,7 +508,7 @@ lemma fDiv_absolutelyContinuous_add_mutuallySingular {μ₁ μ₂ ν : Measure simp [hx] lemma fDiv_add_measure_le (μ₁ μ₂ ν : Measure α) [IsFiniteMeasure μ₁] [IsFiniteMeasure μ₂] - [IsFiniteMeasure ν] (hf : StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) : + [IsFiniteMeasure ν] (hf : StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Ici 0) f) : fDiv f (μ₁ + μ₂) ν ≤ fDiv f μ₁ ν + derivAtTop f * μ₂ Set.univ := by rw [μ₂.haveLebesgueDecomposition_add ν, μ₁.haveLebesgueDecomposition_add ν] have : μ₁.singularPart ν + ν.withDensity (∂μ₁/∂ν) + (μ₂.singularPart ν + ν.withDensity (∂μ₂/∂ν)) @@ -536,7 +548,7 @@ lemma fDiv_add_measure_le (μ₁ μ₂ ν : Measure α) [IsFiniteMeasure μ₁] rw [add_assoc, EReal.mul_add_coe_of_nonneg _ ENNReal.toReal_nonneg ENNReal.toReal_nonneg] lemma fDiv_le_zero_add_top_of_ac [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hμν : μ ≪ ν) - (hf : StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) : + (hf : StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Ici 0) f) : fDiv f μ ν ≤ f 0 * ν Set.univ + derivAtTop f * μ Set.univ := by classical by_cases hμ : μ = 0 @@ -555,7 +567,7 @@ lemma fDiv_le_zero_add_top_of_ac [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hμ simp only [zero_add] at h rw [← EReal.coe_ennreal_toReal (measure_ne_top _ _), ← EReal.coe_ennreal_toReal (measure_ne_top _ _)] - lift derivAtTop f to ℝ using ⟨h_top, derivAtTop_ne_bot⟩ with df + lift derivAtTop f to ℝ using ⟨h_top, hf_cvx.derivAtTop_ne_bot⟩ with df norm_cast refine (integral_mono h_int ?_ h).trans_eq ?_ · exact (integrable_const _).add (Measure.integrable_toReal_rnDeriv.const_mul _) @@ -565,7 +577,7 @@ lemma fDiv_le_zero_add_top_of_ac [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hμ · exact Measure.integrable_toReal_rnDeriv.const_mul _ lemma fDiv_le_zero_add_top [IsFiniteMeasure μ] [IsFiniteMeasure ν] - (hf : StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) : + (hf : StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Ici 0) f) : fDiv f μ ν ≤ f 0 * ν Set.univ + derivAtTop f * μ Set.univ := by rw [fDiv_eq_add_withDensity_derivAtTop _ _ hf_cvx] calc fDiv f (ν.withDensity (∂μ/∂ν)) ν + derivAtTop f * μ.singularPart ν Set.univ @@ -636,10 +648,13 @@ lemma fDiv_lt_top_of_derivAtTop_ne_top [IsFiniteMeasure μ] (hf : derivAtTop f refine EReal.add_lt_top ?_ ?_ · simp · rw [ne_eq, EReal.mul_eq_top] - simp only [derivAtTop_ne_bot, false_and, EReal.coe_ennreal_ne_bot, and_false, hf, - EReal.coe_ennreal_pos, Measure.measure_univ_pos, ne_eq, EReal.coe_ennreal_eq_top_iff, - false_or, not_and] - exact fun _ ↦ measure_ne_top _ _ + simp only [EReal.coe_ennreal_ne_bot, and_false, EReal.coe_ennreal_pos, Measure.measure_univ_pos, + ne_eq, EReal.coe_ennreal_eq_top_iff, false_or, not_or, not_and, not_lt, not_not] + refine ⟨fun _ ↦ ?_, ?_, ?_⟩ + · norm_cast + exact zero_le' + · simp [hf] + · exact fun _ ↦ measure_ne_top _ _ lemma fDiv_lt_top_iff_of_derivAtTop_ne_top [IsFiniteMeasure μ] (hf : derivAtTop f ≠ ⊤) : fDiv f μ ν < ⊤ ↔ Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν := by @@ -685,7 +700,7 @@ lemma fDiv_of_ne_top (h : fDiv f μ ν ≠ ⊤) : rw [fDiv_of_integrable] exact integrable_of_fDiv_ne_top h -lemma toReal_fDiv_of_integrable [IsFiniteMeasure μ] +lemma toReal_fDiv_of_integrable [IsFiniteMeasure μ] (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) (h_deriv : derivAtTop f = ⊤ → μ ≪ ν) : (fDiv f μ ν).toReal = ∫ y, f ((∂μ/∂ν) y).toReal ∂ν @@ -694,19 +709,19 @@ lemma toReal_fDiv_of_integrable [IsFiniteMeasure μ] rotate_left · simp · simp - · simp only [ne_eq, EReal.mul_eq_top, derivAtTop_ne_bot, false_and, EReal.coe_ennreal_ne_bot, + · 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, derivAtTop_ne_bot, EReal.coe_ennreal_pos, + · simp only [ne_eq, EReal.mul_eq_bot, hf_cvx.derivAtTop_ne_bot, EReal.coe_ennreal_pos, Measure.measure_univ_pos, false_and, EReal.coe_ennreal_ne_bot, and_false, EReal.coe_ennreal_eq_top_iff, measure_ne_top, or_false, false_or, not_and, not_lt] exact fun _ ↦ EReal.coe_ennreal_nonneg _ rfl lemma le_fDiv_of_ac [IsFiniteMeasure μ] [IsProbabilityMeasure ν] - (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0)) + (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) (hμν : μ ≪ ν) : f (μ Set.univ).toReal ≤ fDiv f μ ν := by by_cases hf_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν @@ -722,7 +737,7 @@ lemma le_fDiv_of_ac [IsFiniteMeasure μ] [IsProbabilityMeasure ν] Measure.integrable_toReal_rnDeriv hf_int lemma f_measure_univ_le_add (μ ν : Measure α) [IsFiniteMeasure μ] [IsProbabilityMeasure ν] - (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) : + (hf_cvx : ConvexOn ℝ (Ici 0) f) : f (μ Set.univ).toReal ≤ f (ν.withDensity (∂μ/∂ν) Set.univ).toReal + derivAtTop f * μ.singularPart ν Set.univ := by have : μ Set.univ = ν.withDensity (∂μ/∂ν) Set.univ + μ.singularPart ν Set.univ := by @@ -732,7 +747,7 @@ lemma f_measure_univ_le_add (μ ν : Measure α) [IsFiniteMeasure μ] [IsProbabi exact toReal_le_add_derivAtTop hf_cvx (measure_ne_top _ _) (measure_ne_top _ _) lemma le_fDiv [IsFiniteMeasure μ] [IsProbabilityMeasure ν] - (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0)) : + (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) : f (μ Set.univ).toReal ≤ fDiv f μ ν := by refine (f_measure_univ_le_add μ ν hf_cvx).trans ?_ rw [fDiv_eq_add_withDensity_singularPart'' μ _ hf_cvx, @@ -745,22 +760,37 @@ lemma le_fDiv [IsFiniteMeasure μ] [IsProbabilityMeasure ν] exact le_fDiv_of_ac hf_cvx hf_cont (withDensity_absolutelyContinuous _ _) lemma fDiv_nonneg [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] - (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0)) (hf_one : f 1 = 0) : + (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) (hf_one : f 1 = 0) : 0 ≤ fDiv f μ ν := by calc (0 : EReal) = f (μ Set.univ).toReal := by simp [hf_one] _ ≤ fDiv f μ ν := le_fDiv hf_cvx hf_cont -lemma fDiv_nonneg_of_nonneg (hf : ∀ x, 0 ≤ f x) (hf_atTop : 0 ≤ derivAtTop f) : - 0 ≤ fDiv f μ ν := by - rw [fDiv] - split_ifs - swap; · exact le_top - refine add_nonneg ?_ (mul_nonneg hf_atTop (EReal.coe_ennreal_nonneg _)) - exact EReal.coe_nonneg.mpr <| integral_nonneg_of_ae <| eventually_of_forall <| fun _ ↦ hf _ +/- The hypothesis `hfg'` can maybe become something like `f ≤ᵐ[atTop] g`, but then we would need +some lemma like `derivAtTop_mono`, and I'm not sure this is true in gneral, without any assumption on `f`. +We could prove it if we had some lemma saying that the new derivAtTop is equal to the old definition, +this is probably false in general, but under some assumptions it should be true. -/ +lemma fDiv_mono' (hf_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) + (hfg : f ≤ᵐ[ν.map (fun x ↦ ((∂μ/∂ν) x).toReal)] g) (hfg' : derivAtTop f ≤ derivAtTop g) : + fDiv f μ ν ≤ fDiv g μ ν := by + rw [fDiv_of_integrable hf_int, fDiv] + split_ifs with hg_int + 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 + · exact EReal.coe_ennreal_nonneg _ + +lemma fDiv_mono (hf_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) + (hfg : f ≤ g) (hfg' : derivAtTop f ≤ derivAtTop g) : fDiv f μ ν ≤ fDiv g μ ν := + fDiv_mono' hf_int (eventually_of_forall hfg) hfg' + +lemma fDiv_nonneg_of_nonneg (hf : 0 ≤ f) (hf' : 0 ≤ derivAtTop f) : + 0 ≤ fDiv f μ ν := + fDiv_zero μ ν ▸ fDiv_mono (integrable_zero α ℝ ν) hf (derivAtTop_zero ▸ hf') lemma fDiv_eq_zero_iff [IsFiniteMeasure μ] [IsFiniteMeasure ν] (h_mass : μ Set.univ = ν Set.univ) - (hf_deriv : derivAtTop f = ⊤) (hf_cvx : StrictConvexOn ℝ (Set.Ici 0) f) - (hf_cont : ContinuousOn f (Set.Ici 0)) (hf_one : f 1 = 0) : + (hf_deriv : derivAtTop f = ⊤) (hf_cvx : StrictConvexOn ℝ (Ici 0) f) + (hf_cont : ContinuousOn f (Ici 0)) (hf_one : f 1 = 0) : fDiv f μ ν = 0 ↔ μ = ν := by refine ⟨fun h ↦ ?_, fun h ↦ h ▸ fDiv_self hf_one _⟩ by_cases hμν : μ ≪ ν @@ -783,8 +813,8 @@ lemma fDiv_eq_zero_iff [IsFiniteMeasure μ] [IsFiniteMeasure ν] (h_mass : μ Se (Measure.rnDeriv_ne_top _ _) (eventually_of_forall fun _ ↦ ENNReal.one_ne_top) h_eq lemma fDiv_eq_zero_iff' [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] - (hf_deriv : derivAtTop f = ⊤) (hf_cvx : StrictConvexOn ℝ (Set.Ici 0) f) - (hf_cont : ContinuousOn f (Set.Ici 0)) (hf_one : f 1 = 0) : + (hf_deriv : derivAtTop f = ⊤) (hf_cvx : StrictConvexOn ℝ (Ici 0) f) + (hf_cont : ContinuousOn f (Ici 0)) (hf_one : f 1 = 0) : fDiv f μ ν = 0 ↔ μ = ν := by exact fDiv_eq_zero_iff (by simp) hf_deriv hf_cvx hf_cont hf_one diff --git a/TestingLowerBounds/FDiv/CompProd.lean b/TestingLowerBounds/FDiv/CompProd.lean index 9c55fe69..88778ee0 100644 --- a/TestingLowerBounds/FDiv/CompProd.lean +++ b/TestingLowerBounds/FDiv/CompProd.lean @@ -24,7 +24,7 @@ import Mathlib.Probability.Kernel.Disintegration.Basic -/ -open Real MeasureTheory Filter MeasurableSpace +open Real MeasureTheory Filter MeasurableSpace Set open scoped ENNReal NNReal @@ -46,7 +46,8 @@ lemma fDiv_ae_ne_top_iff [IsFiniteKernel κ] [IsFiniteKernel η] : /--Equivalence between two possible versions of the second condition for the finiteness of the conditional f divergence, the second version is the preferred one.-/ lemma integrable_fDiv_iff [CountableOrCountablyGenerated α β] [IsFiniteMeasure μ] [IsFiniteKernel κ] - [IsFiniteKernel η] (h_int : ∀ᵐ a ∂μ, Integrable (fun x ↦ f ((∂κ a/∂η a) x).toReal) (η a)) + [IsFiniteKernel η] (h_cvx : ConvexOn ℝ (Ici 0) f) + (h_int : ∀ᵐ a ∂μ, Integrable (fun x ↦ f ((∂κ a/∂η a) x).toReal) (η a)) (h_ac : derivAtTop f = ⊤ → ∀ᵐ a ∂μ, κ a ≪ η a) : Integrable (fun x ↦ (fDiv f (κ x) (η x)).toReal) μ ↔ Integrable (fun a ↦ ∫ b, f ((∂κ a/∂η a) b).toReal ∂η a) μ := by @@ -70,8 +71,8 @@ lemma integrable_fDiv_iff [CountableOrCountablyGenerated α β] [IsFiniteMeasure simp · simp · simp - · simp [h_top, EReal.mul_eq_top, derivAtTop_ne_bot, measure_ne_top] - · simp [EReal.mul_eq_bot, derivAtTop_ne_bot, h_top, measure_ne_top] + · simp [h_top, EReal.mul_eq_top, h_cvx.derivAtTop_ne_bot, measure_ne_top] + · simp [EReal.mul_eq_bot, h_cvx.derivAtTop_ne_bot, h_top, measure_ne_top] rw [integrable_congr this] have h_int : Integrable (fun x ↦ (derivAtTop f).toReal * ((κ x).singularPart (η x) Set.univ).toReal) μ := @@ -92,7 +93,7 @@ variable [CountableOrCountablyGenerated α β] lemma fDiv_compProd_ne_top_iff [IsFiniteMeasure μ] [IsFiniteMeasure ν] [IsFiniteKernel κ] [∀ a, NeZero (κ a)] [IsFiniteKernel η] (hf : StronglyMeasurable f) - (h_cvx : ConvexOn ℝ (Set.Ici 0) f) : + (h_cvx : ConvexOn ℝ (Ici 0) f) : fDiv f (μ ⊗ₘ κ) (ν ⊗ₘ η) ≠ ⊤ ↔ (∀ᵐ a ∂ν, Integrable (fun x ↦ f ((∂μ/∂ν) a * (∂κ a/∂η a) x).toReal) (η a)) ∧ Integrable (fun a ↦ ∫ b, f ((∂μ/∂ν) a * (∂κ a/∂η a) b).toReal ∂(η a)) ν @@ -102,7 +103,7 @@ lemma fDiv_compProd_ne_top_iff [IsFiniteMeasure μ] [IsFiniteMeasure ν] lemma fDiv_compProd_eq_top_iff [IsFiniteMeasure μ] [IsFiniteMeasure ν] [IsFiniteKernel κ] [∀ a, NeZero (κ a)] [IsFiniteKernel η] (hf : StronglyMeasurable f) - (h_cvx : ConvexOn ℝ (Set.Ici 0) f) : + (h_cvx : ConvexOn ℝ (Ici 0) f) : fDiv f (μ ⊗ₘ κ) (ν ⊗ₘ η) = ⊤ ↔ (∀ᵐ a ∂ν, Integrable (fun x ↦ f ((∂μ/∂ν) a * (∂κ a/∂η a) x).toReal) (η a)) → Integrable (fun a ↦ ∫ b, f ((∂μ/∂ν) a * (∂κ a/∂η a) b).toReal ∂η a) ν → @@ -113,7 +114,7 @@ lemma fDiv_compProd_eq_top_iff [IsFiniteMeasure μ] [IsFiniteMeasure ν] lemma fDiv_compProd_right_ne_top_iff [IsFiniteMeasure μ] [IsFiniteKernel κ] [∀ a, NeZero (κ a)] [IsFiniteKernel η] (hf : StronglyMeasurable f) - (h_cvx : ConvexOn ℝ (Set.Ici 0) f) : + (h_cvx : ConvexOn ℝ (Ici 0) f) : fDiv f (μ ⊗ₘ κ) (μ ⊗ₘ η) ≠ ⊤ ↔ (∀ᵐ a ∂μ, Integrable (fun x ↦ f ((∂κ a/∂η a) x).toReal) (η a)) ∧ Integrable (fun a ↦ ∫ b, f ((∂κ a/∂η a) b).toReal ∂(η a)) μ @@ -140,7 +141,7 @@ lemma fDiv_compProd_right_ne_top_iff [IsFiniteMeasure μ] lemma fDiv_compProd_right_eq_top_iff [IsFiniteMeasure μ] [IsFiniteKernel κ] [∀ a, NeZero (κ a)] [IsFiniteKernel η] (hf : StronglyMeasurable f) - (h_cvx : ConvexOn ℝ (Set.Ici 0) f) : + (h_cvx : ConvexOn ℝ (Ici 0) f) : fDiv f (μ ⊗ₘ κ) (μ ⊗ₘ η) = ⊤ ↔ (∀ᵐ a ∂μ, Integrable (fun x ↦ f ((∂κ a/∂η a) x).toReal) (η a)) → Integrable (fun a ↦ ∫ b, f ((∂κ a/∂η a) b).toReal ∂η a) μ → @@ -150,7 +151,7 @@ lemma fDiv_compProd_right_eq_top_iff [IsFiniteMeasure μ] rfl lemma fDiv_compProd_left_ne_top_iff [IsFiniteMeasure μ] [IsFiniteMeasure ν] - [IsMarkovKernel κ] (hf : StronglyMeasurable f) (h_cvx : ConvexOn ℝ (Set.Ici 0) f) : + [IsMarkovKernel κ] (hf : StronglyMeasurable f) (h_cvx : ConvexOn ℝ (Ici 0) f) : fDiv f (μ ⊗ₘ κ) (ν ⊗ₘ κ) ≠ ⊤ ↔ Integrable (fun a ↦ f ((∂μ/∂ν) a).toReal) ν ∧ (derivAtTop f = ⊤ → μ ≪ ν) := by rw [fDiv_compProd_ne_top_iff hf h_cvx] @@ -175,7 +176,7 @@ lemma fDiv_compProd_left_ne_top_iff [IsFiniteMeasure μ] [IsFiniteMeasure ν] · simpa only [this, integral_const, measure_univ, ENNReal.one_toReal, smul_eq_mul, one_mul] lemma fDiv_compProd_left_eq_top_iff [IsFiniteMeasure μ] [IsFiniteMeasure ν] - [IsMarkovKernel κ] (hf : StronglyMeasurable f) (h_cvx : ConvexOn ℝ (Set.Ici 0) f) : + [IsMarkovKernel κ] (hf : StronglyMeasurable f) (h_cvx : ConvexOn ℝ (Ici 0) f) : fDiv f (μ ⊗ₘ κ) (ν ⊗ₘ κ) = ⊤ ↔ Integrable (fun a ↦ f ((∂μ/∂ν) a).toReal) ν → (derivAtTop f = ⊤ ∧ ¬ μ ≪ ν) := by rw [← not_iff_not, ← ne_eq, fDiv_compProd_left_ne_top_iff hf h_cvx] @@ -185,7 +186,7 @@ lemma fDiv_compProd_left_eq_top_iff [IsFiniteMeasure μ] [IsFiniteMeasure ν] lemma fDiv_compProd_right [CountableOrCountablyGenerated α β] (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (κ : Kernel α β) [IsMarkovKernel κ] (hf : StronglyMeasurable f) - (h_cvx : ConvexOn ℝ (Set.Ici 0) f) : + (h_cvx : ConvexOn ℝ (Ici 0) f) : fDiv f (μ ⊗ₘ κ) (ν ⊗ₘ κ) = fDiv f μ ν := by by_cases h_top : fDiv f (μ ⊗ₘ κ) (ν ⊗ₘ κ) = ⊤ · symm @@ -209,6 +210,7 @@ lemma fDiv_compProd_right [CountableOrCountablyGenerated α β] variable {γ : Type*} [MeasurableSpace γ] lemma fDiv_toReal_eq_ae {ξ : Kernel α β} {κ η : Kernel (α × β) γ} [IsFiniteKernel κ] + (hf_cvx : ConvexOn ℝ (Ici 0) f) (h_ac : derivAtTop f = ⊤ → ∀ᵐ a ∂μ, ∀ᵐ b ∂ξ a, κ (a, b) ≪ η (a, b)) (h_int : ∀ᵐ a ∂μ, ∀ᵐ b ∂ξ a, Integrable (fun x ↦ f ((∂κ (a, b)/∂η (a, b)) x).toReal) (η (a, b))) : @@ -225,7 +227,7 @@ lemma fDiv_toReal_eq_ae {ξ : Kernel α β} {κ η : Kernel (α × β) γ} [IsFi all_goals · by_cases h_deriv : derivAtTop f = ⊤ · simp [Measure.singularPart_eq_zero_of_ac <| hb_ae h_deriv] - · simp only [ne_eq, EReal.mul_eq_top, EReal.mul_eq_bot, derivAtTop_ne_bot, false_and, + · simp only [ne_eq, EReal.mul_eq_top, EReal.mul_eq_bot, hf_cvx.derivAtTop_ne_bot, false_and, EReal.coe_ennreal_ne_bot, and_false, h_deriv, EReal.coe_ennreal_pos, Measure.measure_univ_pos, ne_eq, EReal.coe_ennreal_eq_top_iff, false_or, not_and] exact fun _ ↦ measure_ne_top _ _ @@ -237,7 +239,7 @@ end Conditional lemma f_rnDeriv_ae_le_integral [CountableOrCountablyGenerated α β] (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (κ η : Kernel α β) [IsFiniteKernel κ] [IsMarkovKernel η] - (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0)) + (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) (h_int : Integrable (fun p ↦ f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)) (hκη : ∀ᵐ a ∂μ, κ a ≪ η a) : (fun a ↦ f ((∂μ/∂ν) a * κ a Set.univ).toReal) @@ -271,7 +273,7 @@ lemma integrable_f_rnDeriv_mul_kernel [CountableOrCountablyGenerated α β] (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (κ η : Kernel α β) [IsFiniteKernel κ] [IsMarkovKernel η] (hf : StronglyMeasurable f) - (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0)) + (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) (h_int : Integrable (fun p ↦ f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)) (hκη : ∀ᵐ a ∂μ, κ a ≪ η a) : Integrable (fun a ↦ f ((∂μ/∂ν) a * κ a Set.univ).toReal) ν := by @@ -303,7 +305,7 @@ lemma integrable_f_rnDeriv_mul_withDensity [CountableOrCountablyGenerated α β] (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (κ η : Kernel α β) [IsFiniteKernel κ] [IsMarkovKernel η] (hf : StronglyMeasurable f) - (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0)) + (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) (h_int : Integrable (fun p ↦ f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)) : Integrable (fun a ↦ f ((∂μ/∂ν) a * Kernel.withDensity η (Kernel.rnDeriv κ η) a Set.univ).toReal) ν := by @@ -317,7 +319,7 @@ lemma integral_f_rnDeriv_mul_le_integral [CountableOrCountablyGenerated α β] (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (κ η : Kernel α β) [IsFiniteKernel κ] [IsMarkovKernel η] (hf : StronglyMeasurable f) - (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0)) + (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) (h_int : Integrable (fun p ↦ f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)) (hκη : ∀ᵐ a ∂μ, κ a ≪ η a) : ∫ x, f ((∂μ/∂ν) x * κ x Set.univ).toReal ∂ν @@ -334,7 +336,7 @@ lemma integral_f_rnDeriv_mul_withDensity_le_integral [CountableOrCountablyGenera (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (κ η : Kernel α β) [IsFiniteKernel κ] [IsMarkovKernel η] (hf : StronglyMeasurable f) - (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0)) + (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) (h_int : Integrable (fun p ↦ f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)) : ∫ x, f ((∂μ/∂ν) x * Kernel.withDensity η (Kernel.rnDeriv κ η) x Set.univ).toReal ∂ν ≤ ∫ x, f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) x).toReal ∂(ν ⊗ₘ η) := by @@ -355,7 +357,7 @@ lemma integral_f_rnDeriv_mul_withDensity_le_integral [CountableOrCountablyGenera lemma f_rnDeriv_le_add [CountableOrCountablyGenerated α β] (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (κ η : Kernel α β) [IsMarkovKernel κ] [IsFiniteKernel η] - (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (h_deriv : derivAtTop f = ⊤ → ∀ᵐ a ∂μ, κ a ≪ η a) : + (hf_cvx : ConvexOn ℝ (Ici 0) f) (h_deriv : derivAtTop f = ⊤ → ∀ᵐ a ∂μ, κ a ≪ η a) : ∀ᵐ a ∂ ν, f ((∂μ/∂ν) a).toReal ≤ f ((∂μ/∂ν) a * Kernel.withDensity η (Kernel.rnDeriv κ η) a Set.univ).toReal + (derivAtTop f).toReal * ((∂μ/∂ν) a).toReal @@ -401,7 +403,7 @@ lemma integrable_f_rnDeriv_of_integrable_compProd' [CountableOrCountablyGenerate (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (κ η : Kernel α β) [IsMarkovKernel κ] [IsMarkovKernel η] (hf : StronglyMeasurable f) - (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0)) + (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) (hf_int : Integrable (fun p ↦ f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)) (h_deriv : derivAtTop f = ⊤ → ∀ᵐ a ∂μ, κ a ≪ η a) : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν := by @@ -428,7 +430,7 @@ lemma fDiv_ne_top_of_fDiv_compProd_ne_top [CountableOrCountablyGenerated α β] (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (κ η : Kernel α β) [IsMarkovKernel κ] [IsMarkovKernel η] (hf : StronglyMeasurable f) - (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0)) + (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) (h_ne_top : fDiv f (μ ⊗ₘ κ) (ν ⊗ₘ η) ≠ ⊤) : fDiv f μ ν ≠ ⊤ := by rw [fDiv_ne_top_iff] @@ -443,7 +445,7 @@ lemma integral_f_rnDeriv_le_integral_add [CountableOrCountablyGenerated α β] (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (κ η : Kernel α β) [IsMarkovKernel κ] [IsMarkovKernel η] (hf : StronglyMeasurable f) - (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0)) + (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) (h_int : Integrable (fun p ↦ f ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal) (ν ⊗ₘ η)) (h_deriv : derivAtTop f = ⊤ → ∀ᵐ a ∂μ, κ a ≪ η a) : ∫ x, f ((∂μ/∂ν) x).toReal ∂ν @@ -481,8 +483,8 @@ lemma integral_f_rnDeriv_le_integral_add [CountableOrCountablyGenerated α β] lemma le_fDiv_compProd [CountableOrCountablyGenerated α β] (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (κ η : Kernel α β) [IsMarkovKernel κ] [IsMarkovKernel η] - (hf : StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) - (hf_cont : ContinuousOn f (Set.Ici 0)) : + (hf : StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Ici 0) f) + (hf_cont : ContinuousOn f (Ici 0)) : fDiv f μ ν ≤ fDiv f (μ ⊗ₘ κ) (ν ⊗ₘ η) := by by_cases h_top : fDiv f (μ ⊗ₘ κ) (ν ⊗ₘ η) = ⊤ · simp [h_top] @@ -516,7 +518,7 @@ lemma le_fDiv_compProd [CountableOrCountablyGenerated α β] (μ ν : Measure α · simp · rw [Kernel.Measure.absolutelyContinuous_compProd_iff] exact h3 h_top - lift (derivAtTop f) to ℝ using ⟨h_top, derivAtTop_ne_bot⟩ with df + lift (derivAtTop f) to ℝ using ⟨h_top, hf_cvx.derivAtTop_ne_bot⟩ with df simp only [EReal.toReal_coe] rw [← EReal.coe_ennreal_toReal (measure_ne_top _ _), ← EReal.coe_ennreal_toReal (measure_ne_top _ _)] @@ -546,7 +548,7 @@ lemma le_fDiv_compProd [CountableOrCountablyGenerated α β] (μ ν : Measure α lemma fDiv_fst_le [Nonempty β] [StandardBorelSpace β] (μ ν : Measure (α × β)) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hf : StronglyMeasurable f) - (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0)) : + (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) : fDiv f μ.fst ν.fst ≤ fDiv f μ ν := by rw [← μ.compProd_fst_condKernel, ← ν.compProd_fst_condKernel, Measure.fst_compProd, Measure.fst_compProd] @@ -555,7 +557,7 @@ lemma fDiv_fst_le [Nonempty β] [StandardBorelSpace β] lemma fDiv_snd_le [Nonempty α] [StandardBorelSpace α] (μ ν : Measure (α × β)) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hf : StronglyMeasurable f) - (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0)) : + (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) : fDiv f μ.snd ν.snd ≤ fDiv f μ ν := by rw [← μ.fst_map_swap, ← ν.fst_map_swap] refine (fDiv_fst_le _ _ hf hf_cvx hf_cont).trans_eq ?_ @@ -565,7 +567,7 @@ lemma fDiv_comp_le_compProd [Nonempty α] [StandardBorelSpace α] (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] (hf : StronglyMeasurable f) - (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0)) : + (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) : fDiv f (κ ∘ₘ μ) (η ∘ₘ ν) ≤ fDiv f (μ ⊗ₘ κ) (ν ⊗ₘ η) := by simp_rw [Measure.comp_eq_snd_compProd] exact fDiv_snd_le _ _ hf hf_cvx hf_cont @@ -575,7 +577,7 @@ lemma fDiv_comp_right_le [Nonempty α] [StandardBorelSpace α] [CountableOrCount (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] (κ : Kernel α β) [IsMarkovKernel κ] (hf : StronglyMeasurable f) - (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0)) : + (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) : fDiv f (κ ∘ₘ μ) (κ ∘ₘ ν) ≤ fDiv f μ ν := by calc fDiv f (κ ∘ₘ μ) (κ ∘ₘ ν) ≤ fDiv f (μ ⊗ₘ κ) (ν ⊗ₘ κ) := fDiv_comp_le_compProd μ ν κ κ hf hf_cvx hf_cont diff --git a/TestingLowerBounds/FDiv/CondFDiv.lean b/TestingLowerBounds/FDiv/CondFDiv.lean index 2fab7f09..b21029f3 100644 --- a/TestingLowerBounds/FDiv/CondFDiv.lean +++ b/TestingLowerBounds/FDiv/CondFDiv.lean @@ -24,7 +24,7 @@ import Mathlib.MeasureTheory.Order.Group.Lattice -/ -open Real MeasureTheory Filter MeasurableSpace +open Real MeasureTheory Filter MeasurableSpace Set open scoped ENNReal NNReal @@ -74,13 +74,13 @@ lemma condFDiv_of_not_integrable @[simp] lemma condFDiv_of_not_integrable' [CountableOrCountablyGenerated α β] [IsFiniteMeasure μ] - [IsFiniteKernel κ] [IsFiniteKernel η] + [IsFiniteKernel κ] [IsFiniteKernel η] (h_cvx : ConvexOn ℝ (Ici 0) f) (hf : ¬ Integrable (fun a ↦ ∫ b, f ((∂κ a/∂η a) b).toReal ∂η a) μ) : condFDiv f κ η μ = ⊤ := by by_cases h_top : ∀ᵐ a ∂μ, fDiv f (κ a) (η a) ≠ ⊤ swap; exact condFDiv_of_not_ae_finite h_top apply condFDiv_of_not_integrable - rwa [integrable_fDiv_iff (fDiv_ae_ne_top_iff.mp h_top).1 (fDiv_ae_ne_top_iff.mp h_top).2] + rwa [integrable_fDiv_iff h_cvx (fDiv_ae_ne_top_iff.mp h_top).1 (fDiv_ae_ne_top_iff.mp h_top).2] /- Use condFDiv_eq instead: its assumptions are in normal form. -/ lemma condFDiv_eq' (hf_ae : ∀ᵐ a ∂μ, fDiv f (κ a) (η a) ≠ ⊤) @@ -90,7 +90,8 @@ lemma condFDiv_eq' (hf_ae : ∀ᵐ a ∂μ, fDiv f (κ a) (η a) ≠ ⊤) variable [CountableOrCountablyGenerated α β] -lemma condFDiv_ne_top_iff [IsFiniteMeasure μ] [IsFiniteKernel κ] [IsFiniteKernel η] : +lemma condFDiv_ne_top_iff [IsFiniteMeasure μ] [IsFiniteKernel κ] [IsFiniteKernel η] + (h_cvx : ConvexOn ℝ (Ici 0) f) : condFDiv f κ η μ ≠ ⊤ ↔ (∀ᵐ a ∂μ, Integrable (fun x ↦ f ((∂κ a/∂η a) x).toReal) (η a)) ∧ Integrable (fun a ↦ ∫ b, f ((∂κ a/∂η a) b).toReal ∂(η a)) μ @@ -104,7 +105,7 @@ lemma condFDiv_ne_top_iff [IsFiniteMeasure μ] [IsFiniteKernel κ] [IsFiniteKern · filter_upwards [h.1] with a ha exact ha.1 · have h_int := h.2 - rwa [integrable_fDiv_iff (fDiv_ae_ne_top_iff.mp h'.1).1 (fDiv_ae_ne_top_iff.mp h'.1).2] + rwa [integrable_fDiv_iff h_cvx (fDiv_ae_ne_top_iff.mp h'.1).1 (fDiv_ae_ne_top_iff.mp h'.1).2] at h_int · intro h_top filter_upwards [h.1] with a ha @@ -119,47 +120,51 @@ lemma condFDiv_ne_top_iff [IsFiniteMeasure μ] [IsFiniteKernel κ] [IsFiniteKern rw [eventually_and] at h simp only [hf_int, eventually_all, true_and] at h specialize h h_contra - rw [integrable_fDiv_iff hf_int h_contra] at h + rw [integrable_fDiv_iff h_cvx hf_int h_contra] at h exact h h_int -lemma condFDiv_eq_top_iff [IsFiniteMeasure μ] [IsFiniteKernel κ] [IsFiniteKernel η] : +lemma condFDiv_eq_top_iff [IsFiniteMeasure μ] [IsFiniteKernel κ] [IsFiniteKernel η] + (h_cvx : ConvexOn ℝ (Ici 0) f) : condFDiv f κ η μ = ⊤ ↔ ¬ (∀ᵐ a ∂μ, Integrable (fun x ↦ f ((∂κ a/∂η a) x).toReal) (η a)) ∨ ¬ Integrable (fun a ↦ ∫ b, f ((∂κ a/∂η a) b).toReal ∂(η a)) μ ∨ (derivAtTop f = ⊤ ∧ ¬ ∀ᵐ a ∂μ, κ a ≪ η a) := by - have h := condFDiv_ne_top_iff (κ := κ) (η := η) (μ := μ) (f := f) + have h := condFDiv_ne_top_iff (κ := κ) (η := η) (μ := μ) (f := f) h_cvx tauto lemma condFDiv_eq [IsFiniteMeasure μ] [IsFiniteKernel κ] [IsFiniteKernel η] + (h_cvx : ConvexOn ℝ (Ici 0) f) (hf_ae : ∀ᵐ a ∂μ, Integrable (fun x ↦ f ((∂κ a/∂η a) x).toReal) (η a)) (hf : Integrable (fun a ↦ ∫ b, f ((∂κ a/∂η a) b).toReal ∂η a) μ) (h_deriv : derivAtTop f = ⊤ → ∀ᵐ a ∂μ, κ a ≪ η a) : condFDiv f κ η μ = ((μ[fun x ↦ (fDiv f (κ x) (η x)).toReal] : ℝ) : EReal) := condFDiv_eq' (fDiv_ae_ne_top_iff.mpr ⟨hf_ae, h_deriv⟩) - ((integrable_fDiv_iff hf_ae h_deriv).mpr hf) + ((integrable_fDiv_iff h_cvx hf_ae h_deriv).mpr hf) -lemma condFDiv_ne_top_iff' [IsFiniteMeasure μ] [IsFiniteKernel κ] [IsFiniteKernel η] : +lemma condFDiv_ne_top_iff' [IsFiniteMeasure μ] [IsFiniteKernel κ] [IsFiniteKernel η] + (h_cvx : ConvexOn ℝ (Ici 0) f) : condFDiv f κ η μ ≠ ⊤ ↔ condFDiv f κ η μ = ((μ[fun x ↦ (fDiv f (κ x) (η x)).toReal] : ℝ) : EReal) := by constructor - · rw [condFDiv_ne_top_iff] - exact fun ⟨h1, h2, h3⟩ => condFDiv_eq h1 h2 h3 + · rw [condFDiv_ne_top_iff h_cvx] + exact fun ⟨h1, h2, h3⟩ => condFDiv_eq h_cvx h1 h2 h3 · simp_all only [ne_eq, EReal.coe_ne_top, not_false_eq_true, implies_true] lemma condFDiv_eq_add [IsFiniteMeasure μ] [IsFiniteKernel κ] [IsFiniteKernel η] + (h_cvx : ConvexOn ℝ (Ici 0) f) (hf_ae : ∀ᵐ a ∂μ, Integrable (fun x ↦ f ((∂κ a/∂η a) x).toReal) (η a)) (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 - rw [condFDiv_eq hf_ae hf h_deriv] + 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 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 - exact toReal_fDiv_of_integrable hx hx_deriv + exact toReal_fDiv_of_integrable h_cvx hx hx_deriv rw [integral_congr_ae this, integral_add] rotate_left · exact hf @@ -173,11 +178,12 @@ lemma condFDiv_eq_add [IsFiniteMeasure μ] [IsFiniteKernel κ] [IsFiniteKernel lemma condFDiv_of_derivAtTop_eq_top [IsFiniteMeasure μ] [IsFiniteKernel κ] [IsFiniteKernel η] + (h_cvx : ConvexOn ℝ (Ici 0) f) (hf_ae : ∀ᵐ a ∂μ, Integrable (fun x ↦ f ((∂κ a/∂η a) x).toReal) (η a)) (hf : Integrable (fun a ↦ ∫ b, f ((∂κ a/∂η a) b).toReal ∂η a) μ) (h_top : derivAtTop f = ⊤) (h_ac : ∀ᵐ a ∂μ, κ a ≪ η a) : condFDiv f κ η μ = (μ[fun a ↦ ∫ y, f ((∂κ a/∂η a) y).toReal ∂η a] : ℝ) := by - rw [condFDiv_eq_add hf_ae hf] + rw [condFDiv_eq_add h_cvx hf_ae hf] · simp [h_top] · exact fun _ ↦ h_ac @@ -239,7 +245,7 @@ lemma condFDiv_ne_bot (κ η : Kernel α β) (μ : Measure α) : condFDiv f κ · norm_num lemma condFDiv_nonneg [IsMarkovKernel κ] [IsMarkovKernel η] - (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0)) + (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) (hf_one : f 1 = 0) : 0 ≤ condFDiv f κ η μ := by by_cases h_ae : ∀ᵐ a ∂μ, fDiv f (κ a) (η a) ≠ ⊤ swap; · rw[condFDiv_of_not_ae_finite h_ae]; exact le_top @@ -276,9 +282,10 @@ lemma condFDiv_const' {ξ : Measure β} [IsFiniteMeasure ξ] (h_ne_bot : fDiv f · exact EReal.coe_ennreal_toReal (measure_ne_top _ _) @[simp] -lemma condFDiv_const {ξ : Measure β} [IsFiniteMeasure ξ] [IsFiniteMeasure μ] : +lemma condFDiv_const {ξ : Measure β} [IsFiniteMeasure ξ] [IsFiniteMeasure μ] + (h_cvx : ConvexOn ℝ (Ici 0) f) : condFDiv f (Kernel.const β μ) (Kernel.const β ν) ξ = (fDiv f μ ν) * ξ Set.univ := - condFDiv_const' fDiv_ne_bot + condFDiv_const' (fDiv_ne_bot h_cvx) section CompProd @@ -289,30 +296,30 @@ variable [CountableOrCountablyGenerated α β] lemma condFDiv_ne_top_iff_fDiv_compProd_ne_top [IsFiniteMeasure μ] [IsFiniteKernel κ] [∀ a, NeZero (κ a)] [IsFiniteKernel η] (hf : StronglyMeasurable f) - (h_cvx : ConvexOn ℝ (Set.Ici 0) f) : + (h_cvx : ConvexOn ℝ (Ici 0) f) : condFDiv f κ η μ ≠ ⊤ ↔ fDiv f (μ ⊗ₘ κ) (μ ⊗ₘ η) ≠ ⊤ := by - rw [condFDiv_ne_top_iff, fDiv_compProd_right_ne_top_iff hf h_cvx] + rw [condFDiv_ne_top_iff h_cvx, fDiv_compProd_right_ne_top_iff hf h_cvx] lemma condFDiv_eq_top_iff_fDiv_compProd_eq_top [IsFiniteMeasure μ] [IsFiniteKernel κ] [∀ a, NeZero (κ a)] [IsFiniteKernel η] (hf : StronglyMeasurable f) - (h_cvx : ConvexOn ℝ (Set.Ici 0) f) : + (h_cvx : ConvexOn ℝ (Ici 0) f) : condFDiv f κ η μ = ⊤ ↔ fDiv f (μ ⊗ₘ κ) (μ ⊗ₘ η) = ⊤ := by rw [← not_iff_not] exact condFDiv_ne_top_iff_fDiv_compProd_ne_top hf h_cvx lemma fDiv_compProd_left (μ : Measure α) [IsFiniteMeasure μ] (κ η : Kernel α β) [IsFiniteKernel κ] [∀ a, NeZero (κ a)] [IsFiniteKernel η] - (hf : StronglyMeasurable f) (h_cvx : ConvexOn ℝ (Set.Ici 0) f) : + (hf : StronglyMeasurable f) (h_cvx : ConvexOn ℝ (Ici 0) f) : fDiv f (μ ⊗ₘ κ) (μ ⊗ₘ η) = condFDiv f κ η μ := by by_cases hf_top : condFDiv f κ η μ = ⊤ · rwa [hf_top, ← condFDiv_eq_top_iff_fDiv_compProd_eq_top hf h_cvx] have hf_top' := hf_top - rw [← ne_eq, condFDiv_ne_top_iff] at hf_top' + rw [← ne_eq, condFDiv_ne_top_iff h_cvx] at hf_top' rcases hf_top' with ⟨h1, h2, h3⟩ have h_int : Integrable (fun x ↦ f ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) x).toReal) (μ ⊗ₘ η) := by rw [integrable_f_rnDeriv_compProd_right_iff hf h_cvx] exact ⟨h1, h2⟩ - rw [fDiv_of_integrable h_int, condFDiv_eq_add h1 h2 h3, Measure.integral_compProd h_int, + rw [fDiv_of_integrable h_int, condFDiv_eq_add h_cvx h1 h2 h3, Measure.integral_compProd h_int, integral_congr_ae (integral_f_compProd_right_congr _ _ _)] by_cases h_deriv : derivAtTop f = ⊤ · simp only [h_deriv, EReal.toReal_top, EReal.coe_zero, zero_mul] @@ -321,7 +328,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 derivAtTop_ne_bot, integral_singularPart _ _ _ MeasurableSet.univ, + rw [EReal.coe_toReal h_deriv h_cvx.derivAtTop_ne_bot, integral_singularPart _ _ _ MeasurableSet.univ, EReal.coe_ennreal_toReal, Set.univ_prod_univ] exact measure_ne_top _ _ @@ -329,6 +336,7 @@ variable {γ : Type*} [MeasurableSpace γ] lemma condFDiv_snd'_toReal_eq_ae [CountableOrCountablyGenerated β γ] {ξ : Kernel α β} [IsFiniteKernel ξ] {κ η : Kernel (α × β) γ} [IsFiniteKernel κ] [IsFiniteKernel η] + (h_cvx : ConvexOn ℝ (Ici 0) f) (h_ac : derivAtTop f = ⊤ → ∀ᵐ a ∂μ, ∀ᵐ b ∂ξ a, κ (a, b) ≪ η (a, b)) (h_int : ∀ᵐ a ∂μ, ∀ᵐ b ∂ξ a, Integrable (fun x ↦ f ((∂κ (a, b)/∂η (a, b)) x).toReal) (η (a, b))) (h_int2 : ∀ᵐ a ∂μ, Integrable @@ -338,7 +346,7 @@ lemma condFDiv_snd'_toReal_eq_ae [CountableOrCountablyGenerated β γ] {ξ : Ker simp_rw [← Kernel.snd'_apply] at h_int2 h_int h_ac ⊢ rw [← eventually_all] at h_ac filter_upwards [h_ac, h_int, h_int2] with a ha_ac ha_int ha_int2 - rw [condFDiv_eq ha_int ha_int2 ha_ac, EReal.toReal_coe] + rw [condFDiv_eq h_cvx ha_int ha_int2 ha_ac, EReal.toReal_coe] lemma condFDiv_kernel_snd'_integrable_iff [CountableOrCountablyGenerated (α × β) γ] [IsFiniteMeasure μ] {ξ : Kernel α β} [IsFiniteKernel ξ] @@ -346,8 +354,8 @@ lemma condFDiv_kernel_snd'_integrable_iff [CountableOrCountablyGenerated (α × (h_ac : derivAtTop f = ⊤ → ∀ᵐ a ∂μ, ∀ᵐ b ∂ξ a, κ (a, b) ≪ η (a, b)) (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)) - (hf_meas : StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) - (hf_cont : ContinuousOn f (Set.Ici 0)) (hf_one : f 1 = 0) : + (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 ↦ ∫ b, |∫ x, f ((∂κ (a, b)/∂η (a, b)) x).toReal ∂η (a, b)| ∂ξ a) μ := by by_cases h_empty : Nonempty α @@ -357,7 +365,7 @@ lemma condFDiv_kernel_snd'_integrable_iff [CountableOrCountablyGenerated (α × - (fDiv f (κ (a, b)) (η (a, b))).toReal ≤ |(derivAtTop f).toReal| ∧ (fDiv f (κ (a, b)) (η (a, b))).toReal - |∫ x, f ((∂κ (a, b)/∂η (a, b)) x).toReal ∂η (a, b)| ≤ |(derivAtTop f).toReal| := by - filter_upwards [fDiv_toReal_eq_ae h_ac h_int] with a ha_ereal_add + filter_upwards [fDiv_toReal_eq_ae hf_cvx h_ac h_int] with a ha_ereal_add filter_upwards [ha_ereal_add] with b hb_ereal_add apply abs_sub_le_iff.mp calc @@ -378,8 +386,8 @@ lemma condFDiv_kernel_snd'_integrable_iff [CountableOrCountablyGenerated (α × 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 simp_rw [← Kernel.snd'_apply] at ha_int2 ha_int ha_ae ⊢ - exact (integrable_fDiv_iff ha_int ha_ae).mpr ha_int2 - rw [integrable_congr <| condFDiv_snd'_toReal_eq_ae h_ac h_int h_int2] + exact (integrable_fDiv_iff hf_cvx ha_int ha_ae).mpr ha_int2 + rw [integrable_congr <| condFDiv_snd'_toReal_eq_ae hf_cvx h_ac h_int h_int2] refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩ · -- using `h_le` we reduce the problem to the integrability of a sum of an integral and -- `f'(∞) * (ξ x) (univ)` @@ -428,8 +436,8 @@ lemma condFDiv_kernel_fst'_integrable_iff [CountableOrCountablyGenerated (α × (h_ac : derivAtTop f = ⊤ → ∀ᵐ b ∂μ, ∀ᵐ a ∂ξ b, κ (a, b) ≪ η (a, b)) (h_int : ∀ᵐ b ∂μ, ∀ᵐ a ∂ξ b, Integrable (fun x ↦ f ((∂κ (a, b)/∂η (a, b)) x).toReal) (η (a, b))) (h_int2 : ∀ᵐ b ∂μ, Integrable (fun a ↦ ∫ x, f ((∂κ (a, b)/∂η (a, b)) x).toReal ∂η (a, b)) (ξ b)) - (hf_meas : StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) - (hf_cont : ContinuousOn f (Set.Ici 0)) (hf_one : f 1 = 0) : + (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 ↦ ∫ a, |∫ x, f ((∂κ (a, b)/∂η (a, b)) x).toReal ∂η (a, b)| ∂ξ b) μ := by simp_rw [← Kernel.snd'_swapRight] @@ -438,8 +446,8 @@ lemma condFDiv_kernel_fst'_integrable_iff [CountableOrCountablyGenerated (α × lemma condFDiv_compProd_meas_eq_top [CountableOrCountablyGenerated (α × β) γ] [IsFiniteMeasure μ] {ξ : Kernel α β} [IsFiniteKernel ξ] {κ η : Kernel (α × β) γ} [IsMarkovKernel κ] [IsMarkovKernel η] - (hf_meas : StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) - (hf_cont : ContinuousOn f (Set.Ici 0)) (hf_one : f 1 = 0) : + (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 @@ -448,20 +456,21 @@ lemma condFDiv_compProd_meas_eq_top [CountableOrCountablyGenerated (α × β) γ EReal.zero_ne_top, IsEmpty.forall_iff, eventually_of_forall, not_true_eq_false, Integrable.of_isEmpty, or_self] have := countableOrCountablyGenerated_right_of_prod_left_of_nonempty (α := α) (β := β) (γ := γ) - rw [condFDiv_eq_top_iff] + rw [condFDiv_eq_top_iff hf_cvx] constructor · by_cases h_ac : derivAtTop f = ⊤ → ∀ᵐ x ∂(μ ⊗ₘ ξ), κ x ≪ η x swap · rw [Measure.ae_compProd_iff (Kernel.measurableSet_absolutelyContinuous _ _)] at h_ac - simp_rw [condFDiv_ne_top_iff, Kernel.snd'_apply, eventually_and, not_and_or, eventually_all] + 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 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, Kernel.snd'_apply, eventually_and, - h_int, eventually_all, false_and, not_false_eq_true, true_or, implies_true] + swap; · simp only [not_eventually, ne_eq, condFDiv_ne_top_iff hf_cvx, Kernel.snd'_apply, + eventually_and, h_int, eventually_all, false_and, not_false_eq_true, true_or, implies_true] have h_int' := h_int rw [← Measure.ae_compProd_iff (measurableSet_integrable_f_rnDeriv κ η hf_meas)] at h_int' rw [← _root_.not_imp] @@ -479,7 +488,7 @@ lemma condFDiv_compProd_meas_eq_top [CountableOrCountablyGenerated (α × β) γ h_ac h_int h_int2 hf_meas hf_cvx hf_cont hf_one).mp.mt h · left contrapose! h_int2 - simp_rw [not_frequently, condFDiv_ne_top_iff] at h_int2 + simp_rw [not_frequently, condFDiv_ne_top_iff hf_cvx] at h_int2 filter_upwards [h_int2] with a ha_int2 simp_rw [← Kernel.snd'_apply, ha_int2.2.1] · intro h @@ -492,15 +501,15 @@ lemma condFDiv_compProd_meas_eq_top [CountableOrCountablyGenerated (α × β) γ refine ⟨?_, condFDiv_kernel_snd'_integrable_iff h_ac h_int1 h_int2.1 hf_meas hf_cvx hf_cont hf_one |>.mpr h_int2.2⟩ filter_upwards [eventually_all.mpr h_ac, h_int1, h_int2.1] with a ha_ae ha_int ha_int2 - apply condFDiv_ne_top_iff.mpr + apply (condFDiv_ne_top_iff hf_cvx).mpr exact ⟨ha_int, ⟨ha_int2, ha_ae⟩⟩ -- -- TODO: find a better name lemma condFDiv_compProd_meas [CountableOrCountablyGenerated (α × β) γ] [IsFiniteMeasure μ] {ξ : Kernel α β} [IsFiniteKernel ξ] {κ η : Kernel (α × β) γ} [IsMarkovKernel κ] [IsMarkovKernel η] - (hf_meas : StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) - (hf_cont : ContinuousOn f (Set.Ici 0)) (hf_one : f 1 = 0) + (hf_meas : StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Ici 0) f) + (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 @@ -508,15 +517,15 @@ lemma condFDiv_compProd_meas [CountableOrCountablyGenerated (α × β) γ] [IsFi swap; simp only [isEmpty_prod, not_nonempty_iff.mp h_empty, true_or, condFDiv_of_isEmpty_left, integral_of_isEmpty, EReal.coe_zero] have := countableOrCountablyGenerated_right_of_prod_left_of_nonempty (α := α) (β := β) (γ := γ) - have h := (condFDiv_ne_top_iff.mp h_top) - rw [condFDiv_ne_top_iff'.mp h_top, - Measure.integral_compProd <| (integrable_fDiv_iff h.1 h.2.2).mpr h.2.1] + have h := ((condFDiv_ne_top_iff hf_cvx).mp h_top) + rw [(condFDiv_ne_top_iff' hf_cvx).mp h_top, + Measure.integral_compProd <| (integrable_fDiv_iff hf_cvx h.1 h.2.2).mpr h.2.1] replace h_top := (condFDiv_compProd_meas_eq_top hf_meas hf_cvx hf_cont hf_one).mpr.mt h_top push_neg at h_top norm_cast apply integral_congr_ae filter_upwards [h_top.1] with a ha - simp_rw [condFDiv_ne_top_iff'.mp ha, EReal.toReal_coe, Kernel.snd'_apply] + simp_rw [(condFDiv_ne_top_iff' hf_cvx).mp ha, EReal.toReal_coe, Kernel.snd'_apply] end CompProd @@ -526,7 +535,7 @@ lemma fDiv_comp_left_le [Nonempty α] [StandardBorelSpace α] [CountableOrCounta (μ : Measure α) [IsFiniteMeasure μ] (κ η : Kernel α β) [IsFiniteKernel κ] [∀ a, NeZero (κ a)] [IsFiniteKernel η] (hf : StronglyMeasurable f) - (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0)) : + (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) : fDiv f (κ ∘ₘ μ) (η ∘ₘ μ) ≤ condFDiv f κ η μ := by calc fDiv f (κ ∘ₘ μ) (η ∘ₘ μ) ≤ fDiv f (μ ⊗ₘ κ) (μ ⊗ₘ η) := fDiv_comp_le_compProd μ μ κ η hf hf_cvx hf_cont diff --git a/TestingLowerBounds/FDiv/Trim.lean b/TestingLowerBounds/FDiv/Trim.lean index 517c15de..c23612a9 100644 --- a/TestingLowerBounds/FDiv/Trim.lean +++ b/TestingLowerBounds/FDiv/Trim.lean @@ -23,7 +23,7 @@ import TestingLowerBounds.FDiv.Basic -/ -open Real MeasureTheory Filter +open Real MeasureTheory Filter Set open scoped ENNReal NNReal Topology @@ -34,7 +34,7 @@ variable {α β : Type*} {m mα : MeasurableSpace α} {mβ : MeasurableSpace β} lemma f_condexp_rnDeriv_le [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hm : m ≤ mα) (hf : StronglyMeasurable f) - (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0)) + (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) (h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) : (fun x ↦ f ((ν[fun x ↦ ((∂μ/∂ν) x).toReal | m]) x)) ≤ᵐ[ν.trim hm] ν[fun x ↦ f ((∂μ/∂ν) x).toReal | m] := by @@ -42,7 +42,7 @@ lemma f_condexp_rnDeriv_le [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hm : m ≤ lemma f_rnDeriv_trim_le [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hm : m ≤ mα) (hμν : μ ≪ ν) (hf : StronglyMeasurable f) - (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0)) + (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) (h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) : (fun x ↦ f ((∂μ.trim hm/∂ν.trim hm) x).toReal) ≤ᵐ[ν.trim hm] ν[fun x ↦ f ((∂μ/∂ν) x).toReal | m] := by @@ -54,7 +54,7 @@ lemma f_rnDeriv_trim_le [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hm : m ≤ m lemma integrable_f_rnDeriv_trim [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hm : m ≤ mα) (hμν : μ ≪ ν) (hf : StronglyMeasurable f) - (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0)) + (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) (h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) : Integrable (fun x ↦ f ((∂μ.trim hm/∂ν.trim hm) x).toReal) (ν.trim hm) := by obtain ⟨c, c', h⟩ : ∃ c c', ∀ x, 0 ≤ x → c * x + c' ≤ f x := @@ -74,7 +74,7 @@ lemma integrable_f_rnDeriv_trim [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hm : lemma integrable_f_condexp_rnDeriv [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hm : m ≤ mα) (hμν : μ ≪ ν) (hf : StronglyMeasurable f) - (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0)) + (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) (h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) : Integrable (fun x ↦ f ((ν[fun x ↦ ((∂μ/∂ν) x).toReal | m]) x)) ν := by have h := integrable_f_rnDeriv_trim hm hμν hf hf_cvx hf_cont h_int @@ -84,7 +84,7 @@ lemma integrable_f_condexp_rnDeriv [IsFiniteMeasure μ] [IsFiniteMeasure ν] lemma fDiv_trim_of_ac [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hm : m ≤ mα) (hμν : μ ≪ ν) (hf : StronglyMeasurable f) - (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0)) + (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) (h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) : fDiv f (μ.trim hm) (ν.trim hm) = ∫ x, f ((ν[fun x ↦ ((∂μ/∂ν) x).toReal | m]) x) ∂ν := by classical @@ -99,7 +99,7 @@ lemma fDiv_trim_of_ac [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hm : m ≤ mα) lemma fDiv_trim_le_of_ac [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hm : m ≤ mα) (hμν : μ ≪ ν) (hf : StronglyMeasurable f) - (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0)) : + (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) : fDiv f (μ.trim hm) (ν.trim hm) ≤ fDiv f μ ν := by by_cases h_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν swap; · rw [fDiv_of_not_integrable h_int]; exact le_top @@ -115,7 +115,7 @@ lemma fDiv_trim_le_of_ac [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hm : m ≤ m lemma fDiv_trim_le [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hm : m ≤ mα) (hf : StronglyMeasurable f) - (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousOn f (Set.Ici 0)) : + (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) : fDiv f (μ.trim hm) (ν.trim hm) ≤ fDiv f μ ν := by have h1 : μ.trim hm = (ν.withDensity (∂μ/∂ν)).trim hm + (μ.singularPart ν).trim hm := by conv_lhs => rw [μ.haveLebesgueDecomposition_add ν, add_comm, trim_add] diff --git a/TestingLowerBounds/ForMathlib/LeftRightDeriv.lean b/TestingLowerBounds/ForMathlib/LeftRightDeriv.lean index 5578897f..733bd261 100644 --- a/TestingLowerBounds/ForMathlib/LeftRightDeriv.lean +++ b/TestingLowerBounds/ForMathlib/LeftRightDeriv.lean @@ -13,7 +13,7 @@ open Set Filter Topology open scoped ENNReal NNReal -variable {f : ℝ → ℝ} +variable {f : ℝ → ℝ} {x : ℝ} /-- The right derivative of a real function. -/ noncomputable @@ -70,6 +70,33 @@ lemma leftDeriv_eq_rightDeriv (f : ℝ → ℝ) : ext x simp [leftDeriv_eq_rightDeriv_apply] +lemma Filter.EventuallyEq.derivWithin_eq_nhds {𝕜 F : Type*} [NontriviallyNormedField 𝕜] + [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f₁ f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} + (h : f₁ =ᶠ[𝓝 x] f) : + derivWithin f₁ s x = derivWithin f s x := by + simp_rw [derivWithin] + rw [Filter.EventuallyEq.fderivWithin_eq_nhds h] + +lemma Filter.EventuallyEq.rightDeriv_eq_nhds {x : ℝ} {g : ℝ → ℝ} (h : f =ᶠ[𝓝 x] g) : + rightDeriv f x = rightDeriv g x := h.derivWithin_eq_nhds + +lemma rightDeriv_congr_atTop {g : ℝ → ℝ} (h : f =ᶠ[atTop] g) : + rightDeriv f =ᶠ[atTop] rightDeriv g := by + have h' : ∀ᶠ x in atTop, f =ᶠ[𝓝 x] g := by + -- todo: replace by clean filter proof? + simp only [Filter.EventuallyEq, eventually_atTop, ge_iff_le] at h ⊢ + obtain ⟨a, ha⟩ := h + refine ⟨a + 1, fun b hab ↦ ?_⟩ + have h_ge : ∀ᶠ x in 𝓝 b, a ≤ x := eventually_ge_nhds ((lt_add_one _).trans_le hab) + filter_upwards [h_ge] using ha + filter_upwards [h'] with a ha using ha.rightDeriv_eq_nhds + +@[simp] +lemma rightDeriv_zero : rightDeriv 0 = 0 := by + ext x + simp only [rightDeriv, Pi.zero_apply] + exact derivWithin_const x _ 0 (uniqueDiffWithinAt_Ioi x) + @[simp] lemma rightDeriv_const (c : ℝ) : rightDeriv (fun _ ↦ c) = 0 := by ext x @@ -129,6 +156,11 @@ lemma rightDeriv_add_apply {f g : ℝ → ℝ} {x : ℝ} (hf : DifferentiableWit simp_rw [rightDeriv_def, ← derivWithin_add (uniqueDiffWithinAt_Ioi x) hf hg] rfl +lemma rightDeriv_add_apply' {f g : ℝ → ℝ} {x : ℝ} (hf : DifferentiableWithinAt ℝ f (Ioi x) x) + (hg : DifferentiableWithinAt ℝ g (Ioi x) x) : + rightDeriv (fun x ↦ f x + g x) x = rightDeriv f x + rightDeriv g x := + rightDeriv_add_apply hf hg + lemma rightDeriv_add {f g : ℝ → ℝ} (hf : ∀ x, DifferentiableWithinAt ℝ f (Ioi x) x) (hg : ∀ x, DifferentiableWithinAt ℝ g (Ioi x) x) : rightDeriv (f + g) = fun x ↦ rightDeriv f x + rightDeriv g x := by @@ -184,6 +216,12 @@ lemma bddBelow_slope_Ioi (hfc : ConvexOn ℝ univ f) (x : ℝ) : simp_rw [mem_Ici, ← hz'] exact slope_mono hfc trivial (by simp) ⟨trivial, hz.ne'⟩ (by linarith) +lemma bddBelow_slope_Ioi' (hfc : ConvexOn ℝ (Ici 0) f) (x : ℝ) (hx : 0 < x) : + BddBelow (slope f x '' Ioi x) := by + refine bddBelow_iff_subset_Ici.mpr ⟨(slope f x 0), fun y ⟨z, (hz : x < z), hz'⟩ ↦ ?_⟩ + simp_rw [mem_Ici, ← hz'] + exact slope_mono hfc hx.le (by simp [hx.ne]) ⟨(hx.trans hz).le, hz.ne'⟩ (by linarith) + lemma bddAbove_slope_Iio (hfc : ConvexOn ℝ univ f) (x : ℝ) : BddAbove (slope f x '' Iio x) := by refine bddAbove_iff_subset_Iic.mpr ⟨(slope f x (x + 1)), fun y ⟨z, (hz : z < x), hz'⟩ ↦ ?_⟩ @@ -192,7 +230,17 @@ lemma bddAbove_slope_Iio (hfc : ConvexOn ℝ univ f) (x : ℝ) : end Slope --- TODO: this can be generalized to a set S, where the function is convex, but I still need to figure out what hp to require, since the minimal assumption I think is that there exist a right interval of x that is contained in S (so x itself does not have to be in S), i.e. (x, y) ⊆ S, I don't know if. To generalize we will need MonotoneOn.tendsto_nhdsWithin_Ioo_right. However there are dirrerent kinds of sufficient conditions that could be given, for example S open and x in S or x in the interior of S. Discuss this with Remy. Maybe the minimal hp I described is not sufficient, I also need to assure some kind of boundedness of the slope, this should be assured if x is in the interior of S, because then we can take a point to the left of x but still inside S and use the monotonicity of the solpe in S, but can we do better? For now we can leave it like this +-- TODO: this can be generalized to a set S, where the function is convex, +-- but I still need to figure out what hp to require, +-- since the minimal assumption I think is that there exist a right interval of x +-- that is contained in S (so x itself does not have to be in S), i.e. (x, y) ⊆ S, I don't know if. +-- To generalize we will need MonotoneOn.tendsto_nhdsWithin_Ioo_right. +-- However there are dirrerent kinds of sufficient conditions that could be given, +-- for example S open and x in S or x in the interior of S. Discuss this with Remy. +-- Maybe the minimal hp I described is not sufficient, I also need to assure some kind +-- of boundedness of the slope, this should be assured if x is in the interior of S, +-- because then we can take a point to the left of x but still inside S and use the monotonicity +-- of the solpe in S, but can we do better? For now we can leave it like this lemma hasRightDerivAt (hfc : ConvexOn ℝ univ f) (x : ℝ) : HasDerivWithinAt f (sInf (slope f x '' Ioi x)) (Ioi x) x := by simp_rw [hasDerivWithinAt_iff_tendsto_slope] @@ -203,10 +251,24 @@ lemma hasRightDerivAt (hfc : ConvexOn ℝ univ f) (x : ℝ) : exact hfc.secant_mono trivial trivial trivial hy.ne' hz.ne' hz'.le exact MonotoneOn.tendsto_nhdsWithin_Ioi h_mono (bddBelow_slope_Ioi hfc x) +lemma hasRightDerivAt' (hfc : ConvexOn ℝ (Ici 0) f) (hx : 0 < x) : + HasDerivWithinAt f (sInf (slope f x '' Ioi x)) (Ioi x) x := by + simp_rw [hasDerivWithinAt_iff_tendsto_slope] + simp only [mem_Ioi, lt_self_iff_false, not_false_eq_true, diff_singleton_eq_self] + have h_mono : MonotoneOn (slope f x) (Ioi x) := by + refine monotoneOn_iff_forall_lt.mpr fun y (hy : x < y) z (hz : x < z) hz' ↦ ?_ + simp_rw [slope_def_field] + exact hfc.secant_mono hx.le (hx.trans hy).le (hx.trans hz).le hy.ne' hz.ne' hz'.le + exact MonotoneOn.tendsto_nhdsWithin_Ioi h_mono (bddBelow_slope_Ioi' hfc x hx) + lemma differentiableWithinAt_Ioi (hfc : ConvexOn ℝ univ f) (x : ℝ) : DifferentiableWithinAt ℝ f (Ioi x) x := (hfc.hasRightDerivAt x).differentiableWithinAt +lemma differentiableWithinAt_Ioi' (hfc : ConvexOn ℝ (Ici 0) f) (hx : 0 < x) : + DifferentiableWithinAt ℝ f (Ioi x) x := + (hfc.hasRightDerivAt' hx).differentiableWithinAt + lemma hadDerivWithinAt_rightDeriv (hfc : ConvexOn ℝ univ f) (x : ℝ) : HasDerivWithinAt f (rightDeriv f x) (Ioi x) x := (hfc.differentiableWithinAt_Ioi x).hasDerivWithinAt @@ -233,6 +295,10 @@ lemma rightDeriv_eq_sInf_slope (hfc : ConvexOn ℝ univ f) (x : ℝ) : rightDeriv f x = sInf (slope f x '' Ioi x) := (hfc.hasRightDerivAt x).derivWithin (uniqueDiffWithinAt_Ioi x) +lemma rightDeriv_eq_sInf_slope' (hfc : ConvexOn ℝ (Ici 0) f) (hx : 0 < x) : + rightDeriv f x = sInf (slope f x '' Ioi x) := + (hfc.hasRightDerivAt' hx).derivWithin (uniqueDiffWithinAt_Ioi x) + lemma leftDeriv_eq_sSup_slope (hfc : ConvexOn ℝ univ f) (x : ℝ) : leftDeriv f x = sSup (slope f x '' Iio x) := (hfc.hasLeftDerivAt x).derivWithin (uniqueDiffWithinAt_Iio x) @@ -247,6 +313,16 @@ lemma rightDeriv_mono (hfc : ConvexOn ℝ univ f) : Monotone (rightDeriv f) := b rw [slope_comm] exact slope_mono hfc trivial ⟨trivial, hxy.ne⟩ ⟨trivial, yz.ne'⟩ (hxy.trans yz).le +lemma rightDeriv_mono' (hfc : ConvexOn ℝ (Ici 0) f) : MonotoneOn (rightDeriv f) (Ioi 0) := by + intro x (hx : 0 < x) y (hy : 0 < y) hxy + rcases eq_or_lt_of_le hxy with rfl | hxy; · rfl + rw [hfc.rightDeriv_eq_sInf_slope' hx, hfc.rightDeriv_eq_sInf_slope' hy] + refine csInf_le_of_le (b := slope f x y) (bddBelow_slope_Ioi' hfc x hx) + ⟨y, by simp [hxy]⟩ (le_csInf nonempty_of_nonempty_subtype ?_) + rintro _ ⟨z, (yz : y < z), rfl⟩ + rw [slope_comm] + exact slope_mono hfc hy.le ⟨hx.le, hxy.ne⟩ ⟨hy.le.trans yz.le, yz.ne'⟩ (hxy.trans yz).le + lemma leftDeriv_mono (hfc : ConvexOn ℝ univ f) : Monotone (leftDeriv f) := by rw [leftDeriv_eq_rightDeriv] change Monotone (- rightDeriv (f ∘ Neg.neg) ∘ Neg.neg) diff --git a/TestingLowerBounds/StatInfoFun.lean b/TestingLowerBounds/StatInfoFun.lean index 85203f15..542bf082 100644 --- a/TestingLowerBounds/StatInfoFun.lean +++ b/TestingLowerBounds/StatInfoFun.lean @@ -136,63 +136,67 @@ lemma convexOn_statInfoFun (β γ : ℝ) : ConvexOn ℝ univ (fun x ↦ statInfo section derivAtTop -lemma tendsto_statInfoFun_div_at_top_of_pos_of_le (hβ : 0 < β) (hγ : γ ≤ β) : - Tendsto (fun x ↦ statInfoFun β γ x / x) atTop (𝓝 0) := by - refine tendsto_atTop_of_eventually_const (fun x hx ↦ ?_) (i₀ := γ / β) - rw [statInfoFun_of_le hγ, div_eq_zero_iff] - exact Or.inl <| max_eq_left_iff.mpr <| tsub_nonpos.mpr <| (div_le_iff' hβ).mp hx - -lemma tendsto_statInfoFun_div_at_top_of_pos_of_gt (hβ : 0 < β) (hγ : γ > β) : - Tendsto (fun x ↦ statInfoFun β γ x / x) atTop (𝓝 β) := by - have h : (fun x ↦ β + -γ / x) =ᶠ[atTop] fun x ↦ statInfoFun β γ x / x := by - filter_upwards [eventually_ge_atTop (γ / β), eventually_ne_atTop 0] with x hx hx' - rw [statInfoFun_of_pos_of_gt_of_ge hβ hγ hx] - ring_nf - simp_rw [mul_assoc, mul_inv_cancel hx', mul_one] - nth_rw 2 [← add_zero β] - refine Tendsto.congr' h (Tendsto.const_add β ?_) - exact Tendsto.div_atTop tendsto_const_nhds fun _ a ↦ a - -lemma tendsto_statInfoFun_div_at_top_of_neg_of_le (hβ : β < 0) (hγ : γ ≤ β) : - Tendsto (fun x ↦ statInfoFun β γ x / x) atTop (𝓝 (-β)) := by - have h : (fun x ↦ γ / x - β) =ᶠ[atTop] fun x ↦ statInfoFun β γ x / x := by - filter_upwards [eventually_ge_atTop (γ / β), eventually_ne_atTop 0] with x hx hx' - rw [statInfoFun_of_neg_of_le_of_ge hβ hγ hx] - ring_nf - simp_rw [mul_inv_cancel hx', one_mul] - rw [neg_eq_zero_sub β] - refine Tendsto.congr' h (Tendsto.sub_const ?_ β) - exact Tendsto.div_atTop tendsto_const_nhds fun _ a ↦ a - -lemma tendsto_statInfoFun_div_at_top_of_neg_of_gt (hβ : β < 0) (hγ : γ > β) : - Tendsto (fun x ↦ statInfoFun β γ x / x) atTop (𝓝 0) := by - refine tendsto_atTop_of_eventually_const (fun x hx ↦ ?_) (i₀ := γ / β) - rw [statInfoFun_of_gt hγ, div_eq_zero_iff] - refine Or.inl <| max_eq_left_iff.mpr <| tsub_nonpos.mpr <| (div_le_iff_of_neg' hβ).mp hx - lemma derivAtTop_statInfoFun_of_nonneg_of_le (hβ : 0 ≤ β) (hγ : γ ≤ β) : derivAtTop (fun x ↦ statInfoFun β γ x) = 0 := by - rcases eq_or_lt_of_le hβ with (rfl | hβ) - · simp - exact derivAtTop_of_tendsto (tendsto_statInfoFun_div_at_top_of_pos_of_le hβ hγ) + rw [← derivAtTop_zero] + refine derivAtTop_congr ?_ + rw [EventuallyEq, eventually_atTop] + refine ⟨1, fun x hx ↦ ?_⟩ + rw [statInfoFun_of_le hγ] + simp only [Pi.zero_apply, max_eq_left_iff, tsub_le_iff_right, zero_add] + refine hγ.trans ?_ + conv_lhs => rw [← mul_one β] + gcongr lemma derivAtTop_statInfoFun_of_nonneg_of_gt (hβ : 0 ≤ β) (hγ : γ > β) : derivAtTop (fun x ↦ statInfoFun β γ x) = β := by rcases eq_or_lt_of_le hβ with (rfl | hβ) · simp - exact derivAtTop_of_tendsto (tendsto_statInfoFun_div_at_top_of_pos_of_gt hβ hγ) + have : (β : EReal) = derivAtTop (fun x ↦ β * x - γ) := by + rw [derivAtTop_sub_const] + swap; · exact (ConvexOn.const_mul_id _).subset (subset_univ _) (convex_Ici _) + change _ = derivAtTop (fun x ↦ β * x) + rw [derivAtTop_const_mul _ hβ.ne'] + swap; · exact convexOn_id (convex_Ici _) + simp only [derivAtTop_id', mul_one] + rw [this] + refine derivAtTop_congr ?_ + rw [EventuallyEq, eventually_atTop] + refine ⟨γ / β, fun x hx ↦ ?_⟩ + rw [statInfoFun_of_pos_of_gt_of_ge hβ hγ hx] lemma derivAtTop_statInfoFun_of_nonpos_of_le (hβ : β ≤ 0) (hγ : γ ≤ β) : derivAtTop (fun x ↦ statInfoFun β γ x) = -β := by rcases eq_or_lt_of_le hβ with (rfl | hβ) · simp - exact derivAtTop_of_tendsto (tendsto_statInfoFun_div_at_top_of_neg_of_le hβ hγ) + have : -(β : EReal) = derivAtTop (fun x ↦ γ - β * x) := by + simp_rw [sub_eq_add_neg, ← neg_mul] + rw [derivAtTop_const_add] + swap + · change ConvexOn ℝ (Ici _) (fun x ↦ (-β) • x) + refine (convexOn_id (convex_Ici _)).smul ?_ + simp [hβ.le] + rw [derivAtTop_const_mul] + · simp + · exact convexOn_id (convex_Ici _) + · simp only [ne_eq, neg_eq_zero, hβ.ne, not_false_eq_true] + rw [this] + refine derivAtTop_congr ?_ + rw [EventuallyEq, eventually_atTop] + refine ⟨γ / β, fun x hx ↦ ?_⟩ + rw [statInfoFun_of_neg_of_le_of_ge hβ hγ hx] lemma derivAtTop_statInfoFun_of_nonpos_of_gt (hβ : β ≤ 0) (hγ : γ > β) : derivAtTop (fun x ↦ statInfoFun β γ x) = 0 := by rcases eq_or_lt_of_le hβ with (rfl | hβ) · simp - exact derivAtTop_of_tendsto (tendsto_statInfoFun_div_at_top_of_neg_of_gt hβ hγ) + rw [← derivAtTop_zero] + refine derivAtTop_congr ?_ + rw [EventuallyEq, eventually_atTop] + refine ⟨γ / β, fun x hx ↦ ?_⟩ + rw [statInfoFun_of_gt hγ] + simp only [Pi.zero_apply, max_eq_left_iff, tsub_le_iff_right, zero_add] + rwa [ge_iff_le, div_le_iff_of_neg hβ, mul_comm] at hx lemma derivAtTop_statInfoFun_eq : derivAtTop (fun x ↦ statInfoFun β γ x) diff --git a/blueprint/src/sections/convex.tex b/blueprint/src/sections/convex.tex index 7ee7fa83..1ff6f2d2 100644 --- a/blueprint/src/sections/convex.tex +++ b/blueprint/src/sections/convex.tex @@ -4,7 +4,7 @@ \chapter{Convex functions of Radon-Nikodym derivatives} \begin{definition} \label{def:derivAtTop} - \lean{ProbabilityTheory.derivAtTop} + \lean{derivAtTop} \leanok %\uses{} We define $f'(\infty) := \limsup_{x \to + \infty} f(x)/x$. This can be equal to $+\infty$ (but not $-\infty$).