MultiscaleComposition

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

Provider: the composition of the two scale branches of p.multiscale.estimate

What is delivered, and what is NOT

multiscale_estimate_composed is the frozen root's statement body (Frozen/Section3/MultiscaleEstimate.lean, the block between) verbatim, binder for binder and amplitude spelling for amplitude spelling, with NO premise inserted and nothing else changed: the same exists Cms, the same five source binders (M, m, E, the induction state, epsilon), the same window cstar^{-1} eps^{-Cms} <= E, the same smallness cgamma <= (E^{-1})^{10}, the same s in [8 cgamma, 1], ONE (Y, Z) pair serving the main conjunct AND the refinement clause, and the two amplitudes

    Cms E s^{-1} sqrt(eps cgamma)   and   Cms eps (s^{-1})^2 exp(-E^{-3} cgamma^{-1}) .

Until that licensed edit happens, p.multiscale.estimate is not a closed source node, and no docstring here may say otherwise.

The two inputs (consumed, never re-derived)

Both are proved publics of this namespace, each proving the frozen body on one side of the landmark mStarStar M:

• multiscale_estimate_of_mStarStar --- the frozen body with the single premise mStarStar M < m;
• multiscale_estimate_of_le_mStarStar --- the frozen body with the single premise m <= mStarStar M.

The composition is not a plain max

The obvious composition --- take Cms := max Cms_1 Cms_2 and transfer every hypothesis by monotonicity --- does not typecheck, because one hypothesis of the frozen body points the wrong way. The frozen conclusion's second conjunct is an implication

    s <= Cms eps  ->  IsBigOWith mu Gamma_2 Y (Cms eps E s^{-1} sqrt cgamma) ,

so the composed Cms occurs there in negative position: enlarging Cms W the guard we are handed and therefore weakens what the branch clause can be fed. The monotone transfer of the composed guard s <= Cms eps to the branch guard s <= Cms_i eps needs Cms <= Cms_i, while the window hypothesis cstar^{-1} eps^{-Cms} <= E and all three amplitudes need Cms_i <= Cms; the two are compatible only at Cms = Cms_1 = Cms_2. (That the branches' own proofs never consume their guards is irrelevant here: this module consumes their statements, in which the guard is an antecedent.)

Nor do the two routes below rescue the constant max Cms_1 Cms_2 itself. At Cms = max Cms_1 Cms_2, take the branch whose constant a satisfies Cms / 2 < a < Cms, and the regime a / 2 < s <= Cms eps. Feeding the branch at an enlarged parameter eps' (leaf 3) would need s <= a eps' with eps' <= 1/2, i.e. s <= a / 2, which that regime denies; and reading the refinement off the main amplitude (leaf 2) would need a <= Cms sqrt eps, i.e. eps >= (a / Cms)^2, while the regime gives only eps > a / (2 Cms), which is smaller than (a / Cms)^2 exactly when Cms < 2 a. Those two are the only sources of a Gamma_2 tail for Y that the branch statements expose, so the composed constant must exceed 2 a.

The branch window in fact admits any eps' >= eps^{Cms/a} (the window transfers whenever (eps')^{-a} <= eps^{-Cms}), and shrinking eps' makes the leaf-2 comparison easier. So the conclusion stands on the full route family. It is in any case immaterial to the theorem: the frozen statement is existential in Cms.

The route taken instead --- which weakens nothing, the frozen statement being existential in Cms --- is the constant

    Cms := 2 * max Cms_1 Cms_2

together with a three-leaf case analysis, run inside display_of_branch for whichever branch the scale m selects. Write a for that branch's constant, so 2 a <= Cms. Given the model datum and the frozen window at Cms:

1. No guard (Cms eps < s). Apply the branch at eps itself; the main conjunct transfers by amplitude monotonicity (a <= Cms), and the refinement clause is vacuous.
2. Guard, and a < 2 s. Apply the branch at eps. Here s <= Cms eps and a < 2 s force a < 2 Cms eps, whence a^2 <= Cms^2 eps (this is where 2 a <= Cms is spent) and so a sqrt eps <= Cms eps. The refinement is then read off the main conjunct's own Y-tail (the IsBigOWith at the first amplitude bundled in IsTwoTermBigOWithWitnesses), whose amplitude a E s^{-1} sqrt(eps cgamma) is at most the refinement target Cms eps E s^{-1} sqrt cgamma exactly by that inequality. No branch guard is needed.
3. Guard, and 2 s <= a. Apply the branch at the enlarged parameter eps' := max eps (s / a), which lies in (0, 1/2] precisely because 2 s <= a. Then a eps' = max (a eps) s <= Cms eps (using the guard), which drives all three amplitude comparisons, while s <= a eps' is the branch guard, available by le_max_right. Enlarging eps is legitimate in the window because eps |-> eps^{-a} is antitone: eps <= eps' gives (eps')^{-a} <= eps^{-a} <= eps^{-Cms}.

Leaf 2 is the only place where the composed constant must exceed max Cms_1 Cms_2, and 2 x is the cheapest factor that works: the argument needs (a / Cms)^2 <= a / (2 Cms), i.e. exactly 2 a <= Cms.

1. Amplitude arithmetic

Three real-variable lemmas, stated over abstract reals so that no square root, exponential or rpow is ever handed to a decision procedure.

2. The carrier-level transfer

The composition never rebuilds a witness pair: it keeps the branch's (Y, Z) and enlarges the three amplitudes. The refinement clause travels with it, and may be fed either by the branch's own clause or by the first amplitude's Y-tail, which IsTwoTermBigOWithWitnesses bundles.

3. The branch-to-composed transfer

One model datum at a time. hbranch is exactly what either proved branch delivers after its scale premise and the induction state have been supplied.

4. The composition

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.multiscale_estimate_composed (d : ℕ) : ∃ (Cms : ℝ), 0 < Cms ∧ ∀ (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M (m - 1) E → ∀ epsilon ∈ Set.Ioc 0 (1 / 2), (Disorder.cstar M)⁻¹ * epsilon ^ (-Cms) ≤ ↑E → M.gamma ≤ (↑E)⁻¹ ^ 10 → ∀ (s : ℝ) (hsWindow : s ∈ Set.Icc (8 * M.gamma) 1), ∃ (Y : Cutoff.CutoffSample d → ℝ) (Z : Cutoff.CutoffSample d → ℝ), Probability.IsTwoTermBigOWithWitnesses (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (Observable.cutoffHomogenizationError M m ⟨s, ⋯⟩) Y Z (Cms * ↑E * s⁻¹ * √(epsilon * M.gamma)) (Cms * epsilon * s⁻¹ ^ 2 * Real.exp (-((↑E)⁻¹ ^ 3 * M.gamma⁻¹))) ∧ (s ≤ Cms * epsilon → HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) Y (Cms * epsilon * ↑E * s⁻¹ * √M.gamma))

The frozen p.multiscale.estimate body, with no premise.

This is Algsuperdiff.Frozen.Section3.multiscale_estimate's statement body (the block between in Frozen/Section3/MultiscaleEstimate.lean) verbatim --- binder for binder and amplitude spelling for amplitude spelling --- under a different declaration name.

The proof is the tautological case split lt_or_ge (mStarStar M) m feeding the two proved branches, multiscale_estimate_of_mStarStar above the landmark and multiscale_estimate_of_le_mStarStar at or below it, through display_of_branch at the common constant 2 * max Cms₁ Cms₂. The doubling is forced by the refinement clause's guard, which occurs negatively; see the module header, "The composition is not a plain max".