Coarse-graining support:

Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.HarmonicFinal.ExactSmallCube.CenteredFronts

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Local small-cube coefficient package constructors

This sidecar file packages the two local EnergyBridge branch helpers into the canonical harmonic small-cube local coefficient hypothesis used by the final single-cube-to-raw bridge.

theorem HCPolySupport.SmallCubeConstantBranchSplit_of_closedCubeEllipticity {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s t Clocal Calpha Ccross : ℝ) {lam Lam : ℝ} (hClocal : 0 ≤ Clocal) (_hCcross : 0 ≤ Ccross) (hwork_constant_cross : 81 * Real.rpow 3 s * (↑(Fintype.card (Fin d)) * Clocal) ≤ ↑(Fintype.card (Fin d)) * Ccross) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hEllCube : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hlarge : ↑d * 3 ^ (↑d + 1) * (geometricDiscount 1 1)⁻¹ * (4 * (quantitativeCubeCutoffHessianConst d * cubeScaleFactor Q / cubeRadius Q ^ 2) + 2 * (quantitativeCubeCutoffGradientConst d / cubeRadius Q)) ≤ ↑(Fintype.card (Fin d)) * Clocal) (n : ℕ) : have ρ₁ := coarseCaccioppoliRadiusSequence n; have ρ₂ := coarseCaccioppoliRadiusSequence (n + 1); have ρm := coarseCaccioppoliBufferedCutoffRadius ρ₁ ρ₂; have CeffAlpha := ↑(Fintype.card (Fin d)) * Calpha; have CeffCross := ↑(Fintype.card (Fin d)) * Ccross; have hheight := coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t CeffAlpha coarseCaccioppoliTriadicGapScale; have j := coarseCaccioppoliBoundaryLocalizedExplicitHeightDepthOfScaleChoice Q a s t CeffAlpha coarseCaccioppoliTriadicGapScale ρ₁ ρ₂; have ξ := scalarCutoffGradientField (QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρm); have B := coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ ρm; have K := coarseCaccioppoliBoundaryCrossCoeffOfHeight Q a s CeffCross 1 hheight ρ₁ ρ₂; ∀ R ∈ descendantsAtDepth Q j, coarseCaccioppoliFluxEnergyExactConstantCoeff R a * (B + cubeBesovScaleWeight 1 R * cubeLpNorm R ⊤ ξ) ≤ K

Split buffered direct exact-raw constant branch calibration.

The descendant depth and explicit height are chosen with Calpha, while the parent cross coefficient is charged only to Ccross. This is the upstream constant-branch version of the split note-RHS budget.

theorem HCPolySupport.SmallCubeConstantBranchSplitAllRadii_of_closedCubeEllipticity {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s t Clocal Calpha Ccross : ℝ) {lam Lam : ℝ} (hClocal : 0 ≤ Clocal) (_hCcross : 0 ≤ Ccross) (hwork_constant_cross : 81 * Real.rpow 3 s * (↑(Fintype.card (Fin d)) * Clocal) ≤ ↑(Fintype.card (Fin d)) * Ccross) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hEllCube : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hlarge : ↑d * 3 ^ (↑d + 1) * (geometricDiscount 1 1)⁻¹ * (4 * (quantitativeCubeCutoffHessianConst d * cubeScaleFactor Q / cubeRadius Q ^ 2) + 2 * (quantitativeCubeCutoffGradientConst d / cubeRadius Q)) ≤ ↑(Fintype.card (Fin d)) * Clocal) ⦃ρ₁ ρ₂ : ℝ⦄ : 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → have ρm := coarseCaccioppoliBufferedCutoffRadius ρ₁ ρ₂; have CeffAlpha := ↑(Fintype.card (Fin d)) * Calpha; have CeffCross := ↑(Fintype.card (Fin d)) * Ccross; have hheight := coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t CeffAlpha coarseCaccioppoliTriadicGapScale; have j := coarseCaccioppoliBoundaryLocalizedExplicitHeightDepthOfScaleChoice Q a s t CeffAlpha coarseCaccioppoliTriadicGapScale ρ₁ ρ₂; have ξ := scalarCutoffGradientField (QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρm); have B := coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ ρm; have K := coarseCaccioppoliBoundaryCrossCoeffOfHeight Q a s CeffCross 1 hheight ρ₁ ρ₂; ∀ R ∈ descendantsAtDepth Q j, coarseCaccioppoliFluxEnergyExactConstantCoeff R a * (B + cubeBesovScaleWeight 1 R * cubeLpNorm R ⊤ ξ) ≤ K

