StepSixHolderExponent

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

t.regularity Step 6: verifying the Hölder exponent

The target

The step converts the exponential prefactor of e.oscillation.iteration.result into a Hölder rate:

   choosing  C₁ ≥ 4 C (k+1) / log 3 ,
   exp( C₁⁻¹ C (1-α)(m-n) )  ≤  3^{(1/4)(1-α)(m-n)}

and then re-states e.oscillation.iteration.result as e.oscillation.Holder.bound:

   3^{-n'} ‖u - (u)_{U_{n'}}‖_{L²(U_{n'})}
     ≤ C 3^{(1/2)(1-α)(m-n)} · 3^{-m'} ‖u - (u)_{U_{m'}}‖_{L²(U_{m'})}
     + C 3^{(1/2)(1-α)(m-n)} · 3^{m/2} ( σ_m^{-1}[g]_{W^{1/2,∞}(□_m)}
                                        + ‖∇h‖_{W^{1/2,∞}(□_m)} 1_{z ∉ □_{m-1}} ) .

What "composed into the shape" means, exactly

  oscLo  := 3^{-n'} ‖u - (u)_{U_{n'}}‖_{L²(U_{n'})} ,
  oscHi  := 3^{-m'} ‖u - (u)_{U_{m'}}‖_{L²(U_{m'})} ,
  dataG  := 3^{m/2} σ_m^{-1} [g]_{W^{1/2,∞}(□_m)} ,
  dataH  := 3^{m/2} ‖∇h‖_{W^{1/2,∞}(□_m)} 1_{z ∉ □_{m-1}} ,

the inequality oscLo ≤ C e^P (oscHi + C dataG) + C e^P dataH, and e.oscillation.Holder.bound is oscLo ≤ C' 3^{t/2} oscHi + C' 3^{t/2} (dataG + dataH). The composition is therefore the prefactor replacement together with the distribution of the inner C; the produced constant is C' = C + C² (deviation D2 below), which is the honest cost of the manuscript writing one letter C in both places.

References

• ABK26, t.regularity Step 6, (e.oscillation.Holder.bound).
• ABK26, e.oscillation.iteration.result.

1. The abstract-real atoms near exp and log

theorem Algsuperdiff.Section4.Provider.Regularity.exp_le_rpow_three_of_le_mul_log {a t : ℝ} (h : a ≤ t * Real.log 3) : Real.exp a ≤ Real.rpow 3 t

exp a ≤ 3^t as soon as a ≤ t log 3. The only place exp and rpow meet in this module; everything else is scalar arithmetic on Real.log 3, which is kept opaque (only its positivity is used).

theorem Algsuperdiff.Section4.Provider.Regularity.stepSixRatio_le_of_floor {C1 Citer : ℝ} {k : ℕ} (hC1 : 0 < C1) (hCiter : 0 ≤ Citer) (hfloor : 4 * Citer * (↑k + 1) / Real.log 3 ≤ C1) : C1⁻¹ * Citer ≤ Real.log 3 / 4

The Step-6 floor, in ratio form. C₁ ≥ 4 C_iter (k+1)/log 3 gives C₁⁻¹ C_iter ≤ (log 3)/4, which is the whole content of the step's displayed computation. The (k+1) factor is pure slack for THIS display (it is what Step 5 needs when it absorbs exp(C(k + |𝓑|))); it is kept verbatim.

2. The step's own computation: the sharp 1/4

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

   exp( C₁⁻¹ C_iter t )  ≤  3^{(1/4) t}          for every  t ≥ 0 .

Here t is the source's (1-α)(m-n); the statement is uniform in t ≥ 0. This is the sharp form.

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

3^{(1/4)t} ≤ 3^{(1/2)t} for t ≥ 0 — the exact slack measures between Step 6's own computation and the exponent e.oscillation.Holder.bound is printed at.

def Algsuperdiff.Section4.Provider.Regularity.stepSixExponent (alpha : ℝ) (n m : ℤ) : ℝ

The Step-6 exponent argument t := (1-α)(m-n).

Equations

• Algsuperdiff.Section4.Provider.Regularity.stepSixExponent alpha n m = (1 - alpha) * (↑m - ↑n)

theorem Algsuperdiff.Section4.Provider.Regularity.stepSixExponent_nonneg {alpha : ℝ} {n m : ℤ} (halpha : alpha ≤ 1) (hnm : n ≤ m) : 0 ≤ stepSixExponent alpha n m

0 ≤ (1-α)(m-n) in the Step-1/Step-3 regime (α ≤ 1, n ≤ m).

theorem Algsuperdiff.Section4.Provider.Regularity.exp_stepOneC1_le_rpow_three_quarter (d : ℕ) {Cedos Cann Citer alpha : ℝ} {k : ℕ} {n m : ℤ} (hCiter : 0 ≤ Citer) (halpha : alpha ≤ 1) (hnm : n ≤ m) : Real.exp ((stepOneC1 d Cedos Cann Citer k)⁻¹ * Citer * stepSixExponent alpha n m) ≤ Real.rpow 3 (1 / 4 * stepSixExponent alpha n m)

Step 6 at the Step-1 C₁, sharp: the floor is discharged by step6_le_stepOneC1, so no largeness hypothesis is carried.

theorem Algsuperdiff.Section4.Provider.Regularity.exp_stepOneC1_le_rpow_three_half (d : ℕ) {Cedos Cann Citer alpha : ℝ} {k : ℕ} {n m : ℤ} (hCiter : 0 ≤ Citer) (halpha : alpha ≤ 1) (hnm : n ≤ m) : Real.exp ((stepOneC1 d Cedos Cann Citer k)⁻¹ * Citer * stepSixExponent alpha n m) ≤ Real.rpow 3 (1 / 2 * stepSixExponent alpha n m)

4. The composition into e.oscillation.Holder.bound's shape

theorem Algsuperdiff.Section4.Provider.Regularity.holderBound_of_iterationResult {C P t oscLo oscHi dataG dataH : ℝ} (hC : 0 ≤ C) (hoscHi : 0 ≤ oscHi) (hdataG : 0 ≤ dataG) (hdataH : 0 ≤ dataH) (hP : Real.exp P ≤ Real.rpow 3 t) (hiter : oscLo ≤ C * Real.exp P * (oscHi + C * dataG) + C * Real.exp P * dataH) : oscLo ≤ (C + C * C) * Real.rpow 3 t * oscHi + (C + C * C) * Real.rpow 3 t * (dataG + dataH)

e.oscillation.Holder.bound from e.oscillation.iteration.result, as printed: the exponential prefactor is replaced by 3^{(1/2)(1-α)(m-n)} and the inner constant is distributed.

oscLo, oscHi, dataG, dataH are the four real quantities named in the module docstring. The produced constant is C + C² (deviation D2).

theorem Algsuperdiff.Section4.Provider.Regularity.oscillationHolderBound_of_iterationResult (d : ℕ) {Cedos Cann Citer C alpha : ℝ} {k : ℕ} {n m : ℤ} {oscLo oscHi dataG dataH : ℝ} (hC : 0 ≤ C) (hCiter : 0 ≤ Citer) (halpha : alpha ≤ 1) (hnm : n ≤ m) (hoscHi : 0 ≤ oscHi) (hdataG : 0 ≤ dataG) (hdataH : 0 ≤ dataH) (hiter : oscLo ≤ C * Real.exp ((stepOneC1 d Cedos Cann Citer k)⁻¹ * Citer * stepSixExponent alpha n m) * (oscHi + C * dataG) + C * Real.exp ((stepOneC1 d Cedos Cann Citer k)⁻¹ * Citer * stepSixExponent alpha n m) * dataH) : oscLo ≤ (C + C * C) * Real.rpow 3 (1 / 2 * stepSixExponent alpha n m) * oscHi + (C + C * C) * Real.rpow 3 (1 / 2 * stepSixExponent alpha n m) * (dataG + dataH)

t.regularity Step 6, assembled at the Step-1 C₁ — the printed exponent.

From e.oscillation.iteration.result at the prefactor C exp(C₁⁻¹ C_iter (1-α)(m-n)), Step 6 delivers e.oscillation.Holder.bound at 3^{(1/2)(1-α)(m-n)}. The floor is discharged inside (step6_le_stepOneC1), so the only hypotheses are the regime (α ≤ 1, n ≤ m), the constants' signs, and the three nonnegativity facts of the transported quantities.