fDiv and StatInfo #
theorem
ProbabilityTheory.nnreal_mul_fDiv_statInfoFun
{𝒳 : Type u_1}
{m𝒳 : MeasurableSpace 𝒳}
{μ : MeasureTheory.Measure 𝒳}
{ν : MeasureTheory.Measure 𝒳}
{β : ℝ}
{γ : ℝ}
{a : NNReal}
:
↑↑a * ProbabilityTheory.fDiv (ProbabilityTheory.statInfoFun β γ) μ ν = ProbabilityTheory.fDiv (fun (x : ℝ) => ProbabilityTheory.statInfoFun (↑a * β) (↑a * γ) x) μ ν
theorem
ProbabilityTheory.fDiv_statInfoFun_nonneg
{𝒳 : Type u_1}
{m𝒳 : MeasurableSpace 𝒳}
{μ : MeasureTheory.Measure 𝒳}
{ν : MeasureTheory.Measure 𝒳}
{β : ℝ}
{γ : ℝ}
:
0 ≤ ProbabilityTheory.fDiv (ProbabilityTheory.statInfoFun β γ) μ ν
theorem
ProbabilityTheory.stronglyMeasurable_fDiv_statInfoFun
{𝒳 : Type u_1}
{m𝒳 : MeasurableSpace 𝒳}
(μ : MeasureTheory.Measure 𝒳)
(ν : MeasureTheory.Measure 𝒳)
[MeasureTheory.SFinite ν]
:
MeasureTheory.StronglyMeasurable
(Function.uncurry fun (β γ : ℝ) => ProbabilityTheory.fDiv (ProbabilityTheory.statInfoFun β γ) μ ν)
theorem
ProbabilityTheory.fDiv_statInfoFun_eq_integral_max_of_nonneg_of_le
{𝒳 : Type u_1}
{m𝒳 : MeasurableSpace 𝒳}
{μ : MeasureTheory.Measure 𝒳}
{ν : MeasureTheory.Measure 𝒳}
{β : ℝ}
{γ : ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hβ : 0 ≤ β)
(hγ : γ ≤ β)
:
ProbabilityTheory.fDiv (ProbabilityTheory.statInfoFun β γ) μ ν = ↑(∫ (x : 𝒳), max 0 (γ - β * (μ.rnDeriv ν x).toReal) ∂ν)
theorem
ProbabilityTheory.fDiv_statInfoFun_eq_integral_max_of_nonneg_of_gt
{𝒳 : Type u_1}
{m𝒳 : MeasurableSpace 𝒳}
{μ : MeasureTheory.Measure 𝒳}
{ν : MeasureTheory.Measure 𝒳}
{β : ℝ}
{γ : ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hβ : 0 ≤ β)
(hγ : β < γ)
:
ProbabilityTheory.fDiv (ProbabilityTheory.statInfoFun β γ) μ ν = ↑(∫ (x : 𝒳), max 0 (β * (μ.rnDeriv ν x).toReal - γ) ∂ν) + ↑β * ↑((μ.singularPart ν) Set.univ)
theorem
ProbabilityTheory.fDiv_statInfoFun_eq_integral_max_of_nonpos_of_le
{𝒳 : Type u_1}
{m𝒳 : MeasurableSpace 𝒳}
{μ : MeasureTheory.Measure 𝒳}
{ν : MeasureTheory.Measure 𝒳}
{β : ℝ}
{γ : ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hβ : β ≤ 0)
(hγ : γ ≤ β)
:
ProbabilityTheory.fDiv (ProbabilityTheory.statInfoFun β γ) μ ν = ↑(∫ (x : 𝒳), max 0 (γ - β * (μ.rnDeriv ν x).toReal) ∂ν) - ↑β * ↑((μ.singularPart ν) Set.univ)
theorem
ProbabilityTheory.fDiv_statInfoFun_eq_integral_max_of_nonpos_of_gt
{𝒳 : Type u_1}
{m𝒳 : MeasurableSpace 𝒳}
{μ : MeasureTheory.Measure 𝒳}
{ν : MeasureTheory.Measure 𝒳}
{β : ℝ}
{γ : ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hβ : β ≤ 0)
(hγ : β < γ)
:
ProbabilityTheory.fDiv (ProbabilityTheory.statInfoFun β γ) μ ν = ↑(∫ (x : 𝒳), max 0 (β * (μ.rnDeriv ν x).toReal - γ) ∂ν)
theorem
ProbabilityTheory.fDiv_statInfoFun_eq_zero_of_nonneg_of_nonpos
{𝒳 : Type u_1}
{m𝒳 : MeasurableSpace 𝒳}
{μ : MeasureTheory.Measure 𝒳}
{ν : MeasureTheory.Measure 𝒳}
{β : ℝ}
{γ : ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hβ : 0 ≤ β)
(hγ : γ ≤ 0)
:
ProbabilityTheory.fDiv (ProbabilityTheory.statInfoFun β γ) μ ν = 0
theorem
ProbabilityTheory.fDiv_statInfoFun_eq_zero_of_nonpos_of_pos
{𝒳 : Type u_1}
{m𝒳 : MeasurableSpace 𝒳}
{μ : MeasureTheory.Measure 𝒳}
{ν : MeasureTheory.Measure 𝒳}
{β : ℝ}
{γ : ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hβ : β ≤ 0)
(hγ : 0 < γ)
:
ProbabilityTheory.fDiv (ProbabilityTheory.statInfoFun β γ) μ ν = 0
theorem
ProbabilityTheory.integral_max_eq_integral_abs
{𝒳 : Type u_1}
{m𝒳 : MeasurableSpace 𝒳}
{μ : MeasureTheory.Measure 𝒳}
{ν : MeasureTheory.Measure 𝒳}
{β : ℝ}
{γ : ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
:
Auxiliary lemma for fDiv_statInfoFun_eq_integral_abs_of_nonneg_of_le and
fDiv_statInfoFun_eq_integral_abs_of_nonpos_of_le.
theorem
ProbabilityTheory.integral_max_eq_integral_abs'
{𝒳 : Type u_1}
{m𝒳 : MeasurableSpace 𝒳}
{μ : MeasureTheory.Measure 𝒳}
{ν : MeasureTheory.Measure 𝒳}
{β : ℝ}
{γ : ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
:
Auxiliary lemma for fDiv_statInfoFun_eq_integral_abs_of_nonneg_of_gt and
fDiv_statInfoFun_eq_integral_abs_of_nonpos_of_gt.
theorem
ProbabilityTheory.fDiv_statInfoFun_eq_integral_abs_of_nonneg_of_le
{𝒳 : Type u_1}
{m𝒳 : MeasurableSpace 𝒳}
{μ : MeasureTheory.Measure 𝒳}
{ν : MeasureTheory.Measure 𝒳}
{β : ℝ}
{γ : ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hβ : 0 ≤ β)
(hγ : γ ≤ β)
:
theorem
ProbabilityTheory.fDiv_statInfoFun_eq_integral_abs_of_nonneg_of_gt
{𝒳 : Type u_1}
{m𝒳 : MeasurableSpace 𝒳}
{μ : MeasureTheory.Measure 𝒳}
{ν : MeasureTheory.Measure 𝒳}
{β : ℝ}
{γ : ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hβ : 0 ≤ β)
(hγ : β < γ)
:
theorem
ProbabilityTheory.fDiv_statInfoFun_eq_integral_abs_of_nonpos_of_le
{𝒳 : Type u_1}
{m𝒳 : MeasurableSpace 𝒳}
{μ : MeasureTheory.Measure 𝒳}
{ν : MeasureTheory.Measure 𝒳}
{β : ℝ}
{γ : ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hβ : β ≤ 0)
(hγ : γ ≤ β)
:
theorem
ProbabilityTheory.fDiv_statInfoFun_eq_integral_abs_of_nonpos_of_gt
{𝒳 : Type u_1}
{m𝒳 : MeasurableSpace 𝒳}
{μ : MeasureTheory.Measure 𝒳}
{ν : MeasureTheory.Measure 𝒳}
{β : ℝ}
{γ : ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hβ : β ≤ 0)
(hγ : β < γ)
:
theorem
ProbabilityTheory.fDiv_statInfoFun_eq_StatInfo_of_nonneg_of_le
{𝒳 : Type u_1}
{m𝒳 : MeasurableSpace 𝒳}
{μ : MeasureTheory.Measure 𝒳}
{ν : MeasureTheory.Measure 𝒳}
{β : ℝ}
{γ : ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hβ : 0 ≤ β)
(hγ : 0 ≤ γ)
(hγβ : γ ≤ β)
:
ProbabilityTheory.fDiv (ProbabilityTheory.statInfoFun β γ) μ ν = ↑(ProbabilityTheory.statInfo μ ν (Bool.boolMeasure (ENNReal.ofReal β) (ENNReal.ofReal γ))) + 2⁻¹ * (↑|β * (μ Set.univ).toReal - γ * (ν Set.univ).toReal| + ↑γ * ↑(ν Set.univ).toReal - ↑β * ↑(μ Set.univ).toReal)
theorem
ProbabilityTheory.fDiv_statInfoFun_eq_StatInfo_of_nonneg_of_gt
{𝒳 : Type u_1}
{m𝒳 : MeasurableSpace 𝒳}
{μ : MeasureTheory.Measure 𝒳}
{ν : MeasureTheory.Measure 𝒳}
{β : ℝ}
{γ : ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hβ : 0 ≤ β)
(hγ : 0 ≤ γ)
(hγβ : β < γ)
:
ProbabilityTheory.fDiv (ProbabilityTheory.statInfoFun β γ) μ ν = ↑(ProbabilityTheory.statInfo μ ν (Bool.boolMeasure (ENNReal.ofReal β) (ENNReal.ofReal γ))) + 2⁻¹ * (↑|β * (μ Set.univ).toReal - γ * (ν Set.univ).toReal| + ↑β * ↑(μ Set.univ).toReal - ↑γ * ↑(ν Set.univ).toReal)
theorem
ProbabilityTheory.fDiv_statInfoFun_eq_StatInfo_of_nonneg
{𝒳 : Type u_1}
{m𝒳 : MeasurableSpace 𝒳}
{μ : MeasureTheory.Measure 𝒳}
{ν : MeasureTheory.Measure 𝒳}
{β : ℝ}
{γ : ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hβ : 0 ≤ β)
(hγ : 0 ≤ γ)
:
ProbabilityTheory.fDiv (ProbabilityTheory.statInfoFun β γ) μ ν = ↑(ProbabilityTheory.statInfo μ ν (Bool.boolMeasure (ENNReal.ofReal β) (ENNReal.ofReal γ))) + 2⁻¹ * (↑|β * (μ Set.univ).toReal - γ * (ν Set.univ).toReal| + (if γ ≤ β then -1 else 1) * (↑β * ↑(μ Set.univ).toReal - ↑γ * ↑(ν Set.univ).toReal))
theorem
ProbabilityTheory.fDiv_statInfoFun_ne_top
{𝒳 : Type u_1}
{m𝒳 : MeasurableSpace 𝒳}
{μ : MeasureTheory.Measure 𝒳}
{ν : MeasureTheory.Measure 𝒳}
{β : ℝ}
{γ : ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
:
theorem
ProbabilityTheory.integral_statInfoFun_curvatureMeasure
{f : ℝ → ℝ}
{t : ℝ}
(hf_cvx : ConvexOn ℝ Set.univ f)
(hf_cont : Continuous f)
:
∫ (y : ℝ), ProbabilityTheory.statInfoFun 1 y t ∂ConvexOn.curvatureMeasure f = f t - f 1 - rightDeriv f 1 * (t - 1)
theorem
ProbabilityTheory.integral_statInfoFun_curvatureMeasure'
{f : ℝ → ℝ}
{t : ℝ}
(hf_cvx : ConvexOn ℝ Set.univ f)
(hf_cont : Continuous f)
(hf_one : f 1 = 0)
(hfderiv_one : rightDeriv f 1 = 0)
:
∫ (y : ℝ), ProbabilityTheory.statInfoFun 1 y t ∂ConvexOn.curvatureMeasure f = f t
theorem
ProbabilityTheory.lintegral_f_rnDeriv_eq_lintegralfDiv_statInfoFun_of_absolutelyContinuous
{𝒳 : Type u_1}
{m𝒳 : MeasurableSpace 𝒳}
{μ : MeasureTheory.Measure 𝒳}
{ν : MeasureTheory.Measure 𝒳}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hf_cvx : ConvexOn ℝ Set.univ f)
(hf_cont : Continuous f)
(hf_one : f 1 = 0)
(hfderiv_one : rightDeriv f 1 = 0)
(h_ac : μ.AbsolutelyContinuous ν)
:
∫⁻ (x : 𝒳), ENNReal.ofReal (f (μ.rnDeriv ν x).toReal) ∂ν = ∫⁻ (x : ℝ), (ProbabilityTheory.fDiv (ProbabilityTheory.statInfoFun 1 x) μ ν).toENNReal ∂ConvexOn.curvatureMeasure f
theorem
ProbabilityTheory.fDiv_ne_top_iff_integrable_fDiv_statInfoFun_of_absolutelyContinuous'
{𝒳 : Type u_1}
{m𝒳 : MeasurableSpace 𝒳}
{μ : MeasureTheory.Measure 𝒳}
{ν : MeasureTheory.Measure 𝒳}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hf_cvx : ConvexOn ℝ Set.univ f)
(hf_cont : Continuous f)
(hf_one : f 1 = 0)
(hfderiv_one : rightDeriv f 1 = 0)
(h_ac : μ.AbsolutelyContinuous ν)
:
ProbabilityTheory.fDiv f μ ν ≠ ⊤ ↔ MeasureTheory.Integrable (fun (x : ℝ) => (ProbabilityTheory.fDiv (ProbabilityTheory.statInfoFun 1 x) μ ν).toReal)
(ConvexOn.curvatureMeasure f)
theorem
ProbabilityTheory.fDiv_ne_top_iff_integrable_fDiv_statInfoFun_of_absolutelyContinuous
{𝒳 : Type u_1}
{m𝒳 : MeasurableSpace 𝒳}
{μ : MeasureTheory.Measure 𝒳}
{ν : MeasureTheory.Measure 𝒳}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hf_cvx : ConvexOn ℝ Set.univ f)
(hf_cont : Continuous f)
(h_ac : μ.AbsolutelyContinuous ν)
:
ProbabilityTheory.fDiv f μ ν ≠ ⊤ ↔ MeasureTheory.Integrable (fun (x : ℝ) => (ProbabilityTheory.fDiv (ProbabilityTheory.statInfoFun 1 x) μ ν).toReal)
(ConvexOn.curvatureMeasure f)
theorem
ProbabilityTheory.integrable_f_rnDeriv_iff_integrable_fDiv_statInfoFun_of_absolutelyContinuous
{𝒳 : Type u_1}
{m𝒳 : MeasurableSpace 𝒳}
{μ : MeasureTheory.Measure 𝒳}
{ν : MeasureTheory.Measure 𝒳}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hf_cvx : ConvexOn ℝ Set.univ f)
(hf_cont : Continuous f)
(h_ac : μ.AbsolutelyContinuous ν)
:
MeasureTheory.Integrable (fun (x : 𝒳) => f (μ.rnDeriv ν x).toReal) ν ↔ MeasureTheory.Integrable (fun (x : ℝ) => (ProbabilityTheory.fDiv (ProbabilityTheory.statInfoFun 1 x) μ ν).toReal)
(ConvexOn.curvatureMeasure f)
theorem
ProbabilityTheory.fDiv_eq_integral_fDiv_statInfoFun_of_absolutelyContinuous'
{𝒳 : Type u_1}
{m𝒳 : MeasurableSpace 𝒳}
{μ : MeasureTheory.Measure 𝒳}
{ν : MeasureTheory.Measure 𝒳}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hf_cvx : ConvexOn ℝ Set.univ f)
(hf_cont : Continuous f)
(hf_one : f 1 = 0)
(hfderiv_one : rightDeriv f 1 = 0)
(h_int : MeasureTheory.Integrable (fun (x : 𝒳) => f (μ.rnDeriv ν x).toReal) ν)
(h_ac : μ.AbsolutelyContinuous ν)
:
ProbabilityTheory.fDiv f μ ν = ↑(∫ (x : ℝ), (ProbabilityTheory.fDiv (ProbabilityTheory.statInfoFun 1 x) μ ν).toReal ∂ConvexOn.curvatureMeasure f)
theorem
ProbabilityTheory.fDiv_eq_integral_fDiv_statInfoFun_of_absolutelyContinuous
{𝒳 : Type u_1}
{m𝒳 : MeasurableSpace 𝒳}
{μ : MeasureTheory.Measure 𝒳}
{ν : MeasureTheory.Measure 𝒳}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hf_cvx : ConvexOn ℝ Set.univ f)
(hf_cont : Continuous f)
(h_int : MeasureTheory.Integrable (fun (x : 𝒳) => f (μ.rnDeriv ν x).toReal) ν)
(h_ac : μ.AbsolutelyContinuous ν)
:
ProbabilityTheory.fDiv f μ ν = ↑(∫ (x : ℝ), (ProbabilityTheory.fDiv (ProbabilityTheory.statInfoFun 1 x) μ ν).toReal ∂ConvexOn.curvatureMeasure f) + ↑(f 1) * ↑(ν Set.univ) + ↑(rightDeriv f 1) * (↑(μ Set.univ) - ↑(ν Set.univ))
theorem
ProbabilityTheory.fDiv_eq_lintegral_fDiv_statInfoFun_of_absolutelyContinuous
{𝒳 : Type u_1}
{m𝒳 : MeasurableSpace 𝒳}
{μ : MeasureTheory.Measure 𝒳}
{ν : MeasureTheory.Measure 𝒳}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hf_cvx : ConvexOn ℝ Set.univ f)
(hf_cont : Continuous f)
(h_ac : μ.AbsolutelyContinuous ν)
:
ProbabilityTheory.fDiv f μ ν = ↑(∫⁻ (x : ℝ),
(ProbabilityTheory.fDiv (ProbabilityTheory.statInfoFun 1 x) μ ν).toENNReal ∂ConvexOn.curvatureMeasure f) + ↑(f 1) * ↑(ν Set.univ) + ↑(rightDeriv f 1) * (↑(μ Set.univ) - ↑(ν Set.univ))
theorem
ProbabilityTheory.lintegral_statInfoFun_one_zero
{f : ℝ → ℝ}
(hf_cvx : ConvexOn ℝ Set.univ f)
(hf_cont : Continuous f)
:
↑(∫⁻ (x : ℝ), ENNReal.ofReal (ProbabilityTheory.statInfoFun 1 x 0) ∂ConvexOn.curvatureMeasure f) = ↑(f 0) - ↑(f 1) + ↑(rightDeriv f 1)
theorem
ProbabilityTheory.fDiv_eq_lintegral_fDiv_statInfoFun_of_mutuallySingular
{𝒳 : Type u_1}
{m𝒳 : MeasurableSpace 𝒳}
{μ : MeasureTheory.Measure 𝒳}
{ν : MeasureTheory.Measure 𝒳}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hf_cvx : ConvexOn ℝ Set.univ f)
(hf_cont : Continuous f)
(h_ms : μ.MutuallySingular ν)
:
ProbabilityTheory.fDiv f μ ν = ↑(∫⁻ (x : ℝ),
(ProbabilityTheory.fDiv (ProbabilityTheory.statInfoFun 1 x) μ ν).toENNReal ∂ConvexOn.curvatureMeasure f) + ↑(f 1) * ↑(ν Set.univ) + ↑(rightDeriv f 1) * (↑(μ Set.univ) - ↑(ν Set.univ))
theorem
ProbabilityTheory.fDiv_eq_lintegral_fDiv_statInfoFun
{𝒳 : Type u_1}
{m𝒳 : MeasurableSpace 𝒳}
{μ : MeasureTheory.Measure 𝒳}
{ν : MeasureTheory.Measure 𝒳}
{f : ℝ → ℝ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure ν]
(hf_cvx : ConvexOn ℝ Set.univ f)
(hf_cont : Continuous f)
:
ProbabilityTheory.fDiv f μ ν = ↑(∫⁻ (x : ℝ),
(ProbabilityTheory.fDiv (ProbabilityTheory.statInfoFun 1 x) μ ν).toENNReal ∂ConvexOn.curvatureMeasure f) + ↑(f 1) * ↑(ν Set.univ) + ↑(rightDeriv f 1) * (↑(μ Set.univ) - ↑(ν Set.univ))