HomSpineFinalWitness

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

Theorem B, §4.5: two range transfers for the real defect witness

What this module is

The frozen root asks for a real-valued E_B: Ω → ℝ with

  0 ≤ E_B,   E_B measurable,
  ∫⁻ (ofReal E_B)^p ≤ ( C (√p + √|log γ|) √γ (log γ)² )^p
      for every p ∈ [1, C⁻¹ γ⁻¹ |log γ|⁻¹].

This repository's carrier EthmB(m) is [0,∞]-valued (HomStepEnvelope.ethmB), so the real cut needs EthmB < ∞ a.e., and the cut is then made at

  E_B(ω):= K · (EthmB(m)(ω)).toReal,

with K the Step-3/Step-4 absorption factor (the constant the manuscript "absorbs into EthmB(m)"), carried as a parameter and paid for in the constant C.

Two elementary transfers about the p-range are what that construction needs from this file, and they are all it contains:

• range_mono_of_le — a p-range stated at the larger constant is contained in the p-range stated at the smaller one, so the root's own range p ≤ C⁻¹γ⁻¹|log γ|⁻¹ implies every sub-range the chain reads;
• gamma_mul_absLog_le — γ|log γ| ≤ 4√γ on 0 < γ < 1, the only place a logarithm meets a power of γ here. It is spent exactly once, to put p = 1 inside the range, which is where the a.e. finiteness of the [0,∞] carrier comes from.

1. Two elementary transfers

theorem Algsuperdiff.Section4.Provider.Homogenization.range_mono_of_le {K C gam Lg p : ℝ} (hK : 0 < K) (hKC : K ≤ C) (hgam : 0 ≤ gam⁻¹) (hLg : 0 ≤ Lg⁻¹) (hp : p ≤ C⁻¹ * gam⁻¹ * Lg⁻¹) : p ≤ K⁻¹ * gam⁻¹ * Lg⁻¹

Shrinking a reciprocal range: a p-range stated at the larger constant is contained in the p-range stated at the smaller one.

theorem Algsuperdiff.Section4.Provider.Homogenization.gamma_mul_absLog_le {gamma : ℝ} (hg : 0 < gamma) (hg1 : gamma < 1) : gamma * |Real.log gamma| ≤ 4 * √gamma

γ|log γ| ≤ 4√γ on 0 < γ < 1: the absLog_mul_sqrt_le multiplied by √γ and collapsed with t³ ≤ t² at t = γ^{1/4} ≤ 1. This is the only place a logarithm meets a power of γ in this module; it is spent exactly once, to put p = 1 inside the theorem's own range.