SepEnvelope

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Logarithmic square-root estimates

This module contains the elementary real inequalities used to absorb the logarithmic factor in the deterministic separation envelope. The estimates reduce the calculation to -(t log t) ≤ 1 and then apply it at an eighth root.

Main results

• Algsuperdiff.Probability.neg_mul_log_le_one
• Algsuperdiff.Probability.gamma_quarter_log_sq_le
• Algsuperdiff.Probability.sqrt_mul_log_sq_le_quarter

References

• ABK26, l.minimal.scale.sep.

theorem Algsuperdiff.Probability.neg_mul_log_le_one {t : ℝ} (ht : 0 < t) : -(t * Real.log t) ≤ 1

-(t log t) ≤ 1 for every t > 0 (on (0,1] this is the useful half of |t log t| ≤ 1). Proof: t·(-log t) ≤ t·(t⁻¹ − 1) = 1 − t ≤ 1.

theorem Algsuperdiff.Probability.quarter_log_sq_aux {t : ℝ} (ht : 0 < t) (ht1 : t ≤ 1) : t * t * (8 * Real.log t) ^ 2 ≤ 64

The t = γ^{1/8} core of gamma_quarter_log_sq_le, over abstract reals: for t ∈ (0,1], t² · (8 log t)² = 64 (t log t)² ≤ 64.

theorem Algsuperdiff.Probability.gamma_quarter_log_sq_le {γ : ℝ} (hγ : 0 < γ) (hγ1 : γ ≤ 1) : γ ^ (1 / 4) * Real.log γ ^ 2 ≤ 64

The scale-free log bound. γ^{1/4} (log γ)² ≤ 64 for γ ∈ (0,1].

theorem Algsuperdiff.Probability.sqrt_eq_quarter_mul_quarter {γ : ℝ} (hγ : 0 < γ) : √γ = γ ^ (1 / 4) * γ ^ (1 / 4)

√γ = γ^{1/4} · γ^{1/4}.

theorem Algsuperdiff.Probability.sqrt_mul_log_sq_le_quarter {γ : ℝ} (hγ : 0 < γ) (hγ1 : γ ≤ 1) : √γ * Real.log γ ^ 2 ≤ 64 * γ ^ (1 / 4)

√γ (log γ)² ≤ 64 γ^{1/4} on (0,1].