Coarse-graining support: #
Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.HarmonicFinal.CorePositiveFactors
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.coarseCaccioppoli_boundary_qone_of_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)
(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 the canonical raw
coefficient bounds. Compared with the coefficient-bound wrapper below, the
multiscale localization data has already been absorbed into hrawcoeff.
theorem
HCPolySupport.CoarseCaccioppoliBoundaryCanonicalHarmonicVectorNoteRawBridge.of_coefficientBounds
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(baseEnergy : Vec d → ℝ)
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(hC : 0 < C)
(hs : 0 < s)
(ht : 0 < t)
(hst : s + t < 1)
(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 : CoarseCaccioppoliBoundaryCanonicalGradientProjectedPoincareVectorFamily Q a C w)
(hrawcoeff :
CoarseCaccioppoliBoundaryCanonicalHarmonicRawCoefficientBounds Q a s t (↑(Fintype.card (Fin d)) * 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))
:
CoarseCaccioppoliBoundaryCanonicalHarmonicVectorNoteRawBridge Q a s t C uL2Sq baseEnergy
Sequence-local note raw bridge from the vector projected-Poincare family
and canonical raw coefficient bounds stated for the effective scalar-facing
constant (Fintype.card (Fin d) : ℝ) * C.
This is the note-faithful bridge: it proves the local recurrence on the Chapter-3 radius sequence before the recurrence is summed.
theorem
HCPolySupport.coarseCaccioppoli_boundary_qone_of_canonicalHarmonicVectorPositiveFactors
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(baseEnergy : Vec d → ℝ)
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(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 : CoarseCaccioppoliBoundaryCanonicalGradientProjectedPoincareVectorFamily Q a C w)
(hrawcoeff :
CoarseCaccioppoliBoundaryCanonicalHarmonicRawCoefficientBounds Q a s t (↑(Fintype.card (Fin d)) * 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 (↑(Fintype.card (Fin d)) * C) uL2Sq
Boundary fixed-localized-energy coarse Caccioppoli from the vector
projected-Poincare family and canonical raw coefficient bounds stated for the
effective scalar-facing constant (Fintype.card (Fin d) : ℝ) * C.
This is the note-facing replacement for the old componentwise projected Poincare endpoint.
theorem
HCPolySupport.coarseCaccioppoli_interior_qone_of_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)
(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 the canonical raw coefficient bounds.