Coarse-graining support: Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.Localization

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

From single-cube Caccioppoli to the radius raw estimate

This sidecar connects the fixed-cube local estimate produced by CoarseCaccioppoliEnergyBridge to the abstract radius-recursion surface in CoarseCaccioppoli. It keeps the geometric covering/testing step abstract: callers provide a single-cube raw estimate for each radius pair and the two coefficient-localization inequalities that compare the local cube coefficients to the note's radius coefficients.

def HCPolySupport.CoarseCaccioppoliBoundarySingleCubeRawEstimate {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s C uL2Sq : ℝ) (k h : ℝ → ℝ → ℝ) (F : ℝ → ℝ) : Prop

Radius-indexed version of the note-facing single-cube local estimate.

Equations

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

def HCPolySupport.CoarseCaccioppoliBoundarySingleCubeToRawCoefficientControl {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k h : ℝ → ℝ → ℝ) (F : ℝ → ℝ) : Prop

Coefficient-localization controls that turn the fixed-cube single-cube RHS into the radius-recursion raw RHS.

Equations

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

def HCPolySupport.CoarseCaccioppoliBoundarySingleCubeConstantCoefficientLocalization {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s C uL2Sq : ℝ) (k h : ℝ → ℝ → ℝ) : Prop

Pure coefficient localization for the constant single-cube term.

Equations

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

def HCPolySupport.CoarseCaccioppoliBoundarySingleCubeCenteredCoefficientLocalization {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C : ℝ) (k h : ℝ → ℝ → ℝ) : Prop

Pure coefficient localization for the centered single-cube term.

Equations

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

def HCPolySupport.CoarseCaccioppoliBoundarySingleCubeCoefficientLocalization {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k h : ℝ → ℝ → ℝ) : Prop

The pure coefficient localization data needed to convert fixed-cube single-cube coefficients into the radius-recursion coefficients.

Equations

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

def HCPolySupport.CoarseCaccioppoliBoundarySingleCubeConstantBaseLocalization {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (k h : ℝ → ℝ → ℝ) : Prop

Base scale/ellipticity inequality behind the constant coefficient localization, before multiplying by the common C sqrt(uL2Sq) factor.

Equations

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

def HCPolySupport.CoarseCaccioppoliBoundarySingleCubeCenteredBaseLocalization {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t : ℝ) (k h : ℝ → ℝ → ℝ) : Prop

Base scale/ellipticity inequality behind the centered coefficient localization, before multiplying by the common C / (s(1-s)) factor.

Equations

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

def HCPolySupport.CoarseCaccioppoliBoundarySingleCubeBaseLocalization {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t : ℝ) (k h : ℝ → ℝ → ℝ) : Prop

Base coefficient-localization inequalities before the harmless common positive factors are restored.

Equations

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

def HCPolySupport.CoarseCaccioppoliBoundarySingleCubeScaleLocalization (s t : ℝ) (k h : ℝ → ℝ → ℝ) : Prop

Scale-only part of the single-cube-to-raw localization.

Equations

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

theorem HCPolySupport.CoarseCaccioppoliBoundarySingleCubeScaleLocalization.of_gapScale_heightBounds (s t : ℝ) (k : ℝ → ℝ → ℕ) (h : ℝ → ℝ → ℝ) (hs : 0 < s) (ht : 0 < t) (hchoice : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) (hheight_const : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → 4 / s ≤ h ρ₁ ρ₂) (hheight_cent : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → 4 / (s + t) ≤ h ρ₁ ρ₂) : CoarseCaccioppoliBoundarySingleCubeScaleLocalization s t (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂)) h

def HCPolySupport.CoarseCaccioppoliBoundarySingleCubeEllipticityLocalization {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t : ℝ) : Prop

Ellipticity-only part of the single-cube-to-raw localization.

Equations

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

theorem HCPolySupport.CoarseCaccioppoliBoundarySingleCubeEllipticityLocalization.of_monotonicity {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (hLambda : (LambdaSq Q 1 (MultiscaleExponent.finite 1) a).rpow (1 / 2) ≤ (LambdaSq Q s (MultiscaleExponent.finite 1) a).rpow (1 / 2)) (hlambda : (lambdaSq Q (1 - s) (MultiscaleExponent.finite 1) a).rpow (-1 / 2) ≤ (lambdaSq Q t (MultiscaleExponent.finite 1) a).rpow (-1 / 2)) : CoarseCaccioppoliBoundarySingleCubeEllipticityLocalization Q a s t

theorem HCPolySupport.CoarseCaccioppoliBoundarySingleCubeEllipticityLocalization.of_ellipticity_sigmaCoarse {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) {s t lam Lam : ℝ} (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : ∀ j ≤ Q.scale, ∀ R ∈ descendantsAtScale Q j, ∃ (sigmaR : Mat d) (sigmaStarR : Mat d) (kappaR : Mat d), IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a) ∧ IsSigmaStarCoarse (openCubeSet R) a sigmaStarR ∧ IsKappaCoarse (openCubeSet R) a sigmaStarR kappaR ∧ IsSigmaCoarse (openCubeSet R) a sigmaR sigmaStarR kappaR ∧ IsUnit (Matrix.det sigmaStarR)) (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)) : CoarseCaccioppoliBoundarySingleCubeEllipticityLocalization Q a s t

