Coarse-graining support: #
Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.HarmonicCanonicalGradient.Specializations
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.coarseCaccioppoli_interior_qone_of_quantitativeCutoff_of_fixedEnergyProfile
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(k : ℝ → ℝ → ℕ)
{F : ℝ → ℝ}
(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)
(hagree : CoarseCaccioppoliRadiusAgreement F (coarseCaccioppoliLocalizedEnergyRadiusProfile Q baseEnergy))
(hbase_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ baseEnergy x)
(hbase_int : MeasureTheory.IntegrableOn baseEnergy (cubeSet Q) MeasureTheory.volume)
(hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂)
(hinner_energy :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
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 :
CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalCoefficientBounds Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂))
(coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k)
(coarseCaccioppoliCanonicalHarmonicL2Profile Q a w) (coarseCaccioppoliQuantitativeCutoffGradientBound Q)
(coarseCaccioppoliQuantitativeCutoffHessianBound Q) (coarseCaccioppoliCanonicalGradientAcircOne Q a)
(coarseCaccioppoliCanonicalGradientAcircOneSub Q a s))
(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))
:
Interior canonical harmonic Caccioppoli specialized to a fixed localized energy radius profile for the centered quantity.
theorem
HCPolySupport.coarseCaccioppoliInteriorExponentOne_of_fixedLocalizedEnergyProfile
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(k : ℝ → ℝ → ℕ)
(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)
(hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂)
(hinner_energy :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
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 :
CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalCoefficientBounds Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂))
(coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k)
(coarseCaccioppoliCanonicalHarmonicL2Profile Q a w) (coarseCaccioppoliQuantitativeCutoffGradientBound Q)
(coarseCaccioppoliQuantitativeCutoffHessianBound Q) (coarseCaccioppoliCanonicalGradientAcircOne Q a)
(coarseCaccioppoliCanonicalGradientAcircOneSub Q a s))
(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 canonical harmonic Caccioppoli with the interior iterated radius
profile specialized directly to the fixed localized energy profile. This is
the no-public-hagree version of the fixed-profile wrapper.
theorem
HCPolySupport.coarseCaccioppoli_boundary_qone_of_quantitativeCutoff_of_triadicGapScale
{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 :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
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 :
CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalCoefficientBounds Q a s C uL2Sq
(fun (ρ₁ ρ₂ : ℝ) => ↑(coarseCaccioppoliTriadicGapScale ρ₁ ρ₂))
(coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C coarseCaccioppoliTriadicGapScale)
(coarseCaccioppoliCanonicalHarmonicL2Profile Q a w) (coarseCaccioppoliQuantitativeCutoffGradientBound Q)
(coarseCaccioppoliQuantitativeCutoffHessianBound Q) (coarseCaccioppoliCanonicalGradientAcircOne Q a)
(coarseCaccioppoliCanonicalGradientAcircOneSub Q a s))
(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 canonical harmonic Caccioppoli with the canonical Chapter 3 triadic gap scale installed.
theorem
HCPolySupport.coarseCaccioppoli_interior_qone_of_quantitativeCutoff_of_triadicGapScale
{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 :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
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 :
CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalCoefficientBounds Q a s C uL2Sq
(fun (ρ₁ ρ₂ : ℝ) => ↑(coarseCaccioppoliTriadicGapScale ρ₁ ρ₂))
(coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C coarseCaccioppoliTriadicGapScale)
(coarseCaccioppoliCanonicalHarmonicL2Profile Q a w) (coarseCaccioppoliQuantitativeCutoffGradientBound Q)
(coarseCaccioppoliQuantitativeCutoffHessianBound Q) (coarseCaccioppoliCanonicalGradientAcircOne Q a)
(coarseCaccioppoliCanonicalGradientAcircOneSub Q a s))
(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 canonical harmonic Caccioppoli with both the fixed profile and canonical Chapter 3 triadic gap scale installed.
theorem
HCPolySupport.coarseCaccioppoli_boundary_qone_of_quantitativeCutoff_of_of_positiveFactors
{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 :
CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalCoefficientBounds Q a s C uL2Sq
(fun (ρ₁ ρ₂ : ℝ) => ↑(coarseCaccioppoliTriadicGapScale ρ₁ ρ₂))
(coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C coarseCaccioppoliTriadicGapScale)
(coarseCaccioppoliCanonicalHarmonicL2Profile Q a w) (coarseCaccioppoliQuantitativeCutoffGradientBound Q)
(coarseCaccioppoliQuantitativeCutoffHessianBound Q) (coarseCaccioppoliCanonicalGradientAcircOne Q a)
(coarseCaccioppoliCanonicalGradientAcircOneSub Q a s))
(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 canonical harmonic Caccioppoli with the canonical Chapter 3 triadic gap scale installed, requiring only domination of the fixed localized energy by the pair-dependent energy on each inner cube.
theorem
HCPolySupport.coarseCaccioppoli_interior_qone_of_quantitativeCutoff_of_of_positiveFactors
{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 :
CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalCoefficientBounds Q a s C uL2Sq
(fun (ρ₁ ρ₂ : ℝ) => ↑(coarseCaccioppoliTriadicGapScale ρ₁ ρ₂))
(coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C coarseCaccioppoliTriadicGapScale)
(coarseCaccioppoliCanonicalHarmonicL2Profile Q a w) (coarseCaccioppoliQuantitativeCutoffGradientBound Q)
(coarseCaccioppoliQuantitativeCutoffHessianBound Q) (coarseCaccioppoliCanonicalGradientAcircOne Q a)
(coarseCaccioppoliCanonicalGradientAcircOneSub Q a s))
(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 canonical harmonic Caccioppoli with the canonical Chapter 3 triadic gap scale installed, requiring only domination of the fixed localized energy by the pair-dependent energy on each inner cube.