LambdaCaps #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The coarse-grained ellipticity ratios of the flux-corrected field #
This module renders the two ratios of e.bound.Lambdas.by.Es.v2 (ABK26) at
the proved Section 4 carriers, and bounds their maximum by the flux-corrected
homogenization error 𝓔_{s,∞,2}. It is the Λ-side companion of the
good-event caps chain assembled in GoodEventCaps.lean.
What is proved, and what is not #
The printed Section 2 lemma l.mathcal.E.to.Lambdas (display
e.bound.Lambdas.by.Es) asserts the sharp, dimension-free two-sided
comparison
½ 𝓔_{s,∞,q}(□_m; a, σ₀)²
≤ max{ σ₀⁻¹ Λ_{s,q}(□_m; a) , σ₀ λ_{s,q}⁻¹(□_m; a) }
≤ 1 + 2 𝓔_{s,∞,q}(□_m; a, σ₀)² + 2^{1/2} 𝓔_{s,∞,q}(□_m; a, σ₀) .
Only the upper half is treated here, and only in a 2d-lossy form:
max{…} ≤ 2d (𝓔² + 1) at q = 2. This is not the printed statement and
must never be presented as l.mathcal.E.to.Lambdas:
- the printed constants
1, 2, 2^{1/2}are absolute, ours carries a factor2d; the printed proof route (the block quadratic identitye.J.by.f, the matrix inequalitiese.xminusonetimesxminusonesquared.{sstar,b}, and the eigenvalue argument forf(x) = x⁻¹(x−1)²) is not formalized anywhere in this repository or in CoarseGraining; - the printed lower half
½𝓔² ≤ max{…}and theq = 2refinemente.bound.Lambdas.by.Es.q2are not proved here at all; - the printed lemma is stated for every
q ∈ [1,∞]; ours is theq = 2endpoint only, which is the exponent the consumer displaye.bound.Lambdas.by.Es.v2uses.
The lossy form suffices for the only §4.3 consumption site: the good-event cap
needs a bound by a constant C(d), and 2d(𝓔²+1) with 𝓔 capped is such a
constant.
Main definitions #
fluxCorrectedUpperEllipticity—Λ_{s,2}(□_k; a_L − (κ_L−κ_k)_{□_k}).fluxCorrectedLowerEllipticityInv—λ_{s,2}⁻¹(□_k; a_L − (κ_L−κ_k)_{□_k}).fluxCorrectedEllipticityRatioMax— the displayedmax{σ_k⁻¹Λ_{s,2}, σ_kλ_{s,2}⁻¹}.
Main results #
max_ellipticityRatio_le_homogenizationError— the2d-lossy upper half at CoarseGraining's carriers, for an arbitrary positive scalar comparatorσ.fluxCorrectedEllipticityRatioMax_le— its pointwise transport to the flux-corrected literal error at the comparatorσ_k.ae_fluxCorrectedEllipticityRatioMax_le— the almost-everywhere form at the measurable representative, uniformly inL ≥ k.two_mul_dim_mul_sq_add_one_le_of_le— the monotone folding step that turns an𝓔-cap into a constant.
Carrier conventions used (resolution A4) #
Every cube is the origin cube originCube d k; a statement at z + □_k is
obtained by translating the sample, i.e. by evaluating at
Cutoff.translateCutoffSample z omega. The comparator is σ_k Id = isotropicComparatorMatrix (Annealed.sigmaBar M k), which is CoarseGraining's
scalarMatrix (σ_k : ℝ) on the nose.
References #
- ABK26,
l.mathcal.E.to.Lambdas. - ABK26,
e.bound.Lambdas.by.Es.v2.
1. The two ratio carriers at the flux-corrected field #
Λ_{s,2}(□_k; a_L − (κ_L − κ_k)_{□_k}), as a function of the cutoff
sample. The value at z + □_k is this function at
Cutoff.translateCutoffSample z omega (resolution A4).
Equations
- One or more equations did not get rendered due to their size.
Instances For
λ_{s,2}⁻¹(□_k; a_L − (κ_L − κ_k)_{□_k}). The manuscript always writes the
inverse lower constant, and so does the proved Section 3 observable
Observable.cutoffLowerEllipticityInvLiteral; this is the same reading at the
flux-corrected field.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The left-hand side of e.bound.Lambdas.by.Es.v2, taken at the single
comparator σ_k on both legs.
We follow the lemma, i.e. the mathematically supported reading, and take σ₀ = σ_k at the cube □_k that carries the functional.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The unfolded reading of fluxCorrectedEllipticityRatioMax.
2. The 2d-lossy upper half at CoarseGraining's carriers #
The upper half of e.bound.Lambdas.by.Es, in its 2d-lossy q = 2 form.
Transport of CoarseGraining's
Ch02.max_weightedEllipticity_finite_two_le_card_mul_homogenizationError_sq_add_one
with Fintype.card (Fin d) evaluated.
This is not the printed lemma: the printed right-hand side is the
dimension-free 1 + 2𝓔² + 2^{1/2}𝓔. See the module docstring.
3. Transport to the flux-corrected sample carrier #
The ratio maximum at the flux-corrected field, bounded by the literal flux-corrected error. Pointwise in the sample; no probability enters.
The almost-everywhere form at the measurable representative, uniformly
in L ≥ k.
The passage from the literal error to
Support.fluxCorrectedErrorRepresentative is the proved
Support.ae_forall_fluxCorrectedError_eq_representative, which carries all L ≥ k on a single probability-one event because the index set is countable.
4. The folding step #
The cap-folding step. An 𝓔-bound 𝓔 ≤ t turns the envelope
2d(𝓔² + 1) into the constant 2d(t² + 1). This is the arithmetic the
good-event cap performs after the annular anchor has supplied t.