Coarse-graining support: #
Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.HarmonicGradientControls
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Harmonic gradient scalar-control bridges #
This file contains the Phase 2 scalar-control wrappers specialized to the
eventual Chapter 3 auxiliary scalar field g = partial_i w. It keeps the
long generic scalar-control file below the preferred size threshold while
removing routine energy hypotheses from downstream call sites.
noncomputable def
HCPolySupport.coarseCaccioppoliCanonicalGradientAcirc
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(r : ℝ)
:
Canonical scalar Acirc factor used for gradient components at regularity
r. The final harmonic-gradient wrappers specialize this at r = 1 and
r = 1 - s, so the corresponding lower-bound hypotheses become definitional.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
HCPolySupport.coarseCaccioppoliCanonicalGradientAcircOne
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
:
Radius-constant canonical Acirc factor at regularity 1.
Equations
Instances For
noncomputable def
HCPolySupport.coarseCaccioppoliCanonicalGradientAcircOneSub
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(s : ℝ)
:
Radius-constant canonical Acirc factor at regularity 1 - s.
Equations
Instances For
theorem
HCPolySupport.coarseCaccioppoliCanonicalGradientAcirc_nonneg
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
{r : ℝ}
(hr : 0 ≤ r)
:
The canonical gradient Acirc factor is nonnegative in the nonnegative
regularity range.
theorem
HCPolySupport.coarseCaccioppoliCanonicalGradientAcircOne_nonneg
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(ρ₁ ρ₂ : ℝ)
:
The canonical r = 1 gradient Acirc factor is nonnegative.
theorem
HCPolySupport.coarseCaccioppoliCanonicalGradientAcircOneSub_nonneg
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
{s : ℝ}
(hs1 : s ≤ 1)
(ρ₁ ρ₂ : ℝ)
:
The canonical r = 1 - s gradient Acirc factor is nonnegative when
s ≤ 1.
def
HCPolySupport.CoarseCaccioppoliBoundaryCanonicalGradientPositiveFactors
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
:
The strict nondegeneracy inputs still needed for the canonical gradient
Acirc specialization. Nonnegativity of the 1 - s canonical factor is
derived separately from s < 1.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
HCPolySupport.CoarseCaccioppoliBoundaryCanonicalScalarPositiveFactors.of_canonicalGradientAcirc
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(s : ℝ)
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(hs1 : s < 1)
(hpos : CoarseCaccioppoliBoundaryCanonicalGradientPositiveFactors Q a w)
:
Build the scalar-positive-factor package for the canonical gradient
Acirc factors from the genuinely strict nondegeneracy inputs.
theorem
HCPolySupport.memLp_harmonicGradientComponent_normalizedCubeMeasure
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(w : AHarmonicFunction a (openCubeSet Q))
(i : Fin d)
:
MeasureTheory.MemLp (fun (x : Vec d) => w.toH1.grad x i) 2 (normalizedCubeMeasure Q)
A component of the gradient of an open-cube harmonic function is L² for
the normalized closed-cube measure.
theorem
HCPolySupport.summable_maxDescendantSigmaStarInvNormAtScale_geometricWeight_one_of_lt
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
{t r : ℝ}
(ht : 0 < t)
(htr : t < r)
(hsum_t :
Summable fun (n : ℕ) =>
geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
:
Summable fun (n : ℕ) => geometricWeight r 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)
Summability of the sigma_*^{-1} series improves when the geometric
regularity exponent is increased.
theorem
HCPolySupport.CoarseCaccioppoliBoundaryCanonicalProjectedPoincareCircBounds.of_harmonicGradientComponent_of_fluxEnergyControls
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(s C : ℝ)
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(i : Fin d)
(Acirc1 AcircS : ℝ → ℝ → ℝ)
(hs1 : s < 1)
(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)
(hgrad :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
CubeAverageGradientEnergyControl Q a (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.grad x) fun (x : Vec d) =>
scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(hsum1 :
Summable fun (n : ℕ) =>
geometricWeight 1 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
(hsumS :
Summable fun (n : ℕ) =>
geometricWeight (1 - s) 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
(hproj :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
∀ (N : ℕ),
CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C
(cubeFluctuation Q fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.grad x i)
N)
(hAcirc1 :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
cubeBesovScaleWeight (-1) Q * ((geometricDiscount 1 1)⁻¹ * (lambdaSq Q 1 (MultiscaleExponent.finite 1) a).rpow (-1 / 2)) ≤ Acirc1 ρ₁ ρ₂)
(hAcircS :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
cubeBesovScaleWeight (-(1 - s)) Q * ((geometricDiscount (1 - s) 1)⁻¹ * (lambdaSq Q (1 - s) (MultiscaleExponent.finite 1) a).rpow (-1 / 2)) ≤ AcircS ρ₁ ρ₂)
:
CoarseCaccioppoliBoundaryCanonicalProjectedPoincareCircBounds Q a s C w
(fun (ρ₁ ρ₂ : ℝ) (x : Vec d) => (w ρ₁ ρ₂).toH1.grad x i) Acirc1 AcircS
Concrete harmonic-gradient projected/circ package using the already
available flux-energy controls to supply scalar-energy nonnegativity and
integrability. The projected mean-zero Poincare estimate for partial_i w
remains the genuine analytic input.
theorem
HCPolySupport.CoarseCaccioppoliBoundaryCanonicalProjectedPoincareCircBounds.of_harmonicGradientComponent_of_fluxEnergyControls_canonicalGradientAcirc
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(s C : ℝ)
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(i : Fin d)
(hs1 : s < 1)
(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)
(hgrad :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
CubeAverageGradientEnergyControl Q a (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.grad x) fun (x : Vec d) =>
scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(hsum1 :
Summable fun (n : ℕ) =>
geometricWeight 1 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
(hsumS :
Summable fun (n : ℕ) =>
geometricWeight (1 - s) 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
(hproj :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
∀ (N : ℕ),
CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C
(cubeFluctuation Q fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.grad x i)
N)
:
CoarseCaccioppoliBoundaryCanonicalProjectedPoincareCircBounds Q a s C w
(fun (ρ₁ ρ₂ : ℝ) (x : Vec d) => (w ρ₁ ρ₂).toH1.grad x i) (coarseCaccioppoliCanonicalGradientAcircOne Q a)
(coarseCaccioppoliCanonicalGradientAcircOneSub Q a s)
Concrete harmonic-gradient projected/circ package with the canonical
gradient Acirc factors. This removes the two explicit Acirc lower-bound
hypotheses from the projected/circ handoff.
theorem
HCPolySupport.CoarseCaccioppoliBoundaryCanonicalScalarControlFactors.of_positiveFactors_energyControls
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(s C : ℝ)
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(i : Fin d)
(Acirc1 AcircS : ℝ → ℝ → ℝ)
(hpos : CoarseCaccioppoliBoundaryCanonicalScalarPositiveFactors Q a w Acirc1 AcircS)
(hs1 : s < 1)
(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)
(hgrad :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
CubeAverageGradientEnergyControl Q a (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.grad x) fun (x : Vec d) =>
scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(hsum1 :
Summable fun (n : ℕ) =>
geometricWeight 1 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
(hsumS :
Summable fun (n : ℕ) =>
geometricWeight (1 - s) 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
(hproj :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
∀ (N : ℕ),
CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C
(cubeFluctuation Q fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.grad x i)
N)
(hAcirc1 :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
cubeBesovScaleWeight (-1) Q * ((geometricDiscount 1 1)⁻¹ * (lambdaSq Q 1 (MultiscaleExponent.finite 1) a).rpow (-1 / 2)) ≤ Acirc1 ρ₁ ρ₂)
(hAcircS :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
cubeBesovScaleWeight (-(1 - s)) Q * ((geometricDiscount (1 - s) 1)⁻¹ * (lambdaSq Q (1 - s) (MultiscaleExponent.finite 1) a).rpow (-1 / 2)) ≤ AcircS ρ₁ ρ₂)
:
CoarseCaccioppoliBoundaryCanonicalScalarControlFactors Q a s C w
(fun (ρ₁ ρ₂ : ℝ) (x : Vec d) => (w ρ₁ ρ₂).toH1.grad x i) Acirc1 AcircS
Full scalar-control factors for g = partial_i w, with scalar-energy
nonnegativity/integrability taken from the flux-energy controls already used
by the single-cube Caccioppoli bridge.
theorem
HCPolySupport.CoarseCaccioppoliBoundaryCanonicalScalarControlFactors.of_gradientFluxEnergyControls
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(s C : ℝ)
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(i : Fin d)
(hpos : CoarseCaccioppoliBoundaryCanonicalGradientPositiveFactors Q a w)
(hs1 : s < 1)
(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)
(hgrad :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
CubeAverageGradientEnergyControl Q a (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.grad x) fun (x : Vec d) =>
scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(hsum1 :
Summable fun (n : ℕ) =>
geometricWeight 1 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
(hsumS :
Summable fun (n : ℕ) =>
geometricWeight (1 - s) 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
(hproj :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
∀ (N : ℕ),
CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C
(cubeFluctuation Q fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.grad x i)
N)
:
CoarseCaccioppoliBoundaryCanonicalScalarControlFactors Q a s C w
(fun (ρ₁ ρ₂ : ℝ) (x : Vec d) => (w ρ₁ ρ₂).toH1.grad x i) (coarseCaccioppoliCanonicalGradientAcircOne Q a)
(coarseCaccioppoliCanonicalGradientAcircOneSub Q a s)
Full scalar-control factors for g = partial_i w with the canonical
gradient Acirc factors.
theorem
HCPolySupport.coarseCaccioppoli_boundary_qone_of_quantitativeCutoff_of_of_coefficientBounds
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(k : ℝ → ℝ → ℕ)
{F : ℝ → ℝ}
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(i : Fin d)
(Acirc1 AcircS U A1 AS : ℝ → ℝ → ℝ)
(hC : 0 < C)
(hs : 0 < s)
(ht : 0 < t)
(hst : s + t < 1)
(hu : 0 ≤ uL2Sq)
(hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ)
(hbounded : CoarseCaccioppoliRadiusBoundedAbove F)
(hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂)
(hlower :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
F ρ₁ ≤ cubeAverage Q fun (x : Vec d) =>
QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂ x * scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(henergyAvg :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ → ρ₂ ≤ 1 → (cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) = F ρ₂)
(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 : CoarseCaccioppoliBoundaryCanonicalScalarPositiveFactors Q a w Acirc1 AcircS)
(hgrad :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
CubeAverageGradientEnergyControl Q a (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.grad x) fun (x : Vec d) =>
scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(hproj :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
∀ (N : ℕ),
CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C
(cubeFluctuation Q fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.grad x i)
N)
(hAcirc1_lower :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
cubeBesovScaleWeight (-1) Q * ((geometricDiscount 1 1)⁻¹ * (lambdaSq Q 1 (MultiscaleExponent.finite 1) a).rpow (-1 / 2)) ≤ Acirc1 ρ₁ ρ₂)
(hAcircS_lower :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
cubeBesovScaleWeight (-(1 - s)) Q * ((geometricDiscount (1 - s) 1)⁻¹ * (lambdaSq Q (1 - s) (MultiscaleExponent.finite 1) a).rpow (-1 / 2)) ≤ AcircS ρ₁ ρ₂)
(hU :
∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → (cubeLpNorm Q 2 fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) ≤ U ρ₁ ρ₂)
(hA1 : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → Acirc1 ρ₁ ρ₂ ≤ A1 ρ₁ ρ₂)
(hAS : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → AcircS ρ₁ ρ₂ ≤ AS ρ₁ ρ₂)
(hcoeff :
CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalCoefficientBounds Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂))
(coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) U
(coarseCaccioppoliQuantitativeCutoffGradientBound Q) (coarseCaccioppoliQuantitativeCutoffHessianBound Q) A1 AS)
(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))
:
Boundary canonical harmonic Caccioppoli specialized to the concrete scalar
auxiliary field g = partial_i w. The theorem builds the projected/circ
package from flux-energy controls plus gradient-energy controls; projected
mean-zero Poincare for partial_i w is still an explicit analytic input.
theorem
HCPolySupport.coarseCaccioppoli_interior_qone_of_quantitativeCutoff_of_of_coefficientBounds
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(k : ℝ → ℝ → ℕ)
{F G₀ : ℝ → ℝ}
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(i : Fin d)
(Acirc1 AcircS U A1 AS : ℝ → ℝ → ℝ)
(hC : 0 < C)
(hs : 0 < s)
(ht : 0 < t)
(hst : s + t < 1)
(hu : 0 ≤ uL2Sq)
(hagree : CoarseCaccioppoliRadiusAgreement F G₀)
(hG_nonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ G₀ ρ)
(hG_bounded : CoarseCaccioppoliRadiusBoundedAbove G₀)
(hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂)
(hlower :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
G₀ ρ₁ ≤ cubeAverage Q fun (x : Vec d) =>
QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂ x * scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(henergyAvg :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ → ρ₂ ≤ 1 → (cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) = G₀ ρ₂)
(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 : CoarseCaccioppoliBoundaryCanonicalScalarPositiveFactors Q a w Acirc1 AcircS)
(hgrad :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
CubeAverageGradientEnergyControl Q a (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.grad x) fun (x : Vec d) =>
scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(hproj :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
∀ (N : ℕ),
CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C
(cubeFluctuation Q fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.grad x i)
N)
(hAcirc1_lower :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
cubeBesovScaleWeight (-1) Q * ((geometricDiscount 1 1)⁻¹ * (lambdaSq Q 1 (MultiscaleExponent.finite 1) a).rpow (-1 / 2)) ≤ Acirc1 ρ₁ ρ₂)
(hAcircS_lower :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
cubeBesovScaleWeight (-(1 - s)) Q * ((geometricDiscount (1 - s) 1)⁻¹ * (lambdaSq Q (1 - s) (MultiscaleExponent.finite 1) a).rpow (-1 / 2)) ≤ AcircS ρ₁ ρ₂)
(hU :
∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → (cubeLpNorm Q 2 fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) ≤ U ρ₁ ρ₂)
(hA1 : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → Acirc1 ρ₁ ρ₂ ≤ A1 ρ₁ ρ₂)
(hAS : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → AcircS ρ₁ ρ₂ ≤ AS ρ₁ ρ₂)
(hcoeff :
CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalCoefficientBounds Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂))
(coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) U
(coarseCaccioppoliQuantitativeCutoffGradientBound Q) (coarseCaccioppoliQuantitativeCutoffHessianBound Q) A1 AS)
(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
g = partial_i w.
theorem
HCPolySupport.coarseCaccioppoli_boundary_qone_of_quantitativeCutoff_of_projectedPoincare
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(k : ℝ → ℝ → ℕ)
{F : ℝ → ℝ}
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(i : Fin d)
(U A1 AS : ℝ → ℝ → ℝ)
(hC : 0 < C)
(hs : 0 < s)
(ht : 0 < t)
(hst : s + t < 1)
(hu : 0 ≤ uL2Sq)
(hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ)
(hbounded : CoarseCaccioppoliRadiusBoundedAbove F)
(hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂)
(hlower :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
F ρ₁ ≤ cubeAverage Q fun (x : Vec d) =>
QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂ x * scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(henergyAvg :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ → ρ₂ ≤ 1 → (cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) = F ρ₂)
(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)
(hproj :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
∀ (N : ℕ),
CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C
(cubeFluctuation Q fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.grad x i)
N)
(hU :
∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → (cubeLpNorm Q 2 fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) ≤ U ρ₁ ρ₂)
(hA1 : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → coarseCaccioppoliCanonicalGradientAcircOne Q a ρ₁ ρ₂ ≤ A1 ρ₁ ρ₂)
(hAS :
∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → coarseCaccioppoliCanonicalGradientAcircOneSub Q a s ρ₁ ρ₂ ≤ AS ρ₁ ρ₂)
(hcoeff :
CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalCoefficientBounds Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂))
(coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) U
(coarseCaccioppoliQuantitativeCutoffGradientBound Q) (coarseCaccioppoliQuantitativeCutoffHessianBound Q) A1 AS)
(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))
:
Boundary canonical harmonic Caccioppoli specialized to the canonical
gradient Acirc factors. Compared with
...of_harmonicGradientComponent..., the Acirc lower-bound hypotheses are
now definitional.
theorem
HCPolySupport.coarseCaccioppoli_interior_qone_of_quantitativeCutoff_of_projectedPoincare
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(k : ℝ → ℝ → ℕ)
{F G₀ : ℝ → ℝ}
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(i : Fin d)
(U A1 AS : ℝ → ℝ → ℝ)
(hC : 0 < C)
(hs : 0 < s)
(ht : 0 < t)
(hst : s + t < 1)
(hu : 0 ≤ uL2Sq)
(hagree : CoarseCaccioppoliRadiusAgreement F G₀)
(hG_nonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ G₀ ρ)
(hG_bounded : CoarseCaccioppoliRadiusBoundedAbove G₀)
(hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂)
(hlower :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
G₀ ρ₁ ≤ cubeAverage Q fun (x : Vec d) =>
QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂ x * scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(henergyAvg :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ → ρ₂ ≤ 1 → (cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) = G₀ ρ₂)
(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)
(hproj :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
∀ (N : ℕ),
CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C
(cubeFluctuation Q fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.grad x i)
N)
(hU :
∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → (cubeLpNorm Q 2 fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) ≤ U ρ₁ ρ₂)
(hA1 : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → coarseCaccioppoliCanonicalGradientAcircOne Q a ρ₁ ρ₂ ≤ A1 ρ₁ ρ₂)
(hAS :
∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → coarseCaccioppoliCanonicalGradientAcircOneSub Q a s ρ₁ ρ₂ ≤ AS ρ₁ ρ₂)
(hcoeff :
CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalCoefficientBounds Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂))
(coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) U
(coarseCaccioppoliQuantitativeCutoffGradientBound Q) (coarseCaccioppoliQuantitativeCutoffHessianBound Q) A1 AS)
(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 the canonical
gradient Acirc factors.
theorem
HCPolySupport.coarseCaccioppoli_boundary_qone_of_quantitativeCutoff_of_of_harmonicFamily
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(k : ℝ → ℝ → ℕ)
{F : ℝ → ℝ}
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(i : Fin d)
(U : ℝ → ℝ → ℝ)
(hC : 0 < C)
(hs : 0 < s)
(ht : 0 < t)
(hst : s + t < 1)
(hu : 0 ≤ uL2Sq)
(hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ)
(hbounded : CoarseCaccioppoliRadiusBoundedAbove F)
(hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂)
(hlower :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
F ρ₁ ≤ cubeAverage Q fun (x : Vec d) =>
QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂ x * scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(henergyAvg :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ → ρ₂ ≤ 1 → (cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) = F ρ₂)
(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)
(hproj :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
∀ (N : ℕ),
CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C
(cubeFluctuation Q fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.grad x i)
N)
(hU :
∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → (cubeLpNorm Q 2 fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) ≤ U ρ₁ ρ₂)
(hcoeff :
CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalCoefficientBounds Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂))
(coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) U
(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))
:
Boundary canonical harmonic Caccioppoli with the canonical gradient
Acirc factors also installed in the coefficient-bound package. This removes
the caller-facing hA1 and hAS comparison hypotheses from the canonical
gradient endpoint.
theorem
HCPolySupport.coarseCaccioppoli_interior_qone_of_quantitativeCutoff_of_of_harmonicFamily
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(k : ℝ → ℝ → ℕ)
{F G₀ : ℝ → ℝ}
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(i : Fin d)
(U : ℝ → ℝ → ℝ)
(hC : 0 < C)
(hs : 0 < s)
(ht : 0 < t)
(hst : s + t < 1)
(hu : 0 ≤ uL2Sq)
(hagree : CoarseCaccioppoliRadiusAgreement F G₀)
(hG_nonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ G₀ ρ)
(hG_bounded : CoarseCaccioppoliRadiusBoundedAbove G₀)
(hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂)
(hlower :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
G₀ ρ₁ ≤ cubeAverage Q fun (x : Vec d) =>
QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂ x * scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(henergyAvg :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ → ρ₂ ≤ 1 → (cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) = G₀ ρ₂)
(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)
(hproj :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
∀ (N : ℕ),
CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C
(cubeFluctuation Q fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.grad x i)
N)
(hU :
∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → (cubeLpNorm Q 2 fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) ≤ U ρ₁ ρ₂)
(hcoeff :
CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalCoefficientBounds Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂))
(coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) U
(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 with the canonical gradient
Acirc factors also installed in the coefficient-bound package.