UpperOrdinaryBlockProfile

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

The source-indexed ordinary upper block profile

This file proves a local deterministic profile result used by the conditional A in UpperCommonEnvelopeAE.lean. At descendant depth k, the source gap is

m - n = k + 1.

For the adopted deep-band mean split, a future analytic producer must establish the following target per-cube scale for the centred ordinary part of the corrected b_L estimate:

C * cstar⁻¹ * gamma * (k + 1) * 3^(gamma * (k + 1)).

The joint spatial-and-depth maximum contributes one further factor triadicJointDepthEntropyConst d * (k + 1). The resulting expression is exactly upperPolyProfile with head constant

triadicJointDepthEntropyConst d * C * cstar⁻¹ * gamma * 3^gamma.

On the standing range gamma ≤ 1, the harmless factor 3^gamma is at most 3. A second head constant below therefore has exactly the final parameter dependence C(d) * cstar⁻¹ * gamma.

This is only deterministic source-index arithmetic. It does not define the centred per-cube random observable, prove its marginal Gamma_1 estimate, or claim the Step-3 b_L assembly. Those are analytic producer obligations.

Source

• ABK26, p.bfA.multiscalebound, read at L = m, followed by the descendant maximum.
• cstar⁻¹ remains explicit, and the E⁻² deep-band mean must not be discarded. The split adopted here assigns it to the target deterministic shift; an analytic producer must still construct the centred ordinary lane and establish the target scale described here.

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.upperOrdinaryPerCubeAmplitude (C cstar gamma : ℝ) (k : ℕ) : ℝ

The target centred ordinary Gamma_1 scale that an analytic producer must establish for one descendant block at depth k.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.upperOrdinaryPerCubeAmplitude C cstar gamma k = C * cstar⁻¹ * gamma * (↑k + 1) * 3 ^ (gamma * (↑k + 1))

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.upperOrdinaryJointProfileConst (d : ℕ) (C cstar gamma : ℝ) : ℝ

The head constant obtained after paying jointly for the triadic spatial row and for all depths.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.upperOrdinaryJointProfileBound (d : ℕ) (C cstar gamma : ℝ) : ℝ

A dimensionally enlarged profile head with the final parameter dependence C(d) * cstar⁻¹ * gamma, valid on the standing range gamma ≤ 1.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upperOrdinaryJointProfileBound_nonneg (d : ℕ) {C cstar gamma : ℝ} (hC : 0 ≤ C) (hcstar : 0 ≤ cstar⁻¹) (hgamma : 0 ≤ gamma) : 0 ≤ upperOrdinaryJointProfileBound d C cstar gamma

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upperOrdinaryJointProfileConst_le_bound (d : ℕ) {C cstar gamma : ℝ} (hC : 0 ≤ C) (hcstar : 0 ≤ cstar⁻¹) (hgamma : 0 ≤ gamma) (hgamma1 : gamma ≤ 1) : upperOrdinaryJointProfileConst d C cstar gamma ≤ upperOrdinaryJointProfileBound d C cstar gamma

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.triadicJointDepthEntropyConst_mul_upperOrdinaryPerCubeAmplitude_eq (d : ℕ) (C cstar gamma : ℝ) (k : ℕ) : triadicJointDepthEntropyConst d * (↑k + 1) * upperOrdinaryPerCubeAmplitude C cstar gamma k = upperPolyProfile (upperOrdinaryJointProfileConst d C cstar gamma) gamma k

The joint maximum's deterministic row price is exactly the quadratic upper profile. This is the hprofile argument required by exists_ae_isBigOWith_gammaSigma_one_gridSupAbs_aggregate_majorant at the source ordinary per-cube amplitude.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.triadicJointDepthEntropyConst_mul_upperOrdinaryPerCubeAmplitude_le_bound (d : ℕ) {C cstar gamma : ℝ} (hC : 0 ≤ C) (hcstar : 0 ≤ cstar⁻¹) (hgamma : 0 ≤ gamma) (hgamma1 : gamma ≤ 1) (k : ℕ) : triadicJointDepthEntropyConst d * (↑k + 1) * upperOrdinaryPerCubeAmplitude C cstar gamma k ≤ upperPolyProfile (upperOrdinaryJointProfileBound d C cstar gamma) gamma k

The profile comparison with the harmless 3^gamma factor absorbed into a dimension-only head. Its assumptions are sign data and the standing small-gamma range only.