All-radii split buffered direct exact-raw constant branch calibration.

This is the same constant/cross branch as SmallCubeConstantBranchSplit_of_closedCubeEllipticity, but with an arbitrary radius pair 1/3 ≤ ρ₁ < ρ₂ ≤ 1. It is the constant-branch input needed by the standard beta-dependent radius iteration.

noncomputable def HCPolySupport.coarseCaccioppoliCenteredAverageFront (d : ℕ) (s C : ℝ) : ℝ

Scalar front multiplying the average part of the centered exact coefficient after inserting the descendant cutoff-gradient estimate.

Equations

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

theorem HCPolySupport.coarseCaccioppoliFluxEnergyExactCenteredAverageCoeffFactorBound_localAcircOne_le_rpow_sub {d : ℕ} {Q R : TriadicCube d} (a : CoeffField d) {s Ceff : ℝ} {k j : ℕ} {ρ₁ ρ₂ : ℝ} (hCeff : 0 ≤ Ceff) (hs : 0 < s) (hR : R ∈ descendantsAtDepth Q j) (hchoice : CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂) (hlt : ρ₁ < ρ₂) : coarseCaccioppoliFluxEnergyExactCenteredAverageCoeffFactorBound (coarseCaccioppoliLambdaFactor R a s) (coarseCaccioppoliQuantitativeCutoffGradientBound Q ρ₁ ρ₂) (coarseCaccioppoliCanonicalGradientAcircOne R a ρ₁ ρ₂) Ceff ≤ ↑d * (3 / 2 * Ceff * 3 ^ (↑d + 1) * ((geometricDiscount s 1)⁻¹ * (geometricDiscount 1 1)⁻¹)) * (2 * quantitativeCubeCutoffGradientConst d * Real.rpow 3 (↑k - ↑j)) * ((LambdaSq R s (MultiscaleExponent.finite 1) a).rpow (1 / 2) * (lambdaSq R 1 (MultiscaleExponent.finite 1) a).rpow (-1 / 2))

The average part of the centered exact coefficient has the small-cube cutoff-gradient gain 3^(k-j) when the canonical A^\circ_1 factor is kept on the descendant cube. This is the first substitution line in the LaTeX centered single-cube estimate.

theorem HCPolySupport.fluxEnergyExactAverageCoeffBound_buffered_le_geometricGap {d : ℕ} {Q R : TriadicCube d} (a : CoeffField d) {s Ceff : ℝ} {k j : ℕ} {ρ₁ ρ₂ : ℝ} (hCeff : 0 ≤ Ceff) (hs : 0 < s) (hR : R ∈ descendantsAtDepth Q j) (hchoice : CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂) (hlt : ρ₁ < ρ₂) : coarseCaccioppoliFluxEnergyExactCenteredAverageCoeffFactorBound (coarseCaccioppoliLambdaFactor R a s) (coarseCaccioppoliQuantitativeCutoffGradientBound Q ρ₁ (coarseCaccioppoliBufferedCutoffRadius ρ₁ ρ₂)) (coarseCaccioppoliCanonicalGradientAcircOne R a ρ₁ (coarseCaccioppoliBufferedCutoffRadius ρ₁ ρ₂)) Ceff ≤ ↑d * (3 / 2 * Ceff * 3 ^ (↑d + 1) * ((geometricDiscount s 1)⁻¹ * (geometricDiscount 1 1)⁻¹)) * (4 * quantitativeCubeCutoffGradientConst d * Real.rpow 3 (↑k - ↑j)) * ((LambdaSq R s (MultiscaleExponent.finite 1) a).rpow (1 / 2) * (lambdaSq R 1 (MultiscaleExponent.finite 1) a).rpow (-1 / 2))

Buffered version of coarseCaccioppoliFluxEnergyExactCenteredAverageCoeffFactorBound_localAcircOne_le_rpow_sub. The midpoint cutoff doubles the average-branch gradient contribution.

