TwoLaneCoverTransport

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

Lane-separated observation-scale cover transport

This module transports the two-term homogenization-error clause from the cutoff cube to a larger observation cube without merging the two Orlicz lanes.

The grid concentration display of ABK26 is printed with two separate lanes,

O_{Gamma_1}(E^2 gamma 3^{-d(m-n)/2}) + O_{Gamma_{1/4}}(exp(-E^{-3} gamma^{-1}) 3^{-d(m-n)/2}),

and it is obtained by citing e.new.induction.for.shom at the mixed scale pair (coefficient cutoff L, observed cube n). Those two printed lanes are the squares of the two lanes (Gamma_2, Gamma_{1/2}) of the preceding-error clause, at the squared amplitudes: the per-site producers square the mixed-scale error once, lane by lane, through e.powerofGammasigma. Consequently the printed separation survives only if the transport from the cutoff cube to the observation cube is itself performed lane by lane, in the (Gamma_2, Gamma_{1/2}) form.

The proved transport observationScaleFiniteCover_sq_isBigOWith_gammaQuarter squares the error before transporting it and therefore delivers a single Gamma_{1/4} envelope at the merged amplitude A ^ 2 + B ^ 2, which is what the fourth moment of the corrected Step 4 needs but which cannot be reopened into the two printed lanes. This module produces the lane-separated form instead: same mechanism, run once per lane.

Route

The mechanism is the proved one, run once per lane instead of once on the merged square.

1. The two lanes at the cutoff scale. The clause is a two-term relation, so it comes with measurable witnesses Y and Z and a pointwise domination mathcal E <= Y + Z, with Y in Gamma_2(A) and Z in Gamma_{1/2}(B). Translation covariance of the cutoff sample law gives the same witnesses, with the same two amplitudes, at every translated scale-L cell of the observation cube.

2. The deterministic finite cover. The squared raw error of the observation cube square_m splits, at every sample point, into the m - L coarse layers -- each dominated by a maximum over that layer's parents of the average over their scale-L descendants -- and a geometrically damped fine tail dominated by the maximum over all scale-L descendants. Every step is monotone in the cell family, and the two maxima are subadditive, so the cover of the cell squares by 2 max(0,Y)^2 + 2 max(0,Z)^2 splits the whole deterministic bound into one cover functional per lane (laneTotal).

3. The probabilistic aggregation, at each lane's own exponent. The square rule e.powerofGammasigma sends the Gamma_2 lane to Gamma_1 and the Gamma_{1/2} lane to Gamma_{1/4}, at the squared amplitudes. The cover functional of a family with a common Gamma_sigma scale K is then Gamma_sigma at C(d, sigma) K: the descendant average is free (isBigO_finsetAverage_of_isBigO_gammaSigma_aemeasurable), each layer maximum costs (3 max(1, log N))^{1/sigma} (l.maximums.Gamma.s), which the geometric weight 3^{-ell/4} absorbs, and the layers are summed by the countable triangle inequality l.Gamma.sigma.triangle, whose strict positivity premise is met by the strictly positive geometric majorant laneDepthScale. This is run at sigma = 1 and at sigma = 1/4.

4. The square root. Each lane's cover functional is a square: sqrt of the Gamma_1 lane is Gamma_2 at sqrt(2 C_1) A and sqrt of the Gamma_{1/4} lane is Gamma_{1/2} at sqrt(2 C_{1/4}) B, by the same power rule read backwards. The observation-cube error is nonnegative and its square is at most the sum of the two lane functionals, hence at most the sum of the two square roots: the two-term relation of the printed display.

No comparator change occurs anywhere: the coefficient cutoff is a_L and the normalizer is sigmabar_L at the cell scale, at every intermediate scale, and at the observation cube. The only scale comparison is the half-discount one already used by the proved transport: the clause is read at the window s = 1/16 and the observation-cube error is produced at the discount 1/8.

The construction is spread over three modules that are one development. The deterministic cover of step 2 is Provider/Homogenization/TwoLaneCoverDepth.lean; the layer scales and the dimension-only constant laneCoverConst used by step 3 are Provider/Homogenization/TwoLaneCoverConstant.lean; this module carries steps 1, 3 and 4 and the endpoint.

References

• ABK26, proof of p.homogenization.step; the printed lane separation is the two-line display, cited there from e.new.induction.for.shom and p.concentration, for L <= n <= m - 1.
• ABK26, l.Gamma.sigma.triangle; l.maximums.Gamma.s; e.powerofGammasigma (inside l.o.gamma2.mult); the Appendix tail conventions.
• Here that cover is run at a general exponent, where the maximum costs (3 max(1, log N))^{1/sigma}.

The cover functional of one lane, at that lane's own exponent

The two lanes of a single cell

The endpoint

theorem Algsuperdiff.Section3.Provider.Homogenization.exists_twoLaneObservationScaleTransport (d : ℕ) : ∃ (Ctwo : ℝ), 1 ≤ Ctwo ∧ ∀ (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }), (∀ k ≤ m - 1, ∀ (s : ℝ) (hsWindow : s ∈ Set.Icc (8 * M.gamma) 1), Probability.IsTwoTermBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (Observable.cutoffHomogenizationError M k ⟨s, ⋯⟩) (↑E * s⁻¹ * √M.gamma) (s⁻¹ ^ 2 * Real.exp (-((↑E)⁻¹ ^ 3 * M.gamma⁻¹)))) → 1 / 16 ∈ Set.Icc (8 * M.gamma) 1 → ∀ (L n : ℤ), L ≤ m - 1 → L ≤ n → Probability.IsTwoTermBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (Observable.cutoffHomogenizationErrorRepresentative M L n (1 / 8) (Annealed.sigmaBar M L)) (Ctwo * (↑E * (1 / 16)⁻¹ * √M.gamma)) (Ctwo * ((1 / 16)⁻¹ ^ 2 * Real.exp (-((↑E)⁻¹ ^ 3 * M.gamma⁻¹))))

Lane-separated observation-scale transport of the preceding-error clause.

From the preceding-error clause at the induction scale m, read at the single window 1/16, the mixed-scale homogenization error at coefficient cutoff L and observation cube n obeys a two-term (Gamma_2, Gamma_{1/2}) bound with the same two lanes and the two amplitudes of the clause, inflated only by one dimension-only constant. The constant is chosen before the model, the induction scale, the amplitude parameter and the two scales.

This is a Provider endpoint: it carries no source-node status by itself.