StepBoundaryAbsorption

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

1. The print's t e^t ≤ e^{2t}

theorem Algsuperdiff.Section4.Provider.Regularity.mul_exp_le_exp_two_mul {a : ℝ} (ha : 0 ≤ a) : a * Real.exp a ≤ Real.exp (2 * a)

t e^t ≤ e^{2t} for t ≥ 0 -- the print's absorption of a polynomial prefactor into its own exponential. The only input is x ≤ x + 1 ≤ e^x.

theorem Algsuperdiff.Section4.Provider.Regularity.rpow_three_eq_exp (x : ℝ) : Real.rpow 3 x = Real.exp (Real.log 3 * x)

3^x = exp((log 3) x); the single place rpow and exp meet in this module.

theorem Algsuperdiff.Section4.Provider.Regularity.mul_rpow_three_quarter_le (t : ℝ) (ht : 0 ≤ t) : t * Real.rpow 3 (1 / 4 * t) ≤ 4 / Real.log 3 * Real.rpow 3 (1 / 2 * t)

The absorption in 3-powers: for every t ≥ 0,

   t · 3^{(1/4) t}  ≤  (4 / log 3) · 3^{(1/2) t} .

2. The ε-funded flat leg: the print's absorption, α-free

theorem Algsuperdiff.Section4.Provider.Regularity.stepSixFlat_epsFunded_absorb {C1 Citer t S H : ℝ} {k : ℕ} (hC1 : 0 < C1) (hCiter : 0 ≤ Citer) (ht : 0 ≤ t) (hS0 : 0 ≤ S) (hH : 0 ≤ H) (hfloor : 4 * Citer * (↑k + 1) / Real.log 3 ≤ C1) (hS : S ≤ 2 * (C1⁻¹ * t)) : Real.exp (C1⁻¹ * Citer * t) * (S * H) ≤ 8 / (C1 * Real.log 3) * Real.rpow 3 (1 / 2 * t) * H

The printed absorption, at the abstract reals.

If the flat ∇h leg enters the δ-budget multiplied by the ε-sum -- i.e. with the coefficient S ≤ 2 C₁^{-1} t, which e.sum.eps.j.bound supplies with t = (1-α)(m-n) -- then

   exp( C₁^{-1} C_iter t ) · S · H  ≤  (8 / (C₁ log 3)) · 3^{(1/2) t} · H .

The constant carries NO α, NO γ and NO δ: the coefficient IS the exponent's own argument, which is precisely why the print's t e^t ≤ e^{2t} step is free.