TailAssembly

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

p.tail.bounds from p.cg.ellipticity.bounds

This module formalizes the conditional derivation of Proposition p.tail.bounds (statement) from Proposition p.cg.ellipticity.bounds (statement) through Lemma l.mathcal.E.to.Lambdas, printed:

l.mathcal.E.to.Lambdas asserts `E_{s,inf,2}(cu_m; a_m, sig_{m-1})^2 <= 2 sig_{m-1}^{-1} Lambda_{s,2}(cu_m;a_m)

• 2 sig_{m-1} lambda_{s,2}^{-1}(cu_m;a_m)and thereforee.cg.ellip.lowerande.cg.ellip.upperimply `E^2 <= C s (2s-g)^{-1} + O_{Gamma_1}(C s g (2s-g)^{-3})
• O_{Gamma_{(1-sig)/3}}(exp(-C^{-1}E^{-2}g^{-1})). Taking square roots, and specializing to sig = 1/4ands >= 4g, we get e.tail.bounds`.

The provider tail_bounds_of_coarse_ellipticity_bounds takes the exact p.cg.ellipticity.bounds proposition as an explicit analytic A input and returns the exact p.tail.bounds proposition. The proved frozen export Algsuperdiff/Frozen/Section3/TailBounds.lean is by the application

exact Algsuperdiff.Section3.Provider.Tail.tail_bounds_of_coarse_ellipticity_bounds d
  (Algsuperdiff.Frozen.Section3.coarse_ellipticity_bounds d)

The dependency Algsuperdiff.Frozen.Section3.coarse_ellipticity_bounds is proved, and the frozen tail module uses this application directly. This conditional provider still does not by itself confer graph status. A probe checks exact type compatibility against the two blocks; no other node is used.

The four steps, and what each costs

1. l.mathcal.E.to.Lambdas on the Section 3 carriers (sq_cutoffHomogenizationError_le). The proved one-cube inequality ErrorComparison.half_homogenizationErrorOnCube_infinity_two_sq_le_max_weightedEllipticity is stated on a single Ch02.TriadicCoeffFamily; the Section 3 error observable and the Section 3 ellipticity observables are attached to two different families of the same ambient cutoff field. They agree modulo Ch02.TriadicCoeffFamily.A (coefficientCutoffFamily_aeeq), and CoarseGraining's HomogenizationErrorOnCube_eq_ofA, LambdaSq_eq_ofA, lambdaSq_eq_ofA transport the inequality. All three observables are measurable representatives, so the conclusion is almost everywhere; this is what Provider.Tail.isTwoTermBigOWith_of_ae_le exists to bridge. ** (normalization).** Every leg here is normalized at sigmaBar M (m-1): the error at comparator scale m-1, the upper leg by sigmaBar M (m-1)⁻¹, the lower leg by sigmaBar M (m-1). This is forced, because l.mathcal.E.to.Lambdas is an identity in one scalar.

2. The merge of the two rare lanes. e.cg.ellip.lower contributes a Gamma_{(1-sigma)/2} lane and e.cg.ellip.upper a Gamma_{(1-sigma)/3} lane, both at the same scale exp(-C^{-1}E^{-2}g^{-1}); the printed E^2 display has only one. At sigma = 1/4 the exponents are 3/8 and 1/4; the first is downgraded to 1/4 by class antitonicity and the two are merged by isBigOWith_gammaSigma_add_of_nonneg at the explicit constant mergeConstant_quarter = 81, giving the factor 324.

3. The square root (isDeterministicShiftTwoTermOneSidedOrlicz_of_sq_le of TailSqrt.lean), which turns Gamma_1 into Gamma_2 and Gamma_{1/4} into Gamma_{1/2}.

4. The output constant is chosen after the input constant as Ctail = exp(4 Ccg) + 646 Ccg + 2 Ccg^2 + 2, and the four places it is spent are isolated as tailAmplitudeGate_det, tailAmplitudeGate_middle, tailAmplitudeGate_heavy, and tailWindowGate:

   • exp(4 Ccg) <= Ctail opens e.percolation.admissibility at sigma = 1/4 from e.percolation.admissibility.tails;
   • 2 Ccg^2 <= Ctail turns the printed floor 4 gamma <= s into the parameter-dependent floor gamma/2 + exp(-Ccg^{-1}E^{-2}gamma^{-1}) <= s (tailWindowGate);
   • 646 Ccg <= Ctail pays the halved rate and the merge factor 324 (tailAmplitudeGate_heavy), using E^{-2} gamma^{-1} >= E^3 >= Ctail, which is exactly the interaction of the two gates of e.percolation.admissibility.tails;
   • 4 Ccg <= Ctail^2 and 2 Ccg <= Ctail^2 pay the deterministic and Gamma_2 lanes. ** (respected, and independently reconfirmed).** The deterministic and middle gates below are proved under gamma <= s alone; the printed 4 gamma <= s is spent only in tailWindowGate.

Main results

• exponentTwo --- the admissible exponent q = 2.
• coefficientCutoffFamily_aeeq, cutoffUpperEllipticityLiteral_eq, cutoffLowerEllipticityInvLiteral_eq --- the carrier bridge.
• sq_cutoffHomogenizationError_le --- l.mathcal.E.to.Lambdas at q = 2 on the Section 3 observables.
• pow_five_le_inv_of_le_rpow, cube_le_rate --- the admissibility window in polynomial form.
• tail_bounds_of_coarse_ellipticity_bounds --- the conditional coarse-to-tail provider.

References

• ABK26, p.tail.bounds; p.cg.ellipticity.bounds; the derivation.
• ABK26, l.mathcal.E.to.Lambdas.

def Algsuperdiff.Section3.Provider.Tail.exponentTwo : CoarseEllipticityExponent

The admissible exponent q = 2, at which l.mathcal.E.to.Lambdas is available.

Equations

• Algsuperdiff.Section3.Provider.Tail.exponentTwo = Algsuperdiff.Section3.CoarseEllipticityExponent.finite ⟨2, Algsuperdiff.Section3.Provider.Tail.exponentTwo._proof_1⟩

theorem Algsuperdiff.Section3.Provider.Tail.coefficientCutoffFamily_aeeq {d : ℕ} (M : ABKModel d) (m : ℤ) (omega : Cutoff.CutoffSample d) : (Cutoff.coefficientCutoffTriadicCoeffFamily M m omega).AEEq (HCPolySupport.Book.Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField (Cutoff.coefficientCutoff M.nu m omega) ⋯)

The compatible triadic family of the genuine cutoff agrees, modulo Chapter 2 almost-everywhere equality on every cube, with CoarseGraining's dependent family attached to the same ambient field.

theorem Algsuperdiff.Section3.Provider.Tail.cutoffUpperEllipticityLiteral_eq {d : ℕ} (M : ABKModel d) (m : ℤ) {s : ℝ} (q : CoarseEllipticityExponent) (omega : Cutoff.CutoffSample d) : Observable.cutoffUpperEllipticityLiteral M m m s q omega = HCPolySupport.Book.Ch02.LambdaSq (HCPolySupport.originCube d m) s (↑q) (Cutoff.coefficientCutoffTriadicCoeffFamily M m omega)

The literal upper multiscale ellipticity observable, evaluated.

theorem Algsuperdiff.Section3.Provider.Tail.cutoffLowerEllipticityInvLiteral_eq {d : ℕ} (M : ABKModel d) (m : ℤ) {s : ℝ} (q : CoarseEllipticityExponent) (omega : Cutoff.CutoffSample d) : Observable.cutoffLowerEllipticityInvLiteral M m m s q omega = (HCPolySupport.Book.Ch02.lambdaSq (HCPolySupport.originCube d m) s (↑q) (Cutoff.coefficientCutoffTriadicCoeffFamily M m omega))⁻¹

The literal inverse lower multiscale ellipticity observable, evaluated.

theorem Algsuperdiff.Section3.Provider.Tail.sq_cutoffHomogenizationError_le {d : ℕ} (M : ABKModel d) (m r : ℤ) {s : ℝ} (hs : 0 < s) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), Observable.cutoffHomogenizationErrorAtComparatorScale M m r ⟨s, hs⟩ omega ^ 2 ≤ 2 * (Observable.cutoffUpperEllipticity M m m s hs exponentTwo omega * (↑(Annealed.sigmaBar M r))⁻¹) + 2 * (Observable.cutoffLowerEllipticityInv M m m s hs exponentTwo omega * ↑(Annealed.sigmaBar M r))

l.mathcal.E.to.Lambdas on the Section 3 carriers, at q = 2.

Elementary consequences of the admissibility window

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

The upper gate E <= gamma^{-1/5} of e.percolation.admissibility.tails in polynomial form.

theorem Algsuperdiff.Section3.Provider.Tail.cube_le_rate {E gamma : ℝ} (hE : 0 < E) (h5 : E ^ 5 ≤ gamma⁻¹) : E ^ 3 ≤ E⁻¹ ^ 2 * gamma⁻¹

The reciprocal exponential rate of the rare lane is at least the cube of the lower gate: E^{-2} gamma^{-1} >= E ^ 3. Combined with Ctail <= E this is what makes the rare-lane and window gates below closable at a constant chosen after Ccg.

The three amplitude gates

These three lemmas are the exact price.

theorem Algsuperdiff.Section3.Provider.Tail.tailAmplitudeGate_det {Ccg Ctail gamma s : ℝ} (hCcg : 0 < Ccg) (hgamma : 0 < gamma) (hsg : gamma ≤ s) (hC : 4 * Ccg ≤ Ctail ^ 2) : 2 * Ccg + 2 * (Ccg * s * (2 * s - gamma)⁻¹) ≤ Ctail ^ 2

The deterministic gate. The doubled deterministic parts of e.cg.ellip.lower and e.cg.ellip.upper are below Ctail ^ 2, so their square root is below the deterministic shift Ctail of e.tail.bounds.

theorem Algsuperdiff.Section3.Provider.Tail.tailAmplitudeGate_middle {Ccg Ctail cstar gamma s : ℝ} (hCcg : 0 < Ccg) (hcstar : 0 < cstar) (hgamma : 0 < gamma) (hsg : gamma ≤ s) (hC : 2 * Ccg ≤ Ctail ^ 2) : 2 * (Ccg * cstar⁻¹ * s * gamma * (2 * s - gamma)⁻¹ ^ 3) ≤ (Ctail * (√cstar)⁻¹ * s⁻¹ * √gamma) ^ 2

The middle gate. The doubled Gamma_1 amplitude of e.cg.ellip.upper is below the square of the Gamma_2 amplitude of e.tail.bounds.

Only gamma <= s is used, not the printed 4 gamma <= s; this is the formal content.

theorem Algsuperdiff.Section3.Provider.Tail.tailAmplitudeGate_heavy {Ccg Ctail X : ℝ} (hCcg : 0 < Ccg) (hX : 0 < X) (h4 : 4 * Ccg ≤ Ctail) (hbig : 646 * Ccg ≤ X) : 324 * Real.exp (-(Ccg⁻¹ * X)) ≤ Real.exp (-(Ctail⁻¹ * X)) ^ 2

The rare-lane gate. The merged heavy leg, at the merge constant 324 of isBigOWith_gammaSigma_add_of_nonneg at sigma = 1/4, is below the square of the rare amplitude of e.tail.bounds.

theorem Algsuperdiff.Section3.Provider.Tail.tailWindowGate {Ccg Ctail E gamma s : ℝ} (hCcg : 0 < Ccg) (hCtail : 0 < Ctail) (hgamma : 0 < gamma) (hCtailE : Ctail ≤ E) (h5 : E ^ 5 ≤ gamma⁻¹) (hC2 : 2 * Ccg ^ 2 ≤ Ctail) (hs : 4 * gamma ≤ s) : gamma / 2 + Real.exp (-(Ccg⁻¹ * E⁻¹ ^ 2 * gamma⁻¹)) ≤ s

The window gate. The printed floor 4 gamma <= s of p.tail.bounds implies the parameter-dependent floor gamma/2 + exp(-Ccg^{-1} E^{-2} gamma^{-1}) <= s of p.cg.ellipticity.bounds.

theorem Algsuperdiff.Section3.Provider.Tail.sqrt_le_of_le_sq {A B : ℝ} (hB : 0 ≤ B) (h : A ≤ B ^ 2) : √A ≤ B

Squares dominate: A <= B ^ 2 with B >= 0 gives sqrt A <= B.

theorem Algsuperdiff.Section3.Provider.Tail.lowerEllipticityProfile_exponentTwo (C gamma s : ℝ) : lowerEllipticityProfile C gamma s exponentTwo = C * s * (2 * s - gamma)⁻¹

The deterministic lower profile of e.cg.ellip.lower at q = 2: the q >= 2 branch of lowerEllipticityProfile.

theorem Algsuperdiff.Section3.Provider.Tail.mergeConstant_quarter : (3 * max 1 (Real.log 2)) ^ (1 / 4)⁻¹ = 81

The merge constant of isBigOWith_gammaSigma_add_of_nonneg at sigma = 1/4.

The provider

theorem Algsuperdiff.Section3.Provider.Tail.tail_bounds_of_coarse_ellipticity_bounds (d : ℕ) (hcg : ∃ (Ccg : ℝ), 0 < Ccg ∧ ∀ (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M (m - 1) E → ∀ sigma ∈ Set.Ioc 0 (1 / 2), max (Real.exp (Ccg / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E → ↑E ≤ M.gamma ^ (-(1 / 5)) → ∀ (q : CoarseEllipticityExponent) (s : ℝ) (hsWindow : s ∈ Set.Icc (M.gamma / 2 + Real.exp (-(Ccg⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹))) 1), Probability.IsLowerIntegerFamilyOrlicz (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 2)) (fun (L : ℤ) (omega : Cutoff.CutoffSample d) => Observable.cutoffLowerEllipticityInv M m L s ⋯ q omega * ↑(Annealed.sigmaBar M (m - 1))) (m - 1) (lowerEllipticityProfile Ccg M.gamma s q) (Real.exp (-(Ccg⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹))) ∧ Probability.IsDeterministicShiftTwoTermOneSidedOrlicz (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 1) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 3)) (fun (omega : Cutoff.CutoffSample d) => Observable.cutoffUpperEllipticity M m m s ⋯ q omega * (↑(Annealed.sigmaBar M (m - 1)))⁻¹) Ccg (Ccg * (Disorder.cstar M)⁻¹ * s * M.gamma * (2 * s - M.gamma)⁻¹ ^ 3) (Real.exp (-(Ccg⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹)))) : ∃ (Ctail : ℝ), 0 < Ctail ∧ ∀ (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M (m - 1) E → ∀ (s : ℝ) (hsWindow : s ∈ Set.Icc (4 * M.gamma) 1), max Ctail (Disorder.cstar M)⁻¹ ≤ ↑E → ↑E ≤ M.gamma ^ (-(1 / 5)) → Probability.IsDeterministicShiftTwoTermOneSidedOrlicz (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (Observable.cutoffHomogenizationErrorAtComparatorScale M m (m - 1) ⟨s, ⋯⟩) Ctail (Ctail * (√(Disorder.cstar M))⁻¹ * s⁻¹ * √M.gamma) (Real.exp (-(Ctail⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹)))

p.tail.bounds from p.cg.ellipticity.bounds (ABK26).