Coarse-graining support: #
Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.HarmonicFinal.CoefficientBounds
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.coarseCaccioppoli_boundary_qone_of_canonicalHarmonicRawCoefficientBounds
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(baseEnergy : Vec d → ℝ)
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(i : Fin d)
(hC : 0 < C)
(hs : 0 < s)
(ht : 0 < t)
(hst : s + t < 1)
(hu : 0 ≤ uL2Sq)
(hbase_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ baseEnergy x)
(hbase_int : MeasureTheory.IntegrableOn baseEnergy (cubeSet Q) MeasureTheory.volume)
(hinner_energy_le :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ → ρ₂ ≤ 1 → ∀ x ∈ scaledClosedCubeSet Q ρ₁, baseEnergy x ≤ scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(henergyAvg :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
(cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) = coarseCaccioppoliLocalizedEnergyRadiusProfile Q baseEnergy ρ₂)
(hfluxEnergy :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
CoarseCaccioppoliFluxEnergyControls Q a s (fun (x : Vec d) => matVecMul (a x) ((w ρ₁ ρ₂).toH1.grad x))
fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(hnonzeroFactors : CoarseCaccioppoliBoundaryCanonicalGradientNonzeroEnergyFactors Q a w)
(hlambda1 : 0 < lambdaSq Q 1 (MultiscaleExponent.finite 1) a)
(hgrad :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
CubeAverageGradientEnergyControl Q a (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.grad x) fun (x : Vec d) =>
scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(hprojected : CoarseCaccioppoliBoundaryCanonicalGradientProjectedPoincareFamily Q a C w i)
(hrawcoeff : CoarseCaccioppoliBoundaryCanonicalHarmonicRawCoefficientBounds Q a s t C uL2Sq w)
(hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a)
(hSigmaSum_t :
Summable fun (n : ℕ) =>
geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
:
coarseCaccioppoliLocalizedEnergyRadiusProfile Q baseEnergy (1 / 3) ≤ coarseCaccioppoliBoundaryExplicitHeightBound Q a s t C uL2Sq
Boundary fixed-localized-energy coarse Caccioppoli from canonical raw
coefficient bounds, with the older nonzero-energy/lambdaSq positivity split
kept as a compatibility surface.
theorem
HCPolySupport.coarseCaccioppoli_interior_qone_of_canonicalHarmonicRawCoefficientBounds
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(baseEnergy : Vec d → ℝ)
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(i : Fin d)
(hC : 0 < C)
(hs : 0 < s)
(ht : 0 < t)
(hst : s + t < 1)
(hu : 0 ≤ uL2Sq)
(hbase_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ baseEnergy x)
(hbase_int : MeasureTheory.IntegrableOn baseEnergy (cubeSet Q) MeasureTheory.volume)
(hinner_energy_le :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ → ρ₂ ≤ 1 → ∀ x ∈ scaledClosedCubeSet Q ρ₁, baseEnergy x ≤ scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(henergyAvg :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
(cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) = coarseCaccioppoliLocalizedEnergyRadiusProfile Q baseEnergy ρ₂)
(hfluxEnergy :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
CoarseCaccioppoliFluxEnergyControls Q a s (fun (x : Vec d) => matVecMul (a x) ((w ρ₁ ρ₂).toH1.grad x))
fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(hnonzeroFactors : CoarseCaccioppoliBoundaryCanonicalGradientNonzeroEnergyFactors Q a w)
(hlambda1 : 0 < lambdaSq Q 1 (MultiscaleExponent.finite 1) a)
(hgrad :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
CubeAverageGradientEnergyControl Q a (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.grad x) fun (x : Vec d) =>
scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(hprojected : CoarseCaccioppoliBoundaryCanonicalGradientProjectedPoincareFamily Q a C w i)
(hrawcoeff : CoarseCaccioppoliBoundaryCanonicalHarmonicRawCoefficientBounds Q a s t C uL2Sq w)
(hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a)
(hSigmaSum_t :
Summable fun (n : ℕ) =>
geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
:
coarseCaccioppoliLocalizedEnergyRadiusProfile Q baseEnergy (1 / 3) ≤ coarseCaccioppoliInteriorExplicitHeightBound Q a s t C uL2Sq
Interior fixed-localized-energy coarse Caccioppoli from canonical raw
coefficient bounds, with the older nonzero-energy/lambdaSq positivity split
kept as a compatibility surface.
theorem
HCPolySupport.coarseCaccioppoli_boundary_qone_of_canonicalHarmonicPositiveFactors
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(baseEnergy : Vec d → ℝ)
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(i : Fin d)
(hC : 0 < C)
(hs : 0 < s)
(ht : 0 < t)
(hst : s + t < 1)
(hu : 0 ≤ uL2Sq)
(hbase_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ baseEnergy x)
(hbase_int : MeasureTheory.IntegrableOn baseEnergy (cubeSet Q) MeasureTheory.volume)
(hinner_energy_le :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ → ρ₂ ≤ 1 → ∀ x ∈ scaledClosedCubeSet Q ρ₁, baseEnergy x ≤ scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(henergyAvg :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
(cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) = coarseCaccioppoliLocalizedEnergyRadiusProfile Q baseEnergy ρ₂)
(hfluxEnergy :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
CoarseCaccioppoliFluxEnergyControls Q a s (fun (x : Vec d) => matVecMul (a x) ((w ρ₁ ρ₂).toH1.grad x))
fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(hpositiveFactors : CoarseCaccioppoliBoundaryCanonicalGradientPositiveFactors Q a w)
(hgrad :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
CubeAverageGradientEnergyControl Q a (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.grad x) fun (x : Vec d) =>
scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(hprojected : CoarseCaccioppoliBoundaryCanonicalGradientProjectedPoincareFamily Q a C w i)
(hcoeff : CoarseCaccioppoliBoundaryCanonicalHarmonicCoefficientBounds Q a s t C uL2Sq w)
(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))
(hSigmaSum_t :
Summable fun (n : ℕ) =>
geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
:
coarseCaccioppoliLocalizedEnergyRadiusProfile Q baseEnergy (1 / 3) ≤ coarseCaccioppoliBoundaryExplicitHeightBound Q a s t C uL2Sq
Boundary fixed-localized-energy coarse Caccioppoli with all canonical
radius/cutoff/profile choices installed, using the canonical gradient positive
factor package directly. This is the same endpoint as the shorter wrapper
below, but it avoids splitting strict positivity into separate nonzero-energy
and lambdaSq hypotheses.
theorem
HCPolySupport.coarseCaccioppoli_interior_qone_of_canonicalHarmonicPositiveFactors
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(baseEnergy : Vec d → ℝ)
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(i : Fin d)
(hC : 0 < C)
(hs : 0 < s)
(ht : 0 < t)
(hst : s + t < 1)
(hu : 0 ≤ uL2Sq)
(hbase_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ baseEnergy x)
(hbase_int : MeasureTheory.IntegrableOn baseEnergy (cubeSet Q) MeasureTheory.volume)
(hinner_energy_le :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ → ρ₂ ≤ 1 → ∀ x ∈ scaledClosedCubeSet Q ρ₁, baseEnergy x ≤ scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(henergyAvg :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
(cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) = coarseCaccioppoliLocalizedEnergyRadiusProfile Q baseEnergy ρ₂)
(hfluxEnergy :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
CoarseCaccioppoliFluxEnergyControls Q a s (fun (x : Vec d) => matVecMul (a x) ((w ρ₁ ρ₂).toH1.grad x))
fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(hpositiveFactors : CoarseCaccioppoliBoundaryCanonicalGradientPositiveFactors Q a w)
(hgrad :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
CubeAverageGradientEnergyControl Q a (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.grad x) fun (x : Vec d) =>
scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(hprojected : CoarseCaccioppoliBoundaryCanonicalGradientProjectedPoincareFamily Q a C w i)
(hcoeff : CoarseCaccioppoliBoundaryCanonicalHarmonicCoefficientBounds Q a s t C uL2Sq w)
(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))
(hSigmaSum_t :
Summable fun (n : ℕ) =>
geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
:
coarseCaccioppoliLocalizedEnergyRadiusProfile Q baseEnergy (1 / 3) ≤ coarseCaccioppoliInteriorExplicitHeightBound Q a s t C uL2Sq
Interior fixed-localized-energy coarse Caccioppoli with all canonical radius/cutoff/profile choices installed, using the canonical gradient positive factor package directly.
theorem
HCPolySupport.coarseCaccioppoli_boundary_qone_of_canonicalHarmonicCoefficientBounds
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(baseEnergy : Vec d → ℝ)
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(i : Fin d)
(hC : 0 < C)
(hs : 0 < s)
(ht : 0 < t)
(hst : s + t < 1)
(hu : 0 ≤ uL2Sq)
(hbase_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ baseEnergy x)
(hbase_int : MeasureTheory.IntegrableOn baseEnergy (cubeSet Q) MeasureTheory.volume)
(hinner_energy_le :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ → ρ₂ ≤ 1 → ∀ x ∈ scaledClosedCubeSet Q ρ₁, baseEnergy x ≤ scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(henergyAvg :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
(cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) = coarseCaccioppoliLocalizedEnergyRadiusProfile Q baseEnergy ρ₂)
(hfluxEnergy :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
CoarseCaccioppoliFluxEnergyControls Q a s (fun (x : Vec d) => matVecMul (a x) ((w ρ₁ ρ₂).toH1.grad x))
fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(hnonzeroFactors : CoarseCaccioppoliBoundaryCanonicalGradientNonzeroEnergyFactors Q a w)
(hlambda1 : 0 < lambdaSq Q 1 (MultiscaleExponent.finite 1) a)
(hgrad :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
CubeAverageGradientEnergyControl Q a (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.grad x) fun (x : Vec d) =>
scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(hprojected : CoarseCaccioppoliBoundaryCanonicalGradientProjectedPoincareFamily Q a C w i)
(hcoeff : CoarseCaccioppoliBoundaryCanonicalHarmonicCoefficientBounds Q a s t C uL2Sq w)
(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))
(hSigmaSum_t :
Summable fun (n : ℕ) =>
geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
:
coarseCaccioppoliLocalizedEnergyRadiusProfile Q baseEnergy (1 / 3) ≤ coarseCaccioppoliBoundaryExplicitHeightBound Q a s t C uL2Sq
Boundary fixed-localized-energy coarse Caccioppoli with all canonical
radius/cutoff/profile choices installed and the remaining coefficient algebra
named as CoarseCaccioppoliBoundaryCanonicalHarmonicCoefficientBounds.
theorem
HCPolySupport.coarseCaccioppoli_interior_qone_of_canonicalHarmonicCoefficientBounds
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(baseEnergy : Vec d → ℝ)
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(i : Fin d)
(hC : 0 < C)
(hs : 0 < s)
(ht : 0 < t)
(hst : s + t < 1)
(hu : 0 ≤ uL2Sq)
(hbase_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ baseEnergy x)
(hbase_int : MeasureTheory.IntegrableOn baseEnergy (cubeSet Q) MeasureTheory.volume)
(hinner_energy_le :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ → ρ₂ ≤ 1 → ∀ x ∈ scaledClosedCubeSet Q ρ₁, baseEnergy x ≤ scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(henergyAvg :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
(cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) = coarseCaccioppoliLocalizedEnergyRadiusProfile Q baseEnergy ρ₂)
(hfluxEnergy :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
CoarseCaccioppoliFluxEnergyControls Q a s (fun (x : Vec d) => matVecMul (a x) ((w ρ₁ ρ₂).toH1.grad x))
fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(hnonzeroFactors : CoarseCaccioppoliBoundaryCanonicalGradientNonzeroEnergyFactors Q a w)
(hlambda1 : 0 < lambdaSq Q 1 (MultiscaleExponent.finite 1) a)
(hgrad :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
CubeAverageGradientEnergyControl Q a (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.grad x) fun (x : Vec d) =>
scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(hprojected : CoarseCaccioppoliBoundaryCanonicalGradientProjectedPoincareFamily Q a C w i)
(hcoeff : CoarseCaccioppoliBoundaryCanonicalHarmonicCoefficientBounds Q a s t C uL2Sq w)
(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))
(hSigmaSum_t :
Summable fun (n : ℕ) =>
geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
:
coarseCaccioppoliLocalizedEnergyRadiusProfile Q baseEnergy (1 / 3) ≤ coarseCaccioppoliInteriorExplicitHeightBound Q a s t C uL2Sq
Interior fixed-localized-energy coarse Caccioppoli with all canonical
radius/cutoff/profile choices installed and the remaining coefficient algebra
named as CoarseCaccioppoliBoundaryCanonicalHarmonicCoefficientBounds.
theorem
HCPolySupport.coarseCaccioppoli_boundary_qone_of_canonicalHarmonicAnalyticInputs
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(baseEnergy : Vec d → ℝ)
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(i : Fin d)
(hC : 0 < C)
(hs : 0 < s)
(ht : 0 < t)
(hst : s + t < 1)
(hu : 0 ≤ uL2Sq)
(hAnalytic : CoarseCaccioppoliBoundaryCanonicalHarmonicAnalyticInputs Q a s C baseEnergy w i)
(hlambda1 : 0 < lambdaSq Q 1 (MultiscaleExponent.finite 1) a)
(hcoeff : CoarseCaccioppoliBoundaryCanonicalHarmonicCoefficientBounds Q a s t C uL2Sq w)
(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))
(hSigmaSum_t :
Summable fun (n : ℕ) =>
geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
:
coarseCaccioppoliLocalizedEnergyRadiusProfile Q baseEnergy (1 / 3) ≤ coarseCaccioppoliBoundaryExplicitHeightBound Q a s t C uL2Sq
Boundary fixed-localized-energy coarse Caccioppoli with the solution-side
analytic/profile assumptions bundled into
CoarseCaccioppoliBoundaryCanonicalHarmonicAnalyticInputs.
theorem
HCPolySupport.coarseCaccioppoli_interior_qone_of_canonicalHarmonicAnalyticInputs
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(baseEnergy : Vec d → ℝ)
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(i : Fin d)
(hC : 0 < C)
(hs : 0 < s)
(ht : 0 < t)
(hst : s + t < 1)
(hu : 0 ≤ uL2Sq)
(hAnalytic : CoarseCaccioppoliBoundaryCanonicalHarmonicAnalyticInputs Q a s C baseEnergy w i)
(hlambda1 : 0 < lambdaSq Q 1 (MultiscaleExponent.finite 1) a)
(hcoeff : CoarseCaccioppoliBoundaryCanonicalHarmonicCoefficientBounds Q a s t C uL2Sq w)
(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))
(hSigmaSum_t :
Summable fun (n : ℕ) =>
geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
:
coarseCaccioppoliLocalizedEnergyRadiusProfile Q baseEnergy (1 / 3) ≤ coarseCaccioppoliInteriorExplicitHeightBound Q a s t C uL2Sq
Interior fixed-localized-energy coarse Caccioppoli with the solution-side
analytic/profile assumptions bundled into
CoarseCaccioppoliBoundaryCanonicalHarmonicAnalyticInputs.
theorem
HCPolySupport.coarseCaccioppoli_boundary_qone_of_closedCubeHarmonicEnergyControls
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(baseEnergy : Vec d → ℝ)
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(i : Fin d)
(hC : 0 < C)
(hs : 0 < s)
(ht : 0 < t)
(hst : s + t < 1)
(hu : 0 ≤ uL2Sq)
(hEllCube : IsEllipticFieldOn lam Lam (cubeSet Q) a)
(hbase_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ baseEnergy x)
(hbase_int : MeasureTheory.IntegrableOn baseEnergy (cubeSet Q) MeasureTheory.volume)
(hinner_energy_le :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ → ρ₂ ≤ 1 → ∀ x ∈ scaledClosedCubeSet Q ρ₁, baseEnergy x ≤ scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(henergyAvg :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
(cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) = coarseCaccioppoliLocalizedEnergyRadiusProfile Q baseEnergy ρ₂)
(hnonzeroFactors : CoarseCaccioppoliBoundaryCanonicalGradientNonzeroEnergyFactors Q a w)
(hlambda1 : 0 < lambdaSq Q 1 (MultiscaleExponent.finite 1) a)
(hprojected : CoarseCaccioppoliBoundaryCanonicalGradientProjectedPoincareFamily Q a C w i)
(hcoeff : CoarseCaccioppoliBoundaryCanonicalHarmonicCoefficientBounds Q a s t C uL2Sq w)
:
coarseCaccioppoliLocalizedEnergyRadiusProfile Q baseEnergy (1 / 3) ≤ coarseCaccioppoliBoundaryExplicitHeightBound Q a s t C uL2Sq
Boundary fixed-localized-energy coarse Caccioppoli where the solution-side
flux/gradient controls, descendant deterministic data, and Sigma* summability
are derived from closed-cube ellipticity and the origin recovery theorem.
This is not yet the pure open-cube note endpoint, but it removes the main energy-control bookkeeping hypotheses from the public boundary wrapper under the currently available coarse-Poincare compatibility hypothesis.
theorem
HCPolySupport.coarseCaccioppoli_interior_qone_of_closedCubeHarmonicEnergyControls
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(baseEnergy : Vec d → ℝ)
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(i : Fin d)
(hC : 0 < C)
(hs : 0 < s)
(ht : 0 < t)
(hst : s + t < 1)
(hu : 0 ≤ uL2Sq)
(hEllCube : IsEllipticFieldOn lam Lam (cubeSet Q) a)
(hbase_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ baseEnergy x)
(hbase_int : MeasureTheory.IntegrableOn baseEnergy (cubeSet Q) MeasureTheory.volume)
(hinner_energy_le :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ → ρ₂ ≤ 1 → ∀ x ∈ scaledClosedCubeSet Q ρ₁, baseEnergy x ≤ scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(henergyAvg :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
(cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) = coarseCaccioppoliLocalizedEnergyRadiusProfile Q baseEnergy ρ₂)
(hnonzeroFactors : CoarseCaccioppoliBoundaryCanonicalGradientNonzeroEnergyFactors Q a w)
(hlambda1 : 0 < lambdaSq Q 1 (MultiscaleExponent.finite 1) a)
(hprojected : CoarseCaccioppoliBoundaryCanonicalGradientProjectedPoincareFamily Q a C w i)
(hcoeff : CoarseCaccioppoliBoundaryCanonicalHarmonicCoefficientBounds Q a s t C uL2Sq w)
:
coarseCaccioppoliLocalizedEnergyRadiusProfile Q baseEnergy (1 / 3) ≤ coarseCaccioppoliInteriorExplicitHeightBound Q a s t C uL2Sq
Interior fixed-localized-energy coarse Caccioppoli with the same closed-cube compatibility discharge as the boundary wrapper above.