CoarseGrainingP2

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

p.general.coarse.graining at p = 2: the CoarseGraining interface

Nothing here imports that file, and nothing here claims the anchor or any source node.

The finding

  Homogenization.Book.Ch03.generalCoarseGrainingL2TwoExponentTheory
      (d : ℕ) [NeZero d] : GeneralCoarseGrainingL2TwoExponentTheory d

(Homogenization/Book/Ch03/Theorems/GeneralCoarseGrainingL2TwoExponent.lean). Its single field packages the manuscript display e.general.coarse.graining.estimate at p = 2 in a scale-separated form: the flux-response exponent r (the manuscript's s_1) and the forcing exponent r₂ (the manuscript's s_2) are independent, and the forcing term carries the visible inverse depth factor 3^{-r₂ (m-n)}.

This module turns that package into a usable estimate with a named d-only constant and supplies the two conversions the Section 4.3 chain needs:

• the left-hand side of CoarseGraining's estimate dominates its first summand, the constant-coefficient gradient defect a₀(∇u − ∇v) (the second summand is the flux defect the manuscript "throws away");
• CoarseGraining's depth-truncated q = 1 error coarseGrainingHomogenizationErrorAtDepth Q a a₀ r j is dominated by the development's own q = 2 one-cube error at any index t ≤ r/2, at the single cost 3^{t j} — and at j = 0 (the manuscript's m = n specialization) it is the one-cube q = 1 error, with no cost at all.

Divergences from the printed proposition (reported, not hidden)

• Hypothesis r < s/2. The printed proposition asks only s_1 < s < s_2; CoarseGraining's package asks r < s/2 (a factor-two-stricter separation) together with s < 1 and r ≤ r₂. This is what forces the Section 4.3 comparison exponent above the printed s/2 — see CoarseGrainingL2Interior.lean.
• The forcing bracket. The printed proposition writes the forcing prefactor as (1 + 𝓔²_{s_1/2,∞,2}); CoarseGraining writes it through the coarse-grained ellipticity factors Λ^{1/2}_{r/2,2}, λ^{-1/2}_{r/2,2}, λ^{-1}_{r/2,2} and one further 𝓔 λ^{-1/2} product. The two are related by l.mathcal.E.to.Lambdas; on the good event both are capped by C(d).
• The mesoscopic index. The printed 𝓔_{s_1,∞,1}(□_m, n; a, σ₀) is a two-index object; CoarseGraining encodes it as the maximum of the one-cube error over the depth-j descendants of Q. At j = 0 the two encodings agree.

Nothing above is asserted to be the printed statement; every deviation is carried in the statements themselves.

References

• ABK26, p.general.coarse.graining.
• ABK26, l.harmonic.approximation.good.scales, (e.homogenization.L2.interior).

1. The scalar comparison background

def Algsuperdiff.Section4.Provider.ExcessDecay.scalarComparator {d : ℕ} {sigma : ℝ} (hsigma : 0 < sigma) : HCPolySupport.Book.Ch03.ConstantCoeffMatrix d

The constant isotropic background σ Id, bundled as CoarseGraining's ConstantCoeffMatrix. See the duplication disclosure.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.scalarComparator_matrix {d : ℕ} {sigma : ℝ} (hsigma : 0 < sigma) : (scalarComparator hsigma).matrix = HCPolySupport.scalarMatrix sigma

theorem Algsuperdiff.Section4.Provider.ExcessDecay.scalarComparator_isPositiveScalarMatrix {d : ℕ} {sigma : ℝ} (hsigma : 0 < sigma) : HCPolySupport.IsPositiveScalarMatrix (scalarComparator hsigma).matrix

theorem Algsuperdiff.Section4.Provider.ExcessDecay.matrixNorm_scalarMatrix {d : ℕ} [NeZero d] {sigma : ℝ} (hsigma : 0 ≤ sigma) : HCPolySupport.Book.Ch02.matrixNorm (HCPolySupport.scalarMatrix sigma) = sigma

|σ Id| = σ in CoarseGraining's Chapter 2 (Euclidean operator) normalization.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.constantCoeffMatrixNormHalf_scalarComparator {d : ℕ} [NeZero d] {sigma : ℝ} (hsigma : 0 < sigma) : HCPolySupport.Book.Ch03.constantCoeffMatrixNormHalf (scalarComparator hsigma) = sigma.rpow (1 / 2)

|a₀|^{1/2} = σ^{1/2} at the scalar background.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.constantCoeffMatrixNorm_scalarComparator {d : ℕ} [NeZero d] {sigma : ℝ} (hsigma : 0 < sigma) : HCPolySupport.Book.Ch03.constantCoeffMatrixNorm (scalarComparator hsigma) = sigma

|a₀| = σ at the scalar background.

2. The d-only constant and the estimate

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.coarseGrainingP2Const (d : ℕ) [NeZero d] : ℝ

The d-only constant of CoarseGraining's scale-separated p = 2 general coarse-graining package. It is the constant produced by Homogenization.Book.Ch03.generalCoarseGrainingL2TwoExponentTheory; CoarseGraining exposes it only existentially, so it is named here by choice.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.coarseGrainingP2Const d = Classical.choose ⋯

theorem Algsuperdiff.Section4.Provider.ExcessDecay.coarseGrainingP2Const_pos (d : ℕ) [NeZero d] : 0 < coarseGrainingP2Const d

theorem Algsuperdiff.Section4.Provider.ExcessDecay.coarseGrainingP2_estimate {d : ℕ} [NeZero d] {Q : HCPolySupport.TriadicCube d} {a : HCPolySupport.Book.Ch03.CoeffFamily d} {a0 : HCPolySupport.Book.Ch03.ConstantCoeffMatrix d} (ha0 : HCPolySupport.IsPositiveScalarMatrix a0.matrix) {s r r₂ : ℝ} {j : ℕ} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (w : HCPolySupport.Book.Ch03.CoarseGrainingComparisonDatum Q a a0 g) (hs : 0 < s) (hr : 0 < r) (hrs : r < s / 2) (hs1 : s < 1) (hr₂ : r ≤ r₂) (hg : HCPolySupport.Book.Ch03.ForceBesovRegularity Q r₂ g) : HCPolySupport.Book.Ch03.homogenizationComparisonNegativeBesovLHS Q a a0 s w.u w.v ≤ HCPolySupport.Book.Ch03.generalCoarseGrainingL2TwoExponentRHS (coarseGrainingP2Const d) Q a a0 s r r₂ j g w.u

The general coarse-graining estimate at p = 2, with a named constant.

For a coarse-graining datum w on the triadic cube Q (CoarseGraining's CoarseGrainingComparisonDatum: u solves −∇·a∇u = ∇·g, v solves −∇·a₀∇v = ∇·g, and u − v has zero trace), a positive scalar background a₀, and exponents 0 < r < s/2, s < 1, r ≤ r₂ with g ∈ H^{r₂}(Q):

  [a₀(∇u − ∇v)]_{B^{-s}_{2,2}(Q)} + [a∇u − a₀∇v]_{B^{-s}_{2,2}(Q)}
      ≤ generalCoarseGrainingL2TwoExponentRHS (coarseGrainingP2Const d) … .

This is ABK26's e.general.coarse.graining.estimate at p = 2, in CoarseGraining's own carriers and with CoarseGraining's own scale-separated right-hand side.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.generalCoarseGrainingL2TwoExponentRHS_eq_const_mul {d : ℕ} (C : ℝ) (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) (a0 : HCPolySupport.Book.Ch03.ConstantCoeffMatrix d) (s r r₂ : ℝ) (j : ℕ) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (u : HCPolySupport.H1Function (HCPolySupport.Book.Ch02.cubeDomain Q).carrier) : HCPolySupport.Book.Ch03.generalCoarseGrainingL2TwoExponentRHS C Q a a0 s r r₂ j g u = C * HCPolySupport.Book.Ch03.generalCoarseGrainingL2TwoExponentRHS 1 Q a a0 s r r₂ j g u

The right-hand side is linear in its constant.

3. Discarding the flux summand

theorem Algsuperdiff.Section4.Provider.ExcessDecay.negativeSeminormTwo_nonneg {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) : 0 ≤ HCPolySupport.cubeBesovNegativeVectorSeminormTwo Q s F

The q = 2 negative Besov seminorm is nonnegative, with no boundedness hypothesis. See the duplication disclosure.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.constantGradientSeminorm_le_comparisonLHS {d : ℕ} (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) (a0 : HCPolySupport.Book.Ch03.ConstantCoeffMatrix d) (s : ℝ) (u v : HCPolySupport.H1Function (HCPolySupport.Book.Ch02.cubeDomain Q).carrier) : HCPolySupport.cubeBesovNegativeVectorSeminormTwo Q s (HCPolySupport.Book.Ch03.homogenizationComparisonConstantGradientField a0 u v) ≤ HCPolySupport.Book.Ch03.homogenizationComparisonNegativeBesovLHS Q a a0 s u v

"Throwing away the flux term". The first summand of CoarseGraining's comparison left-hand side — the constant-coefficient gradient defect a₀(∇u − ∇v), which is what ABK26's display e.homogenization.L2.interior keeps — is dominated by the full left-hand side.

4. The homogenization error: CoarseGraining's depth maximum vs the development object

theorem Algsuperdiff.Section4.Provider.ExcessDecay.coarseGrainingHomogenizationErrorAtDepth_le {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) (a0 : HCPolySupport.Book.Ch03.ConstantCoeffMatrix d) {r t : ℝ} (j : ℕ) (ht : 0 < t) (htr : t ≤ r / 2) : HCPolySupport.Book.Ch03.coarseGrainingHomogenizationErrorAtDepth Q a a0 r j ≤ Real.rpow 3 (t * ↑j) * HCPolySupport.Book.Ch02.HomogenizationErrorOnCube Q t HCPolySupport.Book.Ch02.MultiscaleExponent.infinity (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a a0.matrix

CoarseGraining's q = 1 depth maximum, in the development's q = 2 one-cube object.

For 0 < t ≤ r/2,

  max_{R ∈ descendants_j(Q)} 𝓔_{r,∞,1}(R; a, a₀)  ≤  3^{t j} 𝓔_{t,∞,2}(Q; a, a₀) .

At j = 0 the factor is 1, and at t = r/2 the index is exactly half the flux-response index.