Coarse-graining support: #
Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.HarmonicFinal.ExactSmallCube .LocalPatchConstructor.ConstantBranch
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Local-patch exact small-cube constant branches #
This file contains the constant/cross branch constructors for the arbitrary-center local-patch exact small-cube coefficient route.
theorem
HCPolySupport.SmallCubeConstantBranchSplit_of_closedCubeEllipticity_of_closedCubeEllipticity
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(center : Vec d)
(a : CoeffField d)
(s t Clocal Calpha Ccross : ℝ)
{lam Lam : ℝ}
(hClocal : 0 ≤ Clocal)
(hwork_constant_cross :
81 * Real.rpow 3 (2 * 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)⁻¹ * (12 * (quantitativeCubeCutoffHessianConst d * cubeScaleFactor Q / cubeRadius Q ^ 2) + 6 * (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
ρ₁ ρ₂ + 1;
have ξ := scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center ρ₁ ρm);
have B := coarseCaccioppoliLocalPatchCutoffHessianBound 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 constant branch of the local-patch exact-to-parent-raw coefficient constructor.
The integerized height/depth is governed by Calpha, but the constant/cross
coefficient itself is paid for by the independent Ccross budget.
theorem
HCPolySupport.SmallCubeConstantBranchSplitAllRadii_of_of_closedCubeEllipticity
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(center : Vec d)
(a : CoeffField d)
(s t Clocal Calpha Ccross : ℝ)
{lam Lam : ℝ}
(hClocal : 0 ≤ Clocal)
(hwork_constant_cross :
81 * Real.rpow 3 (2 * 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)⁻¹ * (12 * (quantitativeCubeCutoffHessianConst d * cubeScaleFactor Q / cubeRadius Q ^ 2) + 6 * (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 ρ₁ ρ₂ + 1;
have ξ := scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center ρ₁ ρm);
have B := coarseCaccioppoliLocalPatchCutoffHessianBound 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 constant branch of the local-patch exact-to-parent-raw coefficient constructor.
This is the proof-producing version used by the standard beta-dependent radius iteration.