From 82817a33d95d88bf84c9ba33624a6a1ebf9302ce Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Degenne?= Date: Fri, 2 Aug 2024 12:20:30 +0200 Subject: [PATCH 01/17] merge two lemmas --- blueprint/src/sections/f_divergence.tex | 26 ++++++------------------- 1 file changed, 6 insertions(+), 20 deletions(-) diff --git a/blueprint/src/sections/f_divergence.tex b/blueprint/src/sections/f_divergence.tex index bb0ab9b5..6e30cb10 100644 --- a/blueprint/src/sections/f_divergence.tex +++ b/blueprint/src/sections/f_divergence.tex @@ -498,29 +498,15 @@ \subsection{Integral representation of $f$-divergences} \end{proof} \begin{lemma} - \label{lem:convex_taylor_gt} + \label{lem:convex_taylor} \lean{ConvexOn.convex_taylor} \leanok \uses{def:curvatureMeasure} - For $f: \mathbb{R} \to \mathbb{R}$ a convex function and $x,y \in \mathbb{R}$ with $x < y$, + For $f: \mathbb{R} \to \mathbb{R}$ a convex function and $x,y \in \mathbb{R}$, \begin{align*} - f(y) - f(x) - (y - x)f'_+(x) = \int_{z \in (x,y]} (y - z) \partial \gamma_f \: . - \end{align*} -\end{lemma} - -\begin{proof}\leanok -\uses{} - -\end{proof} - -\begin{lemma} - \label{lem:convex_taylor_lt} - \lean{ConvexOn.convex_taylor} - \leanok - \uses{def:curvatureMeasure} - For $f: \mathbb{R} \to \mathbb{R}$ a convex function and $x,y \in \mathbb{R}$ with $y < x$, - \begin{align*} - f(y) - f(x) - (y - x)f'_+(x) = \int_{z \in (y,x]} (z - y) \partial \gamma_f \: . + f(y) - f(x) - (y - x)f'_+(x) &= \int_{z \in (x,y]} (y - z) \partial \gamma_f & \text{ if } x \le y \: , + \\ + f(y) - f(x) - (y - x)f'_+(x) &= \int_{z \in (y,x]} (z - y) \partial \gamma_f & \text{ if } y \le x \: . \end{align*} \end{lemma} @@ -543,7 +529,7 @@ \subsection{Integral representation of $f$-divergences} \end{corollary} \begin{proof}%\leanok -\uses{lem:convex_taylor_lt, lem:convex_taylor_gt} +\uses{lem:convex_taylor} \end{proof} From 833ac9bc3cea232353cc8ceeca3a7506dac7e34b Mon Sep 17 00:00:00 2001 From: Lorenzo Luccioli Date: Fri, 2 Aug 2024 20:53:28 +0200 Subject: [PATCH 02/17] apply changes --- TestingLowerBounds/Divergences/KullbackLeibler.lean | 7 ++++--- TestingLowerBounds/ForMathlib/LeftRightDeriv.lean | 8 ++++++++ 2 files changed, 12 insertions(+), 3 deletions(-) diff --git a/TestingLowerBounds/Divergences/KullbackLeibler.lean b/TestingLowerBounds/Divergences/KullbackLeibler.lean index 544e0f6b..8897c64b 100644 --- a/TestingLowerBounds/Divergences/KullbackLeibler.lean +++ b/TestingLowerBounds/Divergences/KullbackLeibler.lean @@ -61,8 +61,9 @@ 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 rightDeriv_mul_log {x : ℝ} (hx : x ≠ 0) : rightDeriv (fun x ↦ x * log x) x = log x + 1 := + rightDeriv_of_hasDerivAt (Real.hasDerivAt_mul_log hx) + lemma derivAtTop_mul_log : derivAtTop (fun x ↦ x * log x) = ⊤ := by refine derivAtTop_of_tendsto_atTop ?_ @@ -70,7 +71,7 @@ lemma derivAtTop_mul_log : derivAtTop (fun x ↦ x * log x) = ⊤ := by tendsto_log_atTop.atTop_add tendsto_const_nhds refine (tendsto_congr' ?_).mpr h_tendsto rw [EventuallyEq, eventually_atTop] - exact ⟨0, fun _ ↦ rightDeriv_mul_log⟩ + exact ⟨1, fun _ hx ↦ rightDeriv_mul_log (zero_lt_one.trans_le hx).ne'⟩ lemma fDiv_mul_log_eq_top_iff [IsFiniteMeasure μ] [SigmaFinite ν] : fDiv (fun x ↦ x * log x) μ ν = ⊤ ↔ μ ≪ ν → ¬ Integrable (llr μ ν) μ := by diff --git a/TestingLowerBounds/ForMathlib/LeftRightDeriv.lean b/TestingLowerBounds/ForMathlib/LeftRightDeriv.lean index 733bd261..efe6b797 100644 --- a/TestingLowerBounds/ForMathlib/LeftRightDeriv.lean +++ b/TestingLowerBounds/ForMathlib/LeftRightDeriv.lean @@ -91,6 +91,14 @@ lemma rightDeriv_congr_atTop {g : ℝ → ℝ} (h : f =ᶠ[atTop] g) : filter_upwards [h_ge] using ha filter_upwards [h'] with a ha using ha.rightDeriv_eq_nhds +lemma rightDeriv_of_hasDerivAt {f : ℝ → ℝ} {f' : ℝ} {x : ℝ} (h : HasDerivAt f f' x) : + rightDeriv f x = f' := by + rw [rightDeriv_def, h.hasDerivWithinAt.derivWithin (uniqueDiffWithinAt_Ioi x)] + +lemma leftDeriv_of_hasDerivAt {f : ℝ → ℝ} {f' : ℝ} {x : ℝ} (h : HasDerivAt f f' x) : + leftDeriv f x = f' := by + rw [leftDeriv_def, h.hasDerivWithinAt.derivWithin (uniqueDiffWithinAt_Iio x)] + @[simp] lemma rightDeriv_zero : rightDeriv 0 = 0 := by ext x From 05ae496323fba2ad5f44add67be8451992620474 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Degenne?= Date: Sat, 3 Aug 2024 08:56:48 +0200 Subject: [PATCH 03/17] details about the integral representation --- blueprint/src/sections/dpi_div.tex | 2 +- blueprint/src/sections/f_divergence.tex | 96 +++++++++++++++++-------- 2 files changed, 66 insertions(+), 32 deletions(-) diff --git a/blueprint/src/sections/dpi_div.tex b/blueprint/src/sections/dpi_div.tex index 301d5072..a97fee57 100644 --- a/blueprint/src/sections/dpi_div.tex +++ b/blueprint/src/sections/dpi_div.tex @@ -93,7 +93,7 @@ \section{Generic divergences} \begin{lemma}[Conditioning increases divergence] - \label{lem:} + \label{lem:div_comp_le_div_compProd_right} %\lean{} %\leanok \uses{def:div, def:dpi} diff --git a/blueprint/src/sections/f_divergence.tex b/blueprint/src/sections/f_divergence.tex index 6e30cb10..6744cccb 100644 --- a/blueprint/src/sections/f_divergence.tex +++ b/blueprint/src/sections/f_divergence.tex @@ -476,14 +476,15 @@ \subsection{Conditional f-divergence} \subsection{Integral representation of $f$-divergences} -\begin{definition} +\begin{definition}[Curvature measure] \label{def:curvatureMeasure} \lean{ConvexOn.curvatureMeasure} \leanok \uses{} - Let $f: \mathbb{R} \to \mathbb{R}$ be a convex function. Then $f'_+(x) \coloneqq \lim_{y \downarrow x}\frac{f(y) - f(x)}{y - x}$ is a Stieltjes function (a monotone right continuous function) and it defines a measure $\gamma_f$ on $\mathbb{R}$ by $\gamma_f((x,y]) \coloneqq f'_+(y) - f'_+(x)$~. \cite{liese2012phi} calls $\gamma_f$ the curvature measure of $f$. + Let $f: \mathbb{R} \to \mathbb{R}$ be a convex function. Then its right derivative $f'_+(x) \coloneqq \lim_{y \downarrow x}\frac{f(y) - f(x)}{y - x}$ is a Stieltjes function (a monotone right continuous function) and it defines a measure $\gamma_f$ on $\mathbb{R}$ by $\gamma_f((x,y]) \coloneqq f'_+(y) - f'_+(x)$~. \cite{liese2012phi} calls $\gamma_f$ the curvature measure of $f$. \end{definition} + \begin{lemma} \label{lem:curvatureMeasure_mul} %\lean{} @@ -497,6 +498,21 @@ \subsection{Integral representation of $f$-divergences} \end{proof} + +\begin{lemma} + \label{lem:curvatureMeasure_add} + %\lean{} + %\leanok + \uses{def:curvatureMeasure} + For $f,g: \mathbb{R} \to \mathbb{R}$ two convex functions, the curvature measure of $f+g$ is $\gamma_{f+g} = \gamma_f + \gamma_g$~. +\end{lemma} + +\begin{proof}%\leanok +\uses{} + +\end{proof} + + \begin{lemma} \label{lem:convex_taylor} \lean{ConvexOn.convex_taylor} @@ -512,26 +528,22 @@ \subsection{Integral representation of $f$-divergences} \begin{proof}\leanok \uses{} - +Let $\Lambda$ be the Lebesgue measure and let $x < y$. Since $f$ has right derivative $f'_+$ in $(x,y)$ and $f'_+$ is integrable on that interval, +\begin{align*} +f(y) - f(x) = \int_{z \in (x, y]} f'_+(z) \partial \Lambda +\: . +\end{align*} +We now integrate by parts, using Theorem TODO. $\Lambda$ is the measure obtained from the Stieltjes function $z \mapsto z - y$. +\begin{align*} +\int_{z \in (x, y]} f'_+(z) \partial \Lambda +&= - \int_{z \in (x,y]} (z - y)\partial \gamma_f + f'_+(y)(y - y) - f'_+(x)(x - y) +\\ +&= \int_{z \in (x,y]} (y - z)\partial \gamma_f + f'_+(x)(y - x) +\: . +\end{align*} +Putting the two equalities together, we get the result for $x < y$. The proof for $x > y$ is similar, and for $x = y$ both sides of both equations are zero. \end{proof} -\begin{corollary} - \label{cor:convex_taylor_one} - %\lean{} - %\leanok - \uses{def:curvatureMeasure} - For $f: \mathbb{R} \to \mathbb{R}$ a convex function with $f(1) = 0$ and $f'_+(1) = 0$~, for all $x \in \mathbb{R}$~, - \begin{align*} - f(x) &= \int_{y \in (x, 1]} (y - x) \partial\gamma_f & \text{ for } x \le 1 \: , - \\ - f(x) &= \int_{y \in (1, x]} (x - y) \partial\gamma_f & \text{ for } x > 1 \: , - \end{align*} -\end{corollary} - -\begin{proof}%\leanok -\uses{lem:convex_taylor} - -\end{proof} \begin{definition} \label{def:statInfoFun} @@ -546,24 +558,28 @@ \subsection{Integral representation of $f$-divergences} \end{align*} \end{definition} + \begin{corollary} \label{cor:convex_taylor_statInfoFun} \lean{ProbabilityTheory.integral_statInfoFun_curvatureMeasure} \leanok \uses{def:curvatureMeasure, def:statInfoFun} - For $f: \mathbb{R} \to \mathbb{R}$ a convex function with $f(1) = 0$ and $f'_+(1) = 0$~, for all $x \in \mathbb{R}$~, + For $f: \mathbb{R} \to \mathbb{R}$ a convex function, for all $x \in \mathbb{R}$~, \begin{align*} - f(x) &= \int_{y} \phi_{1,y}(x) \partial\gamma_f \: . + f(x) &= f(1) + f'_+(1) (x - 1) + \int_{y} \phi_{1,y}(x) \partial\gamma_f \: . \end{align*} \end{corollary} \begin{proof}\leanok -\uses{cor:convex_taylor_one} -By Corollary~\ref{cor:convex_taylor_one}, for $x > 1$, +\uses{lem:convex_taylor} +By Lemma~\ref{lem:convex_taylor}, for $x > 1$, \begin{align*} -f(x) = \int_{y \in (1, x]} (x - y) \partial\gamma_f +f(x) - f(1) - f'_+(1) (x - 1) +&= \int_{y \in (1, x]} (x - y) \partial\gamma_f +\\ &= \int_{y \in (1, +\infty)} \max\{0, x - y\} \partial\gamma_f -= \int_{y \in (1, +\infty)} \phi_{1,y}(x) \partial\gamma_f +\\ +&= \int_{y \in (1, +\infty)} \phi_{1,y}(x) \partial\gamma_f \: . \end{align*} That final integral is equal to $\int_y \phi_{1,y}(x) \partial\gamma_f$ (without the restriction to $(1, +\infty)$) because $\phi_{1,y}(x)$ is zero outside of $(1, +\infty)$ for $x \ge 1$. @@ -571,6 +587,7 @@ \subsection{Integral representation of $f$-divergences} The case of $x < 1$ is similar. \end{proof} + \begin{lemma} \label{lem:curvatureMeasure_statInfoFun} %\lean{} @@ -591,7 +608,7 @@ \subsection{Integral representation of $f$-divergences} %\lean{} %\leanok \uses{def:fDiv, def:curvatureMeasure, def:eGamma} - For $\mu, \nu \in \mathcal M(\mathcal X)$, + For two finite measures $\mu, \nu \in \mathcal M(\mathcal X)$, \begin{align*} D_f(\mu, \nu) = f(1) \nu(\mathcal X) + f'_+(1)(\mu(\mathcal X) - \nu(\mathcal X)) + \int_y D_{\phi_{1,y}}(\mu, \nu) \partial\gamma_f \: . \end{align*} @@ -601,9 +618,7 @@ \subsection{Integral representation of $f$-divergences} \begin{proof}%\leanok \uses{cor:convex_taylor_statInfoFun} -TODO: this proof ignores the non-integral part of divergences and should be fixed. - -We prove the result for $f(1) = 0$ and $f'_+(1) = 0$. The general case is then a consequence of Lemma TODO. +We prove the result for $f(1) = 0$ and $f'_+(1) = 0$ for simplicity of exposition. From Corollary~\ref{cor:convex_taylor_statInfoFun} we get that $f(x) = \int_y \phi_{1,y}(x) \partial\gamma_f$~. From this and the theorem of Fubini, @@ -613,7 +628,26 @@ \subsection{Integral representation of $f$-divergences} = \int_{y} \int_{x} \phi_{1,y} \left(\frac{d \mu}{d \nu}(x) \right) \partial\nu \partial\gamma_f \: . \end{align*} -The inner integral is a divergence: $\int_{x} \phi_{1,y} \left(\frac{d \mu}{d \nu}(x) \right) \partial\nu = D_{\phi_{1,y}}(\mu, \nu)$~. +For the mutually singular part of the divergence $D_f$, +\begin{align*} +f'(\infty) += f'_+(\infty) - f'_+(1) += \gamma_f((1,+\infty)) += \int_{y > 1} 1 \partial \gamma_f += \int_{y > 1} \phi_{1,y}'(\infty) \partial \gamma_f +\: . +\end{align*} +The last integral is equal to $\int_{y \in \mathbb{R}} \phi_{1,y}'(\infty) \partial \gamma_f$ since $\phi_{1,y}'(\infty) = 0$ for $y \le 1$. +Finally, +\begin{align*} +D_f(\mu, \nu) +&= \int_x f\left( \frac{d \mu}{d \nu}(x) \right) \partial\nu + f'(\infty) \mu_{\perp \nu}(\mathcal X) +\\ +&= \int_{y} \left(\int_{x} \phi_{1,y} \left(\frac{d \mu}{d \nu}(x) \right) \partial\nu + \phi_{1,y}'(\infty) \mu(\mathcal X) \right) \partial\gamma_f +\\ +&= \int_y D_{\phi_{1,y}}(\mu, \nu) \partial \gamma_f +\: . +\end{align*} \end{proof} TODO: define $\Gamma_f$. From b099af579615504514e9159569a7ac8384f25455 Mon Sep 17 00:00:00 2001 From: Lorenzo Luccioli Date: Sat, 3 Aug 2024 15:12:21 +0200 Subject: [PATCH 04/17] rename fDiv_mono' and add comment --- TestingLowerBounds/FDiv/Basic.lean | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/TestingLowerBounds/FDiv/Basic.lean b/TestingLowerBounds/FDiv/Basic.lean index 5b42950d..b636db32 100644 --- a/TestingLowerBounds/FDiv/Basic.lean +++ b/TestingLowerBounds/FDiv/Basic.lean @@ -769,7 +769,7 @@ lemma fDiv_nonneg [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] 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) ν) +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] @@ -780,9 +780,10 @@ lemma fDiv_mono' (hf_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) 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) ν) +/- The hypothesis `hfg'` can probably be removed if we ask for the functions to be convex, since then it is true that `derivAtTop` is monotone, but we still don't have the result formalized. Moreover in the convex case we can also relax `hf_int` and only ask for a.e. strong measurability of `f` (at least when `μ` and `ν` are finite), because then the negative part of the function is always integrable, hence if `f` is not integrable `g` is also not integrable. -/ +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' + fDiv_mono'' hf_int (eventually_of_forall hfg) hfg' lemma fDiv_nonneg_of_nonneg (hf : 0 ≤ f) (hf' : 0 ≤ derivAtTop f) : 0 ≤ fDiv f μ ν := From 5982a5ff2bec1658da6386feee828d7b5a17e93c Mon Sep 17 00:00:00 2001 From: Lorenzo Luccioli Date: Sat, 3 Aug 2024 15:12:48 +0200 Subject: [PATCH 05/17] bug fix --- TestingLowerBounds/FDiv/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/TestingLowerBounds/FDiv/Basic.lean b/TestingLowerBounds/FDiv/Basic.lean index b636db32..b08fe754 100644 --- a/TestingLowerBounds/FDiv/Basic.lean +++ b/TestingLowerBounds/FDiv/Basic.lean @@ -787,7 +787,7 @@ lemma fDiv_mono' (hf_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν) 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') + 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 ℝ (Ici 0) f) From e483a8ae9b6810ca4ef8301109a7e706559f2d2b Mon Sep 17 00:00:00 2001 From: Lorenzo Luccioli Date: Sat, 3 Aug 2024 15:17:56 +0200 Subject: [PATCH 06/17] apply suggestions --- TestingLowerBounds/FDiv/Basic.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/TestingLowerBounds/FDiv/Basic.lean b/TestingLowerBounds/FDiv/Basic.lean index b08fe754..9402338c 100644 --- a/TestingLowerBounds/FDiv/Basic.lean +++ b/TestingLowerBounds/FDiv/Basic.lean @@ -143,9 +143,7 @@ lemma fDiv_congr (μ ν : Measure α) (h : ∀ x ≥ 0, f x = g x) : 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`? -lemma fDiv_of_zero_on_nonneg (μ ν : Measure α) (hf : ∀ x ≥ 0, f x = 0) : +lemma fDiv_eq_zero_of_forall_nonneg (μ ν : Measure α) (hf : ∀ x ≥ 0, f x = 0) : fDiv f μ ν = 0 := by have (x : α) : f ((∂μ/∂ν) x).toReal = 0 := hf _ ENNReal.toReal_nonneg rw [fDiv_of_integrable (by simp [this])] From 947992d06ba04091a07664db8da2e68f6d985b16 Mon Sep 17 00:00:00 2001 From: Lorenzo Luccioli Date: Tue, 6 Aug 2024 10:43:58 +0200 Subject: [PATCH 07/17] remove import --- TestingLowerBounds/Divergences/StatInfo.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/TestingLowerBounds/Divergences/StatInfo.lean b/TestingLowerBounds/Divergences/StatInfo.lean index f603a269..2edc68ad 100644 --- a/TestingLowerBounds/Divergences/StatInfo.lean +++ b/TestingLowerBounds/Divergences/StatInfo.lean @@ -10,7 +10,6 @@ import TestingLowerBounds.FDiv.Basic import TestingLowerBounds.Testing.Binary import Mathlib.MeasureTheory.Constructions.Prod.Integral import TestingLowerBounds.ForMathlib.SetIntegral -import Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup /-! # Statistical information From 22f59bcc35d8875da8068ae01f1546f5de271442 Mon Sep 17 00:00:00 2001 From: Lorenzo Luccioli Date: Tue, 6 Aug 2024 10:44:22 +0200 Subject: [PATCH 08/17] move fDiv_eq_fDiv_centeredFunction --- TestingLowerBounds/Divergences/StatInfo.lean | 20 ------------------ TestingLowerBounds/FDiv/Basic.lean | 22 ++++++++++++++++++++ 2 files changed, 22 insertions(+), 20 deletions(-) diff --git a/TestingLowerBounds/Divergences/StatInfo.lean b/TestingLowerBounds/Divergences/StatInfo.lean index 2edc68ad..719edb46 100644 --- a/TestingLowerBounds/Divergences/StatInfo.lean +++ b/TestingLowerBounds/Divergences/StatInfo.lean @@ -717,26 +717,6 @@ lemma integral_statInfoFun_curvatureMeasure' (hf_cvx : ConvexOn ℝ univ f) (hf_ rw [integral_statInfoFun_curvatureMeasure hf_cvx hf_cont, hf_one, hfderiv_one, sub_zero, zero_mul, sub_zero] -lemma fDiv_eq_fDiv_centeredFunction [IsFiniteMeasure μ] [IsFiniteMeasure ν] - (hf_cvx : ConvexOn ℝ univ f) : - fDiv f μ ν = fDiv (fun x ↦ f x - f 1 - rightDeriv f 1 * (x - 1)) μ ν - + f 1 * ν univ + rightDeriv f 1 * ((μ univ).toReal - (ν univ).toReal) := by - simp_rw [sub_eq_add_neg (f _), sub_eq_add_neg (_ + _), ← neg_mul] - rw [fDiv_add_linear'] - swap; · exact hf_cvx.subset (fun _ _ ↦ trivial) (convex_Ici 0) |>.add_const _ - rw [fDiv_add_const] - swap; · exact hf_cvx.subset (fun _ _ ↦ trivial) (convex_Ici 0) - simp_rw [EReal.coe_neg, neg_mul] - rw [add_assoc, add_comm (_ * _), ← add_assoc, add_assoc _ (-(_ * _)), add_comm (-(_ * _)), - ← sub_eq_add_neg (_ * _), EReal.sub_self, add_zero] - rotate_left - · refine (EReal.mul_ne_top _ _).mpr ⟨?_, Or.inr <| EReal.add_top_iff_ne_bot.mp rfl, - ?_, Or.inr <| Ne.symm (ne_of_beq_false rfl)⟩ <;> simp - · refine (EReal.mul_ne_bot _ _).mpr ⟨?_, Or.inr <| EReal.add_top_iff_ne_bot.mp rfl, - ?_, Or.inr <| Ne.symm (ne_of_beq_false rfl)⟩ <;> simp - rw [add_assoc, add_comm (-(_ * _)), ← sub_eq_add_neg, EReal.sub_self, add_zero] - <;> simp [EReal.mul_ne_top, EReal.mul_ne_bot, measure_ne_top] - lemma lintegral_f_rnDeriv_eq_lintegralfDiv_statInfoFun_of_absolutelyContinuous [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hf_cvx : ConvexOn ℝ univ f) (hf_cont : Continuous f) (hf_one : f 1 = 0) (hfderiv_one : rightDeriv f 1 = 0) (h_ac : μ ≪ ν) : diff --git a/TestingLowerBounds/FDiv/Basic.lean b/TestingLowerBounds/FDiv/Basic.lean index 9402338c..6b9db311 100644 --- a/TestingLowerBounds/FDiv/Basic.lean +++ b/TestingLowerBounds/FDiv/Basic.lean @@ -6,6 +6,8 @@ Authors: Rémy Degenne, Lorenzo Luccioli import TestingLowerBounds.DerivAtTop import TestingLowerBounds.ForMathlib.RadonNikodym import TestingLowerBounds.ForMathlib.RnDeriv +-- TODO: remove this import after the next mathlib bump, now it is only needed for `ConvexOn.add_const`, but this lemma has recently been moved to `Mathlib.Analysis.Convex.Function`. +import Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup /-! @@ -361,6 +363,26 @@ lemma fDiv_add_linear {c : ℝ} [IsFiniteMeasure μ] [IsFiniteMeasure ν] rw [fDiv_add_linear' hf_cvx, h_eq, ← EReal.coe_sub, sub_self] simp +lemma fDiv_eq_fDiv_centeredFunction [IsFiniteMeasure μ] [IsFiniteMeasure ν] + (hf_cvx : ConvexOn ℝ univ f) : + fDiv f μ ν = fDiv (fun x ↦ f x - f 1 - rightDeriv f 1 * (x - 1)) μ ν + + f 1 * ν univ + rightDeriv f 1 * ((μ univ).toReal - (ν univ).toReal) := by + simp_rw [sub_eq_add_neg (f _), sub_eq_add_neg (_ + _), ← neg_mul] + rw [fDiv_add_linear'] + swap; · exact hf_cvx.subset (fun _ _ ↦ trivial) (convex_Ici 0) |>.add_const _ + rw [fDiv_add_const] + swap; · exact hf_cvx.subset (fun _ _ ↦ trivial) (convex_Ici 0) + simp_rw [EReal.coe_neg, neg_mul] + rw [add_assoc, add_comm (_ * _), ← add_assoc, add_assoc _ (-(_ * _)), add_comm (-(_ * _)), + ← sub_eq_add_neg (_ * _), EReal.sub_self, add_zero] + rotate_left + · refine (EReal.mul_ne_top _ _).mpr ⟨?_, Or.inr <| EReal.add_top_iff_ne_bot.mp rfl, + ?_, Or.inr <| Ne.symm (ne_of_beq_false rfl)⟩ <;> simp + · refine (EReal.mul_ne_bot _ _).mpr ⟨?_, Or.inr <| EReal.add_top_iff_ne_bot.mp rfl, + ?_, Or.inr <| Ne.symm (ne_of_beq_false rfl)⟩ <;> simp + rw [add_assoc, add_comm (-(_ * _)), ← sub_eq_add_neg, EReal.sub_self, add_zero] + <;> simp [EReal.mul_ne_top, EReal.mul_ne_bot, measure_ne_top] + lemma fDiv_of_mutuallySingular [SigmaFinite μ] [IsFiniteMeasure ν] (h : μ ⟂ₘ ν) : fDiv f μ ν = (f 0 : EReal) * ν Set.univ + derivAtTop f * μ Set.univ := by have : μ.singularPart ν = μ := (μ.singularPart_eq_self).mpr h From 21d56c96d18c8f8c6b4759cb89dded27ccc1745e Mon Sep 17 00:00:00 2001 From: Lorenzo Luccioli Date: Tue, 6 Aug 2024 10:58:24 +0200 Subject: [PATCH 09/17] apply suggestion --- TestingLowerBounds/Divergences/StatInfo.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/TestingLowerBounds/Divergences/StatInfo.lean b/TestingLowerBounds/Divergences/StatInfo.lean index 719edb46..12c81933 100644 --- a/TestingLowerBounds/Divergences/StatInfo.lean +++ b/TestingLowerBounds/Divergences/StatInfo.lean @@ -150,8 +150,6 @@ lemma toReal_statInfo_eq_min_sub_integral (μ ν : Measure 𝒳) [IsFiniteMeasur rw [toReal_bayesBinaryRisk_eq_integral_min, MonotoneOn.map_min (fun _ _ _ hb hab ↦ ENNReal.toReal_mono hb hab) hμ hν] -#check Measure.rnDeriv_eq_div' - lemma toReal_statInfo_eq_min_sub_integral' {ζ : Measure 𝒳} [IsFiniteMeasure μ] [IsFiniteMeasure ν] [SigmaFinite ζ] (π : Measure Bool) [IsFiniteMeasure π] (hμζ : μ ≪ ζ) (hνζ : ν ≪ ζ) : (statInfo μ ν π).toReal = min (π {false} * μ univ).toReal (π {true} * ν univ).toReal From f627eacb50763db6341479c1f86d20db523a780e Mon Sep 17 00:00:00 2001 From: Lorenzo Luccioli <71074618+LorenzoLuccioli@users.noreply.github.com> Date: Tue, 6 Aug 2024 11:03:18 +0200 Subject: [PATCH 10/17] Update TestingLowerBounds/Divergences/StatInfo.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Rémy Degenne --- TestingLowerBounds/Divergences/StatInfo.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/TestingLowerBounds/Divergences/StatInfo.lean b/TestingLowerBounds/Divergences/StatInfo.lean index 12c81933..40b3b98b 100644 --- a/TestingLowerBounds/Divergences/StatInfo.lean +++ b/TestingLowerBounds/Divergences/StatInfo.lean @@ -695,7 +695,7 @@ lemma fDiv_statInfoFun_eq_StatInfo_of_nonneg [IsFiniteMeasure μ] [IsFiniteMeasu · rw [fDiv_statInfoFun_eq_StatInfo_of_nonneg_of_gt hβ hγ hβγ, if_neg hβγ.not_le, one_mul, add_sub_assoc] -lemma fDiv_statInfoFun_ne_top_of_nonneg [IsFiniteMeasure μ] [IsFiniteMeasure ν] : +lemma fDiv_statInfoFun_ne_top [IsFiniteMeasure μ] [IsFiniteMeasure ν] : fDiv (statInfoFun β γ) μ ν ≠ ⊤ := by simp [derivAtTop_statInfoFun_ne_top, fDiv_ne_top_iff, integrable_statInfoFun_rnDeriv] From 3707382da8dbbfbc05df5e8818380f9c53da2485 Mon Sep 17 00:00:00 2001 From: Lorenzo Luccioli Date: Tue, 6 Aug 2024 11:05:22 +0200 Subject: [PATCH 11/17] fix bugs --- TestingLowerBounds/Divergences/StatInfo.lean | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/TestingLowerBounds/Divergences/StatInfo.lean b/TestingLowerBounds/Divergences/StatInfo.lean index 40b3b98b..393541f2 100644 --- a/TestingLowerBounds/Divergences/StatInfo.lean +++ b/TestingLowerBounds/Divergences/StatInfo.lean @@ -769,8 +769,7 @@ lemma fDiv_ne_top_iff_integrable_fDiv_statInfoFun_of_absolutelyContinuous' rotate_left · exact (fDiv_statInfoFun_stronglyMeasurable μ ν).measurable.comp (f := fun x ↦ (1, x)) (by fun_prop) |>.ereal_toENNReal.aemeasurable - · exact eventually_of_forall fun _ ↦ EReal.toENNReal_ne_top_iff.mpr - fDiv_statInfoFun_ne_top_of_nonneg + · exact eventually_of_forall fun _ ↦ EReal.toENNReal_ne_top_iff.mpr fDiv_statInfoFun_ne_top rw [lintegral_f_rnDeriv_eq_lintegralfDiv_statInfoFun_of_absolutelyContinuous hf_cvx hf_cont hf_one hfderiv_one h_ac] @@ -882,15 +881,14 @@ lemma fDiv_eq_lintegral_fDiv_statInfoFun_of_absolutelyContinuous · exact eventually_of_forall <| fun _ ↦ EReal.toReal_nonneg fDiv_statInfoFun_nonneg · exact (fDiv_statInfoFun_stronglyMeasurable μ ν).measurable.comp (f := fun x ↦ (1, x)) (by fun_prop) |>.ereal_toReal.aestronglyMeasurable - simp_rw [← EReal.toENNReal_of_ne_top fDiv_statInfoFun_ne_top_of_nonneg] + simp_rw [← EReal.toENNReal_of_ne_top fDiv_statInfoFun_ne_top] rw [ENNReal.toReal_toEReal_of_ne_top] rw [integrable_f_rnDeriv_iff_integrable_fDiv_statInfoFun_of_absolutelyContinuous hf_cvx hf_cont h_ac] at h_int refine (integrable_toReal_iff ?_ ?_).mp ?_ · exact (fDiv_statInfoFun_stronglyMeasurable μ ν).measurable.comp (f := fun x ↦ (1, x)) (by fun_prop) |>.ereal_toENNReal.aemeasurable - · exact eventually_of_forall fun _ ↦ EReal.toENNReal_ne_top_iff.mpr - fDiv_statInfoFun_ne_top_of_nonneg + · exact eventually_of_forall fun _ ↦ EReal.toENNReal_ne_top_iff.mpr fDiv_statInfoFun_ne_top simp_rw [EReal.toReal_toENNReal fDiv_statInfoFun_nonneg, h_int] · classical rw [fDiv_of_absolutelyContinuous h_ac, if_neg h_int] @@ -907,8 +905,7 @@ lemma fDiv_eq_lintegral_fDiv_statInfoFun_of_absolutelyContinuous refine (integrable_toReal_iff ?_ ?_).mpr h · exact (fDiv_statInfoFun_stronglyMeasurable μ ν).measurable.comp (f := fun x ↦ (1, x)) (by fun_prop) |>.ereal_toENNReal.aemeasurable - · exact eventually_of_forall fun _ ↦ EReal.toENNReal_ne_top_iff.mpr - fDiv_statInfoFun_ne_top_of_nonneg + · exact eventually_of_forall fun _ ↦ EReal.toENNReal_ne_top_iff.mpr fDiv_statInfoFun_ne_top end StatInfoFun From c14b5fa5f8b346a1b7897f7a63554df7809cf5e7 Mon Sep 17 00:00:00 2001 From: Lorenzo Luccioli Date: Tue, 6 Aug 2024 16:08:51 +0200 Subject: [PATCH 12/17] apply suggestion --- TestingLowerBounds/CurvatureMeasure.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/TestingLowerBounds/CurvatureMeasure.lean b/TestingLowerBounds/CurvatureMeasure.lean index a4cc7772..174278cc 100644 --- a/TestingLowerBounds/CurvatureMeasure.lean +++ b/TestingLowerBounds/CurvatureMeasure.lean @@ -44,36 +44,36 @@ lemma measure_Ioi {l : ℝ} (hf : Tendsto f atTop (𝓝 l)) (x : ℝ) : --PR this and the following lemmas to mathlib, just after `StieltjesFunction.measure_univ` lemma measure_Ioi_of_tendsto_atTop_atTop (hf : Tendsto f atTop atTop) (x : ℝ) : - f.measure (Ioi x) = ⊤ := by + f.measure (Ioi x) = ∞ := by refine ENNReal.eq_top_of_forall_nnreal_le fun r ↦ ?_ obtain ⟨N, hN⟩ := eventually_atTop.mp (tendsto_atTop.mp hf (r + f x)) exact (f.measure_Ioc x (max x N) ▸ ENNReal.coe_nnreal_eq r ▸ (ENNReal.ofReal_le_ofReal <| le_tsub_of_add_le_right <| hN _ (le_max_right x N))).trans (measure_mono Ioc_subset_Ioi_self) lemma measure_Ici_of_tendsto_atTop_atTop (hf : Tendsto f atTop atTop) (x : ℝ) : - f.measure (Ici x) = ⊤ := by + f.measure (Ici x) = ∞ := by rw [← top_le_iff, ← f.measure_Ioi_of_tendsto_atTop_atTop hf x] exact measure_mono Ioi_subset_Ici_self lemma measure_Iic_of_tendsto_atBot_atBot (hf : Tendsto f atBot atBot) (x : ℝ) : - f.measure (Iic x) = ⊤ := by + f.measure (Iic x) = ∞ := by refine ENNReal.eq_top_of_forall_nnreal_le fun r ↦ ?_ obtain ⟨N, hN⟩ := eventually_atBot.mp (tendsto_atBot.mp hf (f x - r)) exact (f.measure_Ioc (min x N) x ▸ ENNReal.coe_nnreal_eq r ▸ (ENNReal.ofReal_le_ofReal <| le_sub_comm.mp <| hN _ (min_le_right x N))).trans (measure_mono Ioc_subset_Iic_self) lemma measure_Iio_of_tendsto_atBot_atBot (hf : Tendsto f atBot atBot) (x : ℝ) : - f.measure (Iio x) = ⊤ := by + f.measure (Iio x) = ∞ := by rw [← top_le_iff, ← f.measure_Iic_of_tendsto_atBot_atBot hf (x - 1)] exact measure_mono <| Set.Iic_subset_Iio.mpr <| sub_one_lt x lemma measure_univ_of_tendsto_atTop_atTop (hf : Tendsto f atTop atTop) : - f.measure univ = ⊤ := by + f.measure univ = ∞ := by rw [← top_le_iff, ← f.measure_Ioi_of_tendsto_atTop_atTop hf 0] exact measure_mono fun _ _ ↦ trivial lemma measure_univ_of_tendsto_atBot_atBot (hf : Tendsto f atBot atBot) : - f.measure univ = ⊤ := by + f.measure univ = ∞ := by rw [← top_le_iff, ← f.measure_Iio_of_tendsto_atBot_atBot hf 0] exact measure_mono fun _ _ ↦ trivial From 03ec7e403fea910fdddcb64d156cfcb9f7ed341c Mon Sep 17 00:00:00 2001 From: Lorenzo Luccioli Date: Tue, 6 Aug 2024 16:18:21 +0200 Subject: [PATCH 13/17] apply suggestion --- TestingLowerBounds/DerivAtTop.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/TestingLowerBounds/DerivAtTop.lean b/TestingLowerBounds/DerivAtTop.lean index ba08cbf1..60865b41 100644 --- a/TestingLowerBounds/DerivAtTop.lean +++ b/TestingLowerBounds/DerivAtTop.lean @@ -159,8 +159,8 @@ lemma ConvexOn.derivAtTop_eq_iff {y : EReal} (hf : ConvexOn ℝ (Ici 0) f) : lemma MonotoneOn.derivAtTop_eq_top_iff (hf : MonotoneOn (rightDeriv f) (Ioi 0)) : derivAtTop f = ⊤ ↔ Tendsto (rightDeriv f) atTop atTop := by refine ⟨fun h ↦ ?_, fun h ↦ derivAtTop_of_tendsto_atTop h⟩ - exact EReal.tendsto_toReal_atTop.comp (tendsto_punctured_nhds_of_tendsto_nhds_right - (eventually_of_forall fun _ ↦ EReal.coe_ne_top _) (h ▸ hf.tendsto_derivAtTop)) + exact EReal.tendsto_toReal_atTop.comp (tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ + (h ▸ hf.tendsto_derivAtTop) (eventually_of_forall fun _ ↦ EReal.coe_ne_top _)) lemma ConvexOn.derivAtTop_eq_top_iff (hf : ConvexOn ℝ (Ici 0) f) : derivAtTop f = ⊤ ↔ Tendsto (rightDeriv f) atTop atTop := From e761044d3193d01a939809b30430930b633bc609 Mon Sep 17 00:00:00 2001 From: Lorenzo Luccioli Date: Tue, 6 Aug 2024 16:18:51 +0200 Subject: [PATCH 14/17] delete `Tendsto.lean` --- TestingLowerBounds/ForMathlib/Tendsto.lean | 23 ---------------------- 1 file changed, 23 deletions(-) delete mode 100644 TestingLowerBounds/ForMathlib/Tendsto.lean diff --git a/TestingLowerBounds/ForMathlib/Tendsto.lean b/TestingLowerBounds/ForMathlib/Tendsto.lean deleted file mode 100644 index 999c0327..00000000 --- a/TestingLowerBounds/ForMathlib/Tendsto.lean +++ /dev/null @@ -1,23 +0,0 @@ -import Mathlib.Topology.ContinuousOn - -open Filter Set - -open scoped Topology - -variable {α β : Type*} [TopologicalSpace β] {f : α → β} {b : β} {l : Filter α} - ---I'm not sure if something that easily implies those lemmas already exists in mathlib, they can probably be proved in a simpler and more elegant way than I did. - -lemma tendsto_nhdsWithin_of_tendsto_nhds_right {t : Set β} (hf : ∀ᶠ x in l, f x ∈ t) - (h : Tendsto f l (𝓝 b)) : Tendsto f l (𝓝[t] b) := by - simp_rw [Tendsto, Filter.le_def, mem_map] at h ⊢ - intro s hs - rcases mem_nhdsWithin_iff_exists_mem_nhds_inter.mp hs with ⟨U, hU, hU'⟩ - specialize h (s ∪ tᶜ) (mem_of_superset hU (union_comm _ _ ▸ ((Set.inter_subset _ _ _).mp hU'))) - filter_upwards [hf, h] with x hx hx' - rw [mem_preimage] at hx' ⊢ - simp_all - -lemma tendsto_punctured_nhds_of_tendsto_nhds_right (hf : ∀ᶠ x in l, f x ≠ b) - (h : Tendsto f l (𝓝 b)) : Tendsto f l (𝓝[≠] b) := - tendsto_nhdsWithin_of_tendsto_nhds_right hf h From 54ec946209c1b3aae82001e31e39b2fc1abda31c Mon Sep 17 00:00:00 2001 From: Lorenzo Luccioli Date: Tue, 6 Aug 2024 16:24:50 +0200 Subject: [PATCH 15/17] fix bug --- TestingLowerBounds/DerivAtTop.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/TestingLowerBounds/DerivAtTop.lean b/TestingLowerBounds/DerivAtTop.lean index 60865b41..39cf73aa 100644 --- a/TestingLowerBounds/DerivAtTop.lean +++ b/TestingLowerBounds/DerivAtTop.lean @@ -6,7 +6,6 @@ Authors: Rémy Degenne import TestingLowerBounds.Convex import TestingLowerBounds.ForMathlib.LeftRightDeriv import TestingLowerBounds.ForMathlib.EReal -import TestingLowerBounds.ForMathlib.Tendsto /-! From 1b1f98cd83861469f023b2a2c652c70fc5295d7b Mon Sep 17 00:00:00 2001 From: Lorenzo Luccioli Date: Tue, 6 Aug 2024 17:20:27 +0200 Subject: [PATCH 16/17] apply suggestion --- TestingLowerBounds/Divergences/StatInfo.lean | 6 +++--- TestingLowerBounds/ForMathlib/EReal.lean | 8 ++++---- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/TestingLowerBounds/Divergences/StatInfo.lean b/TestingLowerBounds/Divergences/StatInfo.lean index d03cb0b1..9511fe96 100644 --- a/TestingLowerBounds/Divergences/StatInfo.lean +++ b/TestingLowerBounds/Divergences/StatInfo.lean @@ -969,10 +969,10 @@ lemma fDiv_eq_lintegral_fDiv_statInfoFun_of_mutuallySingular [IsFiniteMeasure μ · rw [h_top, EReal.top_sub_coe, EReal.toENNReal_top, StieltjesFunction.measure_Ioi_of_tendsto_atTop_atTop] exact hf_cvx'.derivAtTop_eq_top_iff.mp h_top - · have ⟨x, hx⟩ := EReal.eq_coe_of_ne_top_of_ne_bot h_top hf_cvx'.derivAtTop_ne_bot - rw [hx, StieltjesFunction.measure_Ioi _ ?_ 1 (l := x)] + · lift (derivAtTop f) to ℝ using ⟨h_top, hf_cvx'.derivAtTop_ne_bot⟩ with x hx + rw [StieltjesFunction.measure_Ioi _ ?_ 1 (l := x)] · norm_cast - exact (hx ▸ hf_cvx'.tendsto_toReal_derivAtTop h_top :) + exact (hx ▸ hf_cvx'.tendsto_toReal_derivAtTop (hx ▸ h_top) :) simp_rw [fDiv_of_mutuallySingular h_ms, h1] push_cast rw [lintegral_statInfoFun_one_zero hf_cvx hf_cont, h2, EReal.coe_toENNReal] diff --git a/TestingLowerBounds/ForMathlib/EReal.lean b/TestingLowerBounds/ForMathlib/EReal.lean index d506d384..2fc32964 100644 --- a/TestingLowerBounds/ForMathlib/EReal.lean +++ b/TestingLowerBounds/ForMathlib/EReal.lean @@ -288,12 +288,12 @@ lemma toReal_eq_zero_iff {x : EReal} : x.toReal = 0 ↔ x = 0 ∨ x = ⊤ ∨ x induction x <;> norm_num lemma sub_nonneg {x y : EReal} (hy : y ≠ ⊤) (hy' : y ≠ ⊥) : 0 ≤ x - y ↔ y ≤ x := by - obtain ⟨_, ha⟩ := eq_coe_of_ne_top_of_ne_bot hy hy' - induction x <;> simp [← EReal.coe_sub, ha] + lift y to ℝ using ⟨hy, hy'⟩ + induction x <;> simp [← EReal.coe_sub] lemma sub_nonpos {x y : EReal} (hy : y ≠ ⊤) (hy' : y ≠ ⊥) : x - y ≤ 0 ↔ x ≤ y := by - obtain ⟨_, ha⟩ := eq_coe_of_ne_top_of_ne_bot hy hy' - induction x <;> simp [← EReal.coe_sub, ha] + lift y to ℝ using ⟨hy, hy'⟩ + induction x <;> simp [← EReal.coe_sub] @[simp] lemma nsmul_eq_mul {n : ℕ} {x : EReal} : n • x = n * x := by From c8050ed7be37e6ae921f8c2bd926f323e7766307 Mon Sep 17 00:00:00 2001 From: Lorenzo Luccioli Date: Tue, 6 Aug 2024 17:20:57 +0200 Subject: [PATCH 17/17] apply suggestion --- TestingLowerBounds/ForMathlib/EReal.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/TestingLowerBounds/ForMathlib/EReal.lean b/TestingLowerBounds/ForMathlib/EReal.lean index 2fc32964..34e34de1 100644 --- a/TestingLowerBounds/ForMathlib/EReal.lean +++ b/TestingLowerBounds/ForMathlib/EReal.lean @@ -9,9 +9,6 @@ namespace EReal instance : CharZero EReal := inferInstanceAs (CharZero (WithBot (WithTop ℝ))) -lemma eq_coe_of_ne_top_of_ne_bot {x : EReal} (hx : x ≠ ⊤) (hx' : x ≠ ⊥) : ∃ r : ℝ, x = r := by - induction x <;> tauto - lemma coe_ennreal_toReal {x : ℝ≥0∞} (hx : x ≠ ∞) : (x.toReal : EReal) = x := by lift x to ℝ≥0 using hx rfl