Coarse-graining support: Support.HighContrast.EntryScale.Inputs #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Source labels and external analytic inputs #
This file is the only place where the development records external analytic source material. It deliberately records metadata, not theorem surfaces: precise Lean statements should be added only after the corresponding provenance has been audited against the source.
Exponents fixed by the high-contrast weak-norm machinery.
This record is indexed by the dimension d and carries the manuscript
quantitative coarse-grained ellipticity parameters params so that the
source-max edge-loss gaps can be stated as pure numeric inequalities on the
record's own parameters (no quantifiers over laws). Consumers recover the
per-(P4) form via sourceMaxLowerGap_of_params/sourceMaxUpperGap_of_params
using hP4.params = hc.params.
Source: the high-moment paper (Armstrong–Kuusi–Loher, to appear), and
ultimately the high-contrast manuscript, label l.weaknorms.moreproto.
The manuscript quantitative coarse-grained ellipticity parameters that the source-max gaps are stated against.
- rhoM : ℝ
Positive stochastic decay exponent controlling source weights and the subthreshold scale decay.
- beta : ℝ
Positive response exponent used in the localization and small-contrast inputs.
- zeta : ℝ
High-contrast exponent constrained to lie strictly between one and two.
- kappaH : ℝ
Memory decay rate
kappa_H = min{rho_M, beta, beta_edge}at which the Lyapunov memory variableHcontracts. It is bounded above by the union-bound exponentrho_Mand the response exponentbeta, whilerho_Mretains its other (union-bound / stochastic-decay) roles.Source: the high-moment paper (Armstrong–Kuusi–Loher, to appear), memory-decay discussion
s.memoryandl.lyapunov. - sourceMaxLowerGap : self.rhoM < self.params.sLower + Book.Ch05.Section53.JUpperBoundCoarseFluctuations.coarseFluctuationBeta self.params
Source-max edge-loss compatibility at the lower ellipticity exponent.
This is the exponent gap used by the faithful
p.HC.CRsource-max argument: the stochastic source weight must decay strictly slower than the lower Section 5.2 edge-loss exponent. Stated as a pure numeric inequality on the record's own parameters. - sourceMaxUpperGap : self.rhoM < self.params.sUpper + Book.Ch05.Section53.JUpperBoundCoarseFluctuations.coarseFluctuationBeta self.params
Source-max edge-loss compatibility at the upper ellipticity exponent.
This is the matching upper-edge gap for the same manuscript source-max argument.
Instances For
Per-(P4) form of the lower source-max gap: for any law whose (P4)
parameters match the record, the gap holds against section53CoarseFluctuationBeta.
Per-(P4) form of the upper source-max gap.
Constants in the localization and small-contrast handoff.
Source: e.localization and e.small.contrast.
- localizationCoefficient : ℝ
Nonnegative prefactor of the localization error.
- localizationExponent : ℝ
Positive decay exponent of the localization error across scales.
- delta0 : ℝ
Positive small-contrast threshold, bounded above by one.
- smallContrastCoefficient : ℝ
Positive prefactor of the small-contrast decay bound.
- alpha0 : ℝ
Positive decay exponent after the small-contrast threshold is met.
Instances For
Typed external handoff for localization and the small-contrast theorem.
Source: e.localization and e.small.contrast. This is one of the audited
external inputs allowed at final assembly; downstream theorems should consume
this surface rather than assuming already assembled final decay.
The localization and small-contrast fields are guarded by the requirement
hP4.params = hc.params: the fixed constants below are the ones produced by the
Section 5.5/5.6 source theorems at the record's own manuscript parameters, so the
bounds only fire for laws whose (P4) parameters agree with hc.params. This
guard is exactly what makes the record inhabitable (see RecordsFinal.lean).
- localization {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (hP4 : Book.Ch05.QuantitativeCoarseGrainedEllipticity P) : hP4.params = hc.params → ∀ {k n : ℕ}, k ≤ n → Book.Ch05.thetaAtScale hP hStruct ↑n ≤ Book.Ch05.Section55.shiftedWidetildeThetaAtScale P (↑n) hP4 (2 * hc.beta) ∧ Book.Ch05.Section55.shiftedWidetildeThetaAtScale P (↑n) hP4 (2 * hc.beta) ≤ Book.Ch05.thetaAtScale hP hStruct ↑k + self.localizationCoefficient * 3 ^ (-(self.localizationExponent * ↑(n - k))) * Book.Ch05.widetildeThetaAtScale P 0 hP4
- small_contrast {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (hP4 : Book.Ch05.QuantitativeCoarseGrainedEllipticity P) : hP4.params = hc.params → ∀ {N : ℕ}, Book.Ch05.Section55.shiftedWidetildeThetaAtScale P (↑N) hP4 (2 * hc.beta) - 1 ≤ self.delta0 → ∀ (n : ℕ), Book.Ch05.thetaAtScale hP hStruct ↑(N + n) - 1 ≤ self.smallContrastCoefficient * 3 ^ (-(self.alpha0 * ↑n))
Instances For
Parameters in the high centered block moment hypothesis.
Source: a.HM, e.HM, and e.Q.large. The fields
holderExponentFloor, p4Params, and two_mul_p4_xi_le_Q record the finite
Holder-exponent thresholds from the high-contrast estimate; the TeX
requirement is represented by the concrete inequalities
holderExponentFloor < Q and 2 * xi <= Q. The latter is relative to the
fixed quantitative coarse-grained ellipticity parameters used by the theorem;
it is not quantified over every possible witness for every law.
- highMomentParameter : ℝ
Nonnegative parameter in the high centered block moment data.
- Q : ℝ
Moment order, at least two, satisfying the dimension and decay threshold.
- gamma : ℝ
Positive scale decay rate in the high centered moment envelope.
- momentCoefficient : ℝ
Nonnegative prefactor of the high centered moment envelope.
- holderExponentFloor : ℝ
Nonnegative Holder-exponent threshold required to be strictly below the moment order.
- p4Params : Book.Ch05.QuantitativeCoarseGrainedEllipticityParams d
Fixed quantitative ellipticity parameters, with twice the exponent
xibounded by the moment order.
Instances For
Constants for the old polynomial subthreshold contribution in a.HM.
Source: the high-moment paper (Armstrong–Kuusi–Loher, to appear). This records
only the polynomial prefactor before the weak-norm weight is used; the
geometric buffer absorption is proved in MomentConsequences.lean.
- polynomialCoefficient : ℝ
Nonnegative prefactor of the polynomial subthreshold moment envelope.
- polynomialExponent : ℝ
Exponent of the polynomial factor in the subthreshold moment envelope.
Instances For
The deterministic envelope appearing in the high-moment input a.HM.
The source note writes this as C_Q 3^{-Q γ (j-N)} for every j ≥ N,
uniformly over triadic translates. We keep the j - N dependence explicit
so later results can substitute this exact scale decay into the descendant
union bound.
Equations
- HCPolySupport.HighContrast.EntryScale.highCenteredMomentEnvelope hm N j = ENNReal.ofReal (hm.momentCoefficient * Real.rpow 3 (-(hm.Q * hm.gamma) * ↑(j - N)))
Instances For
Moving the initial scale of the high-moment envelope forward only weakens the decay requirement.
The scale-uniform high centered-moment assumption from a.HM/e.HM.
Here centeredBlockDeviation j Q ω denotes the nonnegative matrix-normalized
observable
|Ahom_j^{-1/2}(A(Q)-Ahom_j)Ahom_j^{-1/2}| attached to a triadic cube Q of
scale j. The hypothesis is intentionally only a one-block input: descendant
counts, weak-norm weights, terminal normalization losses, and union bounds are
proved downstream rather than built into this assumption.
- measurable {j : ℕ} : N ≤ j → ∀ {Q : TriadicCube d}, Q.scale = ↑j → AEMeasurable (fun (ω : Ω) => centeredBlockDeviation j Q ω ^ hm.Q) μ
Instances For
The high centered-moment hypothesis may be restarted at any later scale.
The subthreshold second-moment envelope after applying the weak-norm gap.
The source paragraph says that before the weak-norm weight the old
high-contrast bound contributes at most C (2+T)^A. Since the subthreshold
scales have m - j >= m - N, the squared weak weight contributes
3^{-2 rho_M (m-N)}.
Equations
- HCPolySupport.HighContrast.EntryScale.subthresholdPolynomialMomentEnvelope hc sub T n = ENNReal.ofReal (sub.polynomialCoefficient * ((2 + T) ^ sub.polynomialExponent * 3 ^ (-(2 * hc.rhoM) * ↑n)))
Instances For
Root-level subthreshold envelope from the old high-contrast input.
This is the same source paragraph as subthresholdPolynomialMomentEnvelope,
but before squaring. It is the shape needed by the lower-edge coefficient
comparison, whose residual local-window terms are controlled as
L^{xi_edge} roots rather than by the L^2 union-bound estimate.
Equations
- HCPolySupport.HighContrast.EntryScale.subthresholdPolynomialRootEnvelope hc sub T n = sub.polynomialCoefficient * ((2 + T) ^ sub.polynomialExponent * 3 ^ (-hc.rhoM * ↑n))
Instances For
Source-facing old polynomial subthreshold input from a.HM.
Here subthresholdMax m denotes the already weighted contribution
\mathcal M_m^{<N} from scales j < N, including the deterministic drift
assigned to that range. The only analytic content assumed here is the old
high-contrast polynomial bound from the corrected note; the buffer that makes
it small is proved downstream.
- aestronglyMeasurable {m : ℕ} : N ≤ m → MeasureTheory.AEStronglyMeasurable (subthresholdMax m) μ