Merge remote-tracking branch 'origin/master' into blueprint

TestingLowerBounds/ForMathlib/RadonNikodym.lean

@@ -122,84 +122,6 @@ lemma rnDeriv_measure_compProd_left' (μ ν : Measure α) (κ : Kernel α γ)
 
 variable [CountableOrCountablyGenerated α γ]
 
--- PR #17682
-/-- For two kernels `κ, η`, the singular part of `κ a` with respect to `η a` is a measurable
-function of `a`. -/
-lemma measurable_singularPart (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η] :
-    Measurable (fun a ↦ (κ a).singularPart (η a)) := by
-  refine Measure.measurable_of_measurable_coe _ (fun s hs ↦ ?_)
-  simp_rw [← κ.singularPart_eq_singularPart_measure, κ.singularPart_def η]
-  exact Kernel.measurable_coe _ hs
-
--- PR #17682
-lemma rnDeriv_self (κ : Kernel α γ) [IsFiniteKernel κ] (a : α) : rnDeriv κ κ a =ᵐ[κ a] 1 :=
-  (κ.rnDeriv_eq_rnDeriv_measure).trans (κ a).rnDeriv_self
-
--- PR #17682
-lemma rnDeriv_singularPart (κ ν : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel ν] (a : α) :
-    rnDeriv (singularPart κ ν) ν a =ᵐ[ν a] 0 := by
-  filter_upwards [(singularPart κ ν).rnDeriv_eq_rnDeriv_measure,
-    (Measure.rnDeriv_eq_zero _ _).mpr (mutuallySingular_singularPart κ ν a)] with x h1 h2
-  rw [h1, h2]
-
--- PR #17682
-lemma rnDeriv_lt_top (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η] {a : α} :
-    ∀ᵐ x ∂(η a), rnDeriv κ η a x < ∞ := by
-  filter_upwards [κ.rnDeriv_eq_rnDeriv_measure, (κ a).rnDeriv_ne_top _]
-    with x heq htop using heq ▸ htop.lt_top
-
--- PR #17682
-lemma rnDeriv_ne_top (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η] {a : α} :
-    ∀ᵐ x ∂(η a), rnDeriv κ η a x ≠ ∞ := by
-  filter_upwards [κ.rnDeriv_lt_top η] with a h using h.ne
-
--- PR #17682
-lemma rnDeriv_pos [IsFiniteKernel κ] [IsFiniteKernel η] {a : α} (ha : κ a ≪ η a) :
-    ∀ᵐ x ∂(κ a), 0 < rnDeriv κ η a x := by
-  filter_upwards [ha.ae_le κ.rnDeriv_eq_rnDeriv_measure, Measure.rnDeriv_pos ha]
-    with x heq hpos using heq ▸ hpos
-
--- PR #17682
-lemma rnDeriv_toReal_pos [IsFiniteKernel κ] [IsFiniteKernel η] {a : α} (h : κ a ≪ η a) :
-    ∀ᵐ x ∂(κ a), 0 < (rnDeriv κ η a x).toReal := by
-  filter_upwards [rnDeriv_pos h, h.ae_le (rnDeriv_ne_top κ _)] with x h0 htop
-  simp_all only [pos_iff_ne_zero, ne_eq, ENNReal.toReal_pos, not_false_eq_true, and_self]
-
--- PR #17682
-lemma rnDeriv_add (κ ν η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel ν] [IsFiniteKernel η]
-    (a : α) :
-    rnDeriv (κ + ν) η a =ᵐ[η a] rnDeriv κ η a + rnDeriv ν η a := by
-  filter_upwards [(κ + ν).rnDeriv_eq_rnDeriv_measure, κ.rnDeriv_eq_rnDeriv_measure,
-    ν.rnDeriv_eq_rnDeriv_measure, (κ 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]
-
--- PR #17682
-lemma withDensity_rnDeriv_le (κ η : Kernel α γ) [IsFiniteKernel κ] [IsFiniteKernel η] (a : α) :
-    η.withDensity (κ.rnDeriv η) a ≤ κ a := by
-  refine Measure.le_intro (fun s hs _ ↦ ?_)
-  rw [Kernel.withDensity_apply']
-  swap; · exact κ.measurable_rnDeriv _
-  rw [setLIntegral_congr_fun hs ((κ.rnDeriv_eq_rnDeriv_measure).mono (fun x hx _ ↦ hx)),
-    ← withDensity_apply _ hs]
-  exact (κ a).withDensity_rnDeriv_le _ _
-
--- PR #17682
-lemma withDensity_rnDeriv_eq [IsFiniteKernel κ] [IsFiniteKernel η] {a : α} (h : κ a ≪ η a) :
-    η.withDensity (κ.rnDeriv η) a = κ a := by
-  rw [Kernel.withDensity_apply]
-  swap; · exact κ.measurable_rnDeriv _
-  have h_ae := κ.rnDeriv_eq_rnDeriv_measure (η := η) (a := a)
-  rw [MeasureTheory.withDensity_congr_ae h_ae, (κ a).withDensity_rnDeriv_eq _ h]
-
--- PR #17682
-lemma rnDeriv_withDensity [IsFiniteKernel κ] {f : α → γ → ℝ≥0∞} [IsFiniteKernel (withDensity κ f)]
-    (hf : Measurable (Function.uncurry f)) (a : α) :
-    (κ.withDensity f).rnDeriv κ a =ᵐ[κ a] f a := by
-  have h_ae := (κ.withDensity f).rnDeriv_eq_rnDeriv_measure (η := κ) (a := a)
-  have hf' : ∀ a, Measurable (f a) := fun _ ↦ hf.of_uncurry_left
-  filter_upwards [h_ae, (κ a).rnDeriv_withDensity (hf' a)] with x hx1 hx2
-  rw [hx1, κ.withDensity_apply hf, hx2]
-
 section MeasureCompProd
 
 lemma setLIntegral_prod_rnDeriv

TestingLowerBounds/MeasureCompProd.lean

@@ -126,10 +126,10 @@ lemma Measure.snd_sum {ι : Type*} (μ : ι → Measure (α × β)) :
   · exact measurable_snd hs
 
 instance {μ : Measure (α × β)} [SFinite μ] : SFinite μ.fst :=
-  ⟨fun n ↦ (sFiniteSeq μ n).fst, inferInstance, by rw [← Measure.fst_sum, sum_sFiniteSeq μ]⟩
+  ⟨fun n ↦ (sfiniteSeq μ n).fst, inferInstance, by rw [← Measure.fst_sum, sum_sfiniteSeq μ]⟩
 
 instance {μ : Measure (α × β)} [SFinite μ] : SFinite μ.snd :=
-  ⟨fun n ↦ (sFiniteSeq μ n).snd, inferInstance, by rw [← Measure.snd_sum, sum_sFiniteSeq μ]⟩
+  ⟨fun n ↦ (sfiniteSeq μ n).snd, inferInstance, by rw [← Measure.snd_sum, sum_sfiniteSeq μ]⟩
 
 instance {μ : Measure α} [SFinite μ] {κ : Kernel α β} [IsSFiniteKernel κ] : SFinite (κ ∘ₘ μ) := by
   rw [Measure.comp_eq_snd_compProd]

blueprint/src/sections/f_divergence.tex

@@ -813,14 +813,14 @@ \subsubsection{Sigma-algebras}
 
 \begin{lemma}[Superseded by Theorem~\ref{thm:fDiv_trim_le}]
   \label{lem:fDiv_trim_le_of_ac}
-  \lean{ProbabilityTheory.fDiv_trim_le_of_ac}
-  \leanok
+  %\lean{}
+  %\leanok
   \uses{def:fDiv}
   Let $\mu, \nu$ be two finite measures on $\mathcal X$ with $\mu \ll \nu$ and let $\mathcal A$ be a sub-$\sigma$-algebra of $\mathcal X$. Then
   $D_f(\mu_{| \mathcal A}, \nu_{| \mathcal A}) \le D_f(\mu, \nu)$.
 \end{lemma}
 
-\begin{proof}\leanok
+\begin{proof}%\leanok
 \uses{thm:condexp_jensen, lem:rnDeriv_trim_of_ac}
 Since $\mu \ll \nu$, $\mu_{| \mathcal A} \ll \nu_{| \mathcal A}$ and
 \begin{align*}

blueprint/src/sections/rn_deriv.tex

@@ -166,7 +166,7 @@ \section{Composition}
 
 \begin{lemma}
   \label{lem:rnDeriv_map_eq_condexp}
-  \lean{ProbabilityTheory.toReal_rnDeriv_map}
+  \lean{ProbabilityTheory.Measure.toReal_rnDeriv_map}
   \leanok
   \uses{}
   Let $\mu, \nu \in \mathcal M(\mathcal X)$ with $\mu \ll \nu$, $g : \mathcal X \to \mathcal Y$ a measurable function and denote by $g^* \mathcal Y$ the comap of the $\sigma$-algebra on $\mathcal Y$ by $g$.

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "daf1ed91789811cf6bbb7bf2f4dad6b3bad8fbf4",
+   "rev": "9efd9c267ad7a71c5e3a83e8fbbd446fe61ef119",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2b2f6d7fbe9d917fc010e9054c1ce11774c9088b",
+   "rev": "fa3d73a2cf077f4b14c7840352ac7b08aeb6eb41",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,10 +35,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c",
+   "rev": "cd20dae87c48495f0220663014dff11671597fcf",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.42",
+   "inputRev": "v0.0.43-pre",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7376ac07aa2b0492372c056b7a2c3163b3026d1e",
+   "rev": "9b4088ccf0f44ddd7b1132bb1348aef8cf481e12",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "282d392e489013a298925f42995f95183301cce4",
+   "rev": "5f0628eab56cdcf7a33982a270433e0fc3a6e9a5",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,