theorem HCPolySupport.coarseCaccioppoliFluxEnergyExactCenteredAverageCoeffFactorBound_localAcircOne_le_alpha_of_scale {d : ℕ} [NeZero d] {Q R : TriadicCube d} (a : CoeffField d) {s t CeffLocal CeffWork : ℝ} {k j : ℕ} {ρ₁ ρ₂ lam Lam : ℝ} {hheight : ℝ → ℝ → ℝ} (hCeffLocal : 0 ≤ CeffLocal) (hCeffWork : 0 ≤ CeffWork) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hEllCube : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hR : R ∈ descendantsAtDepth Q j) (hBsum_s : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) (hSigmaSum_t : Summable fun (n : ℕ) => geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) (hchoice : CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂) (hlt : ρ₁ < ρ₂) (hscale : ↑d * (3 / 2 * CeffLocal * 3 ^ (↑d + 1) * ((geometricDiscount s 1)⁻¹ * (geometricDiscount 1 1)⁻¹)) * (2 * quantitativeCubeCutoffGradientConst d) * Real.rpow 3 ↑k ≤ CeffWork / (s * (1 - s)) * coarseCaccioppoliGapInv ρ₁ ρ₂) (hheight_le_j : hheight ρ₁ ρ₂ ≤ ↑j) : coarseCaccioppoliFluxEnergyExactCenteredAverageCoeffFactorBound (coarseCaccioppoliLambdaFactor R a s) (coarseCaccioppoliQuantitativeCutoffGradientBound Q ρ₁ ρ₂) (coarseCaccioppoliCanonicalGradientAcircOne R a ρ₁ ρ₂) CeffLocal ≤ coarseCaccioppoliBoundaryAlphaOfHeight Q a s t CeffWork hheight ρ₁ ρ₂

The average part of the centered exact coefficient localizes directly to the parent Alpha coefficient once the fixed average-branch scalar front is absorbed into the working constant.

This is the average-term line of the LaTeX small-cube coefficient comparison: the cutoff gradient gives 3^(k-j), the new descendant product lemma turns 3^{-j} Lambda_s(R)^{1/2} lambda_1(R)^{-1/2} into the parent theta term, and the integerized height only improves the final 3^{-sigma h} decay.

theorem HCPolySupport.coarseCaccioppoliCenteredAverageFront_nonneg (d : ℕ) {s C : ℝ} (hC : 0 ≤ C) (hs : 0 < s) : 0 ≤ coarseCaccioppoliCenteredAverageFront d s C

theorem HCPolySupport.cubeBesovScaleWeight_mul_eq_add {d : ℕ} (Q : TriadicCube d) (r q : ℝ) : cubeBesovScaleWeight r Q * cubeBesovScaleWeight q Q = cubeBesovScaleWeight (r + q) Q

Multiplicativity of Besov scale weights on a fixed cube.

noncomputable def HCPolySupport.coarseCaccioppoliCenteredBesovHessianBase (d : ℕ) (s C : ℝ) : ℝ

Scalar front multiplying the Hessian piece of the centered Besov exact coefficient before the cutoff scale estimate is inserted.

Equations

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

noncomputable def HCPolySupport.coarseCaccioppoliCenteredBesovGradientBase (d : ℕ) (s C : ℝ) : ℝ

Scalar front multiplying the gradient piece of the centered Besov exact coefficient before the cutoff scale estimate is inserted.

Equations

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

noncomputable def HCPolySupport.coarseCaccioppoliCenteredBesovHessianFront (d : ℕ) (s C : ℝ) : ℝ

Hessian scalar front after inserting the descendant cutoff estimate.

Equations

• HCPolySupport.coarseCaccioppoliCenteredBesovHessianFront d s C = HCPolySupport.coarseCaccioppoliCenteredBesovHessianBase d s C * (4 * HCPolySupport.quantitativeCubeCutoffHessianConst d)

noncomputable def HCPolySupport.coarseCaccioppoliCenteredBesovGradientFront (d : ℕ) (s C : ℝ) : ℝ

Gradient scalar front after inserting the descendant cutoff estimate.

Equations

• HCPolySupport.coarseCaccioppoliCenteredBesovGradientFront d s C = HCPolySupport.coarseCaccioppoliCenteredBesovGradientBase d s C * (2 * HCPolySupport.quantitativeCubeCutoffGradientConst d)

theorem HCPolySupport.coarseCaccioppoliCenteredBesovHessianFront_nonneg (d : ℕ) {s C : ℝ} (hC : 0 ≤ C) (hs : 0 < s) : 0 ≤ coarseCaccioppoliCenteredBesovHessianFront d s C

theorem HCPolySupport.coarseCaccioppoliCenteredBesovGradientFront_nonneg (d : ℕ) {s C : ℝ} (hC : 0 ≤ C) (hs : 0 < s) (hs1 : s < 1) : 0 ≤ coarseCaccioppoliCenteredBesovGradientFront d s C