WaveBandMean

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

The k₀-deep wave band: its deterministic mean, and the absorption arithmetic

The mathematical situation, exactly

corrects the ordinary upper-wave scale of e.bL.multiscale to C (gamma (L - n) + E⁻²) 3^{2 gamma (L-n) - gamma (m-n)}. The extra E⁻² summand cannot be discarded, and it cannot be absorbed into the printed gamma-lane either: absorbing it would force E³ ≤ C₁ - 1 at the admissible tuning gamma = E⁻⁵, with E unbounded. What it can be charged to is the deterministic part of the display. On the k₀-deep band the extra content is therefore split into

• a deterministic mean --- a number, by stationarity, since the gauge sigmaBar is deterministic --- of normalized size D_band = A sqrt(gamma k₀) 3^{gamma k₀} at a C(d) amplitude A; and
• a centred remainder of pure-gamma amplitude, which stays in the ordinary lane.

The mean is not a lane at all. It is a deterministic shift, and a deterministic shift is exactly what the frozen upper display already carries: the Ccg slot of Probability.IsDeterministicShiftTwoTermOneSidedOrlicz. So the resolution is not that the E⁻² content vanishes --- the obstruction above forbids that --- but that it hides in Ccg.

What is proved here

• waveBandDepth, waveBandDepth_spec --- the tuned band depth k₀ = ⌈c E⁻² gamma⁻¹⌉₊ and the only property it is used through: gamma k₀ ≤ c E⁻² + gamma, the integer ceiling costing at most one gamma.
• waveBandMean, waveBandMean_sq_le --- the normalized deterministic band mean and its square, D_band² ≤ A² (c E⁻² + gamma) 3^{2 gamma k₀}, i.e. exactly C (E⁻² + gamma)-class.
• mul_gamma_le_one_of_le_rpow_neg_fifth, gamma_le_one_of_le_rpow_neg_fifth --- the two consequences of the frozen admissibility gate E ≤ gamma^(-1/5) used below: E gamma ≤ 1 and gamma ≤ 1.
• cstarInv_bandBudget_le_two --- the absorption arithmetic. On the frozen window (1 ≤ E, cstar⁻¹ ≤ E from the threshold binder max (exp (Ccg/sigma)) cstar⁻¹ ≤ E, and E ≤ gamma^(-1/5)), cstar⁻¹ (c E⁻² + gamma) ≤ 2: the cstar-corrected band budget is dimension-free.
• cstarInv_mul_waveBandMean_sq_le --- the headline: the cstar-corrected squared band mean is bounded by the dimension-free waveBandConst, so it is absorbable into the deterministic shift.
• gamma_le_inv_pow_five --- the bridge that puts the frozen gate E ≤ gamma^(-1/5) into the algebraic tuning gamma ≤ E⁻⁵, which is the form in which the lane obstruction above is read, so that obstruction is a statement about this window and not about a hypothetical one.

References

• ABK26, p.cg.ellipticity.bounds, statement (e.cg.ellip.upper), proof; the Step-3 endpoint terms.

1. The tuned band depth

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.waveBandDepth (c E gamma : ℝ) : ℕ

The tuned depth of the deep wave band, k₀ = ⌈c E⁻² gamma⁻¹⌉₊ (; k₀ is a deterministic tuning parameter).

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.waveBandDepth c E gamma = ⌈c * (E ^ 2)⁻¹ * gamma⁻¹⌉₊

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.waveBandDepth_spec {c E gamma : ℝ} (hgamma : 0 < gamma) (ht : 0 ≤ c * (E ^ 2)⁻¹ * gamma⁻¹) : gamma * ↑(waveBandDepth c E gamma) ≤ c * (E ^ 2)⁻¹ + gamma

The only property of the tuned depth used downstream: the band's total gamma-weight is c E⁻² up to the one gamma charged by the integer ceiling.

2. The normalized deterministic band mean

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.waveBandMean (A gamma : ℝ) (k0 : ℕ) : ℝ

The normalized deterministic mean of the k₀-deep wave band, D_band = A sqrt(gamma) sqrt(k₀) 3^{gamma k₀}. It is a number, not a random variable: that is the whole content of the split.

The amplitude A is left as a parameter rather than fixed to a numeral: at the proved volume-normalized L^p carrier of this repository the head's amplitude is a genuine C(d, p) (see deepBandAmplitude in DeepBandSplit.lean), and the frozen constant Ccg is dimension-only, so a dimensional amplitude is exactly what the slot admits.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.waveBandMean A gamma k0 = A * √gamma * √↑k0 * 3 ^ (gamma * ↑k0)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.waveBandMean_nonneg {A : ℝ} (hA : 0 ≤ A) (gamma : ℝ) (k0 : ℕ) : 0 ≤ waveBandMean A gamma k0

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.waveBandMean_sq_le {A gamma B : ℝ} (hgamma : 0 ≤ gamma) (k0 : ℕ) (hgk : gamma * ↑k0 ≤ B) : waveBandMean A gamma k0 ^ 2 ≤ A ^ 2 * B * 3 ^ (2 * (gamma * ↑k0))

The squared band mean is A² (gamma k₀)-class, hence A² (c E⁻² + gamma)-class once the depth is tuned: D_band² = A² (gamma k₀) 3^{2 gamma k₀}.

3. The frozen admissibility gate, in algebraic form

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.mul_gamma_le_one_of_le_rpow_neg_fifth {E gamma : ℝ} (hE : 1 ≤ E) (hgamma : 0 < gamma) (hEgamma : E ≤ gamma ^ (-(1 / 5))) : E * gamma ≤ 1

The frozen gate E ≤ gamma^(-1/5) gives E gamma ≤ 1.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.gamma_le_one_of_le_rpow_neg_fifth {E gamma : ℝ} (hE : 1 ≤ E) (hgamma : 0 < gamma) (hEgamma : E ≤ gamma ^ (-(1 / 5))) : gamma ≤ 1

The frozen gate E ≤ gamma^(-1/5) gives gamma ≤ 1.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.gamma_le_inv_pow_five {E gamma : ℝ} (hE : 1 ≤ E) (hgamma : 0 < gamma) (hEgamma : E ≤ gamma ^ (-(1 / 5))) : gamma ≤ (E ^ 5)⁻¹

The frozen gate E ≤ gamma^(-1/5) is the algebraic tuning gamma ≤ E⁻⁵ that argue at.

4. The absorption arithmetic

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.cstarInv_bandBudget_le_two {c E gamma cstar : ℝ} (hc0 : 0 ≤ c) (hc1 : c ≤ 1) (hE : 1 ≤ E) (hgamma : 0 < gamma) (hcstarE : cstar⁻¹ ≤ E) (hEgamma : E ≤ gamma ^ (-(1 / 5))) : cstar⁻¹ * (c * (E ^ 2)⁻¹ + gamma) ≤ 2

The absorption arithmetic (with the cstar⁻¹ factor).

On the frozen window the cstar-corrected band budget is dimension-free: the threshold binder supplies cstar⁻¹ ≤ E, so cstar⁻¹ c E⁻² ≤ c E⁻¹ ≤ 1, and the gate E ≤ gamma^(-1/5) supplies cstar⁻¹ gamma ≤ E gamma ≤ 1. Positivity of cstar is not needed: the threshold binder already dominates cstar⁻¹.

def Algsuperdiff.Section3.Provider.CoarseEllipticity.waveBandConst (A : ℝ) : ℝ

The budget of the squared deep-band deterministic mean at amplitude A. No model parameter enters: cstar, E, gamma and s have all been paid.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.waveBandConst A = A ^ 2 * 2 * 81

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.waveBandConst_nonneg (A : ℝ) : 0 ≤ waveBandConst A

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.cstarInv_mul_waveBandMean_sq_le {A c E gamma cstar : ℝ} (hc0 : 0 ≤ c) (hc1 : c ≤ 1) (hE : 1 ≤ E) (hgamma : 0 < gamma) (hcstar : 0 < cstar) (hcstarE : cstar⁻¹ ≤ E) (hEgamma : E ≤ gamma ^ (-(1 / 5))) : cstar⁻¹ * waveBandMean A gamma (waveBandDepth c E gamma) ^ 2 ≤ waveBandConst A

The E⁻² content is absorbable as a deterministic shift.

On the frozen window the cstar-corrected squared mean of the k₀-deep wave band is bounded by the dimension-free numeral waveBandConst. Contrast the lane obstruction of the module header: the same content is not absorbable when read as a Gamma₁ amplitude against the gamma-lane.

5. The two-lane necessity, reproved