Documentation

LeanPool.HighContrastHomogenization.Support.Probability.IndependentSums.Rosenthal.BennettFunction

Coarse-graining support: Support.Probability.IndependentSums.Rosenthal.BennettFunction #

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

noncomputable def HCPolySupport.IndependentSums.bennettH (r : ℝ) :

The Bennett function h(r) = (1 + r) log (1 + r) - r.

Equations

HCPolySupport.IndependentSums.bennettH r = (1 + r) * Real.log (1 + r) - r

Instances For

noncomputable def HCPolySupport.IndependentSums.bennettBeta (r : ℝ) :

The Bennett quotient β(r) = h(r) / r on (0, ∞).

Equations

HCPolySupport.IndependentSums.bennettBeta r = HCPolySupport.IndependentSums.bennettH r / r

Instances For

noncomputable def HCPolySupport.IndependentSums.bennettLargeScaleThreshold :

An explicit universal threshold for the large-scale Bennett lower bound.

Equations

HCPolySupport.IndependentSums.bennettLargeScaleThreshold = Real.exp 4

Instances For

@[simp]

theorem HCPolySupport.IndependentSums.bennettH_zero :

theorem HCPolySupport.IndependentSums.hasDerivAt_bennettH {r : ℝ} (hr : r ≠ -1) :

HasDerivAt bennettH (Real.log (1 + r)) r

theorem HCPolySupport.IndependentSums.differentiableAt_bennettH {r : ℝ} (hr : r ≠ -1) :

DifferentiableAt ℝ bennettH r

theorem HCPolySupport.IndependentSums.deriv_bennettH {r : ℝ} (hr : r ≠ -1) :

deriv bennettH r = Real.log (1 + r)

theorem HCPolySupport.IndependentSums.differentiableOn_bennettH :

DifferentiableOn ℝ bennettH (Set.Ioi (-1))

theorem HCPolySupport.IndependentSums.deriv2_bennettH {r : ℝ} (hr : r ≠ -1) :

deriv ^[2] bennettH r = (1 + r)⁻¹

theorem HCPolySupport.IndependentSums.bennettBeta_eq_slope_mul_log_sub_one {r : ℝ} (hr : r ≠ 0) :

bennettBeta r = slope (fun (x : ℝ) => x * Real.log x) 1 (1 + r) - 1

theorem HCPolySupport.IndependentSums.monotoneOn_bennettBeta :

MonotoneOn bennettBeta (Set.Ioi 0)

theorem HCPolySupport.IndependentSums.bennettBeta_nonneg {r : ℝ} (hr : 0 < r) :

0 ≤ bennettBeta r

theorem HCPolySupport.IndependentSums.bennettH_nonneg {r : ℝ} (hr : 0 ≤ r) :

0 ≤ bennettH r

theorem HCPolySupport.IndependentSums.one_quarter_sq_le_bennettH_of_mem_Icc {r : ℝ} (hr : r ∈ Set.Icc 0 1) :

r ^ 2 / 4 ≤ bennettH r

theorem HCPolySupport.IndependentSums.log_sub_one_le_bennettBeta {r : ℝ} (hr : 0 < r) :

Real.log r - 1 ≤ bennettBeta r

theorem HCPolySupport.IndependentSums.two_le_bennettLargeScaleThreshold :

2 ≤ bennettLargeScaleThreshold

theorem HCPolySupport.IndependentSums.three_quarters_log_le_bennettBeta_of_bennettLargeScaleThreshold_le {r : ℝ} (hr : bennettLargeScaleThreshold ≤ r) :

3 / 4 * Real.log r ≤ bennettBeta r

theorem HCPolySupport.IndependentSums.exists_bennettBeta_ge_three_quarters_log :

∃ r0 ∈ Set.Ici 2, ∀ {r : ℝ}, r0 ≤ r → 3 / 4 * Real.log r ≤ bennettBeta r