theorem HCPolySupport.CoarseCaccioppoliBoundarySingleCubeBaseLocalization.of_scale_of_ellipticity {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t : ℝ) (k h : ℝ → ℝ → ℝ) (hs : 0 < s) (hs1 : s < 1) (hscale : CoarseCaccioppoliBoundarySingleCubeScaleLocalization s t k h) (helliptic : CoarseCaccioppoliBoundarySingleCubeEllipticityLocalization Q a s t) : CoarseCaccioppoliBoundarySingleCubeBaseLocalization Q a s t k h

theorem HCPolySupport.CoarseCaccioppoliBoundarySingleCubeBaseLocalization.of_scale_ellipticity_sigmaCoarse {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) {s t lam Lam : ℝ} (k h : ℝ → ℝ → ℝ) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hscale : CoarseCaccioppoliBoundarySingleCubeScaleLocalization s t k h) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : ∀ j ≤ Q.scale, ∀ R ∈ descendantsAtScale Q j, ∃ (sigmaR : Mat d) (sigmaStarR : Mat d) (kappaR : Mat d), IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a) ∧ IsSigmaStarCoarse (openCubeSet R) a sigmaStarR ∧ IsKappaCoarse (openCubeSet R) a sigmaStarR kappaR ∧ IsSigmaCoarse (openCubeSet R) a sigmaR sigmaStarR kappaR ∧ IsUnit (Matrix.det sigmaStarR)) (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)) : CoarseCaccioppoliBoundarySingleCubeBaseLocalization Q a s t k h

theorem HCPolySupport.CoarseCaccioppoliBoundarySingleCubeCoefficientLocalization.of_baseLocalization {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k h : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs : 0 < s) (hs1 : s < 1) (hbase : CoarseCaccioppoliBoundarySingleCubeBaseLocalization Q a s t k h) : CoarseCaccioppoliBoundarySingleCubeCoefficientLocalization Q a s t C uL2Sq k h

theorem HCPolySupport.CoarseCaccioppoliBoundarySingleCubeCoefficientLocalization.of_scale_of_ellipticity {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k h : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs : 0 < s) (hs1 : s < 1) (hscale : CoarseCaccioppoliBoundarySingleCubeScaleLocalization s t k h) (helliptic : CoarseCaccioppoliBoundarySingleCubeEllipticityLocalization Q a s t) : CoarseCaccioppoliBoundarySingleCubeCoefficientLocalization Q a s t C uL2Sq k h

theorem HCPolySupport.CoarseCaccioppoliBoundarySingleCubeCoefficientLocalization.of_scale_ellipticity_sigmaCoarse {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) {s t lam Lam : ℝ} (C uL2Sq : ℝ) (k h : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hscale : CoarseCaccioppoliBoundarySingleCubeScaleLocalization s t k h) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : ∀ j ≤ Q.scale, ∀ R ∈ descendantsAtScale Q j, ∃ (sigmaR : Mat d) (sigmaStarR : Mat d) (kappaR : Mat d), IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a) ∧ IsSigmaStarCoarse (openCubeSet R) a sigmaStarR ∧ IsKappaCoarse (openCubeSet R) a sigmaStarR kappaR ∧ IsSigmaCoarse (openCubeSet R) a sigmaR sigmaStarR kappaR ∧ IsUnit (Matrix.det sigmaStarR)) (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)) : CoarseCaccioppoliBoundarySingleCubeCoefficientLocalization Q a s t C uL2Sq k h

theorem HCPolySupport.CoarseCaccioppoliBoundarySingleCubeCoefficientLocalization.of_heightBounds_sigmaData {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) {s t lam Lam : ℝ} (C uL2Sq : ℝ) (k : ℝ → ℝ → ℕ) (h : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hchoice : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) (hheight_const : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → 4 / s ≤ h ρ₁ ρ₂) (hheight_cent : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → 4 / (s + t) ≤ h ρ₁ ρ₂) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : ∀ j ≤ Q.scale, ∀ R ∈ descendantsAtScale Q j, ∃ (sigmaR : Mat d) (sigmaStarR : Mat d) (kappaR : Mat d), IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a) ∧ IsSigmaStarCoarse (openCubeSet R) a sigmaStarR ∧ IsKappaCoarse (openCubeSet R) a sigmaStarR kappaR ∧ IsSigmaCoarse (openCubeSet R) a sigmaR sigmaStarR kappaR ∧ IsUnit (Matrix.det sigmaStarR)) (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)) : CoarseCaccioppoliBoundarySingleCubeCoefficientLocalization Q a s t C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂)) h

theorem HCPolySupport.CoarseCaccioppoliBoundarySingleCubeCoefficientLocalization.of_heightChoice_ellipticSigma {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) {s t lam Lam : ℝ} (C uL2Sq : ℝ) (k : ℝ → ℝ → ℕ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hchoice : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : ∀ j ≤ Q.scale, ∀ R ∈ descendantsAtScale Q j, ∃ (sigmaR : Mat d) (sigmaStarR : Mat d) (kappaR : Mat d), IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a) ∧ IsSigmaStarCoarse (openCubeSet R) a sigmaStarR ∧ IsKappaCoarse (openCubeSet R) a sigmaStarR kappaR ∧ IsSigmaCoarse (openCubeSet R) a sigmaR sigmaStarR kappaR ∧ IsUnit (Matrix.det sigmaStarR)) (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)) : CoarseCaccioppoliBoundarySingleCubeCoefficientLocalization Q a s t C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂)) (coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k)

theorem HCPolySupport.CoarseCaccioppoliBoundarySingleCubeCoefficientLocalization.of_integerizedHeightChoice {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) {s t lam Lam : ℝ} (C uL2Sq : ℝ) (k : ℝ → ℝ → ℕ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hchoice : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : ∀ j ≤ Q.scale, ∀ R ∈ descendantsAtScale Q j, ∃ (sigmaR : Mat d) (sigmaStarR : Mat d) (kappaR : Mat d), IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a) ∧ IsSigmaStarCoarse (openCubeSet R) a sigmaStarR ∧ IsKappaCoarse (openCubeSet R) a sigmaStarR kappaR ∧ IsSigmaCoarse (openCubeSet R) a sigmaR sigmaStarR kappaR ∧ IsUnit (Matrix.det sigmaStarR)) (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)) : CoarseCaccioppoliBoundarySingleCubeCoefficientLocalization Q a s t C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂)) (coarseCaccioppoliBoundaryIntegerizedLocalizedExplicitHeightOfScaleChoice Q a s t C k)

Integerized variant of of_heightChoice_ellipticSigma. The resulting height is the real cast of a natural depth, which is the form needed by the small-cube proof.

theorem HCPolySupport.CoarseCaccioppoliBoundarySingleCubeToRawCoefficientControl.of_localization {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k h : ℝ → ℝ → ℝ) (F : ℝ → ℝ) (hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ) (hloc : CoarseCaccioppoliBoundarySingleCubeCoefficientLocalization Q a s t C uL2Sq k h) : CoarseCaccioppoliBoundarySingleCubeToRawCoefficientControl Q a s t C uL2Sq k h F

theorem HCPolySupport.coarseCaccioppoliSingleCubeBoundaryNoteRhs_le_boundaryRawRhs_of_coefficientControl {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k h : ℝ → ℝ → ℝ) (F : ℝ → ℝ) {ρ₁ ρ₂ : ℝ} (hctrl : CoarseCaccioppoliBoundarySingleCubeToRawCoefficientControl Q a s t C uL2Sq k h F) (hρ₁ : 1 / 3 ≤ ρ₁) (hlt : ρ₁ < ρ₂) (hρ₂ : ρ₂ ≤ 1) : coarseCaccioppoliSingleCubeBoundaryNoteRhs Q a s C (k ρ₁ ρ₂) (h ρ₁ ρ₂) uL2Sq (F ρ₂) ≤ coarseCaccioppoliBoundaryAlphaOfHeight Q a s t C h ρ₁ ρ₂ * F ρ₂ + coarseCaccioppoliBoundaryCrossCoeffOfHeight Q a s C uL2Sq h ρ₁ ρ₂ * √(F ρ₂)

theorem HCPolySupport.coarseCaccioppoli_boundary_noteRawEstimate_of_singleCubeRawEstimate {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k h : ℝ → ℝ → ℝ) {F : ℝ → ℝ} (hsingle : CoarseCaccioppoliBoundarySingleCubeRawEstimate Q a s C uL2Sq k h F) (hctrl : CoarseCaccioppoliBoundarySingleCubeToRawCoefficientControl Q a s t C uL2Sq k h F) : CoarseCaccioppoliBoundaryNoteRawEstimate Q a s t C uL2Sq h F