Coarse-graining support: #
Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.HarmonicScalarControls
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Harmonic scalar-control factors #
This file packages the remaining Phase 2 scalar-control primitives for the
canonical harmonic coarse-Caccioppoli wrappers. The raw bundled hypothesis
CoarseCaccioppoliScalarCutoffControls has already been removed from the
strongest localization-data endpoints; this sidecar replaces the two exact
cutoff-size positivity hypotheses by simpler positive factor assumptions.
theorem
HCPolySupport.memLp_normalizedCubeMeasure_of_memVectorL2_openCubeSet
{d : ℕ}
(Q : TriadicCube d)
{f : Vec d → Vec d}
(hf : MemVectorL2 (openCubeSet Q) f)
:
Vector L² data on the open cube also gives L² data for the normalized
closed-cube measure.
theorem
HCPolySupport.memLp_normalizedCubeMeasure_of_memL2On_openCubeSet
{d : ℕ}
(Q : TriadicCube d)
{f : Vec d → ℝ}
(hf : MemL2On (openCubeSet Q) f)
:
Scalar L² data on the open cube also gives L² data for the normalized
closed-cube measure.
theorem
HCPolySupport.memLp_harmonicFunction_normalizedCubeMeasure
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(w : AHarmonicFunction a (openCubeSet Q))
:
MeasureTheory.MemLp (fun (x : Vec d) => w.toH1.toFun x) 2 (normalizedCubeMeasure Q)
An open-cube harmonic function is L² for the normalized closed-cube
measure.
theorem
HCPolySupport.memLp_harmonicFlux_normalizedCubeMeasure
{d : ℕ}
{lam Lam : ℝ}
(Q : TriadicCube d)
(a : CoeffField d)
(w : AHarmonicFunction a (openCubeSet Q))
(hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a)
:
MeasureTheory.MemLp (fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x)) 2 (normalizedCubeMeasure Q)
The flux of an open-cube harmonic function is L² for the normalized
closed-cube measure under ellipticity.
theorem
HCPolySupport.summable_bBlock_geometricWeight_s_of_fluxEnergyControls_family
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(s : ℝ)
{flux : ℝ → ℝ → Vec d → Vec d}
{energy : ℝ → ℝ → Vec d → ℝ}
(hfluxEnergy :
∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliFluxEnergyControls Q a s (flux ρ₁ ρ₂) (energy ρ₁ ρ₂))
:
Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)
The flux-energy package already includes the B-coefficient summability
needed by the final radius bridge. A single fixed admissible radius pair is
enough because this summability does not depend on the radius pair.
def
HCPolySupport.CoarseCaccioppoliBoundaryCanonicalScalarControlFactors
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(s C : ℝ)
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(g : ℝ → ℝ → Vec d → ℝ)
(Acirc1 AcircS : ℝ → ℝ → ℝ)
:
Radius-wise primitive data that generate the scalar cutoff-control bundle for the canonical Chapter 3 cutoff.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
HCPolySupport.CoarseCaccioppoliBoundaryCanonicalScalarPositiveFactors
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(Acirc1 AcircS : ℝ → ℝ → ℝ)
:
The nondegeneracy/positivity part of the canonical scalar-control factors.
This is deliberately separated from the actual projected-Poincare/circ content: the latter is the real Besov/Poincare input for Phase 2.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
HCPolySupport.CoarseCaccioppoliBoundaryCanonicalProjectedPoincareCircBounds
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(s C : ℝ)
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(g : ℝ → ℝ → Vec d → ℝ)
(Acirc1 AcircS : ℝ → ℝ → ℝ)
:
The actual projected-Poincare and circ estimates needed for Phase 2.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
HCPolySupport.CoarseCaccioppoliBoundaryCanonicalScalarPositiveFactors.cubeLpNorm_pos
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q)}
{Acirc1 AcircS : ℝ → ℝ → ℝ}
(hpos : CoarseCaccioppoliBoundaryCanonicalScalarPositiveFactors Q a w Acirc1 AcircS)
{ρ₁ ρ₂ : ℝ}
(hρ₁ : 1 / 3 ≤ ρ₁)
(hlt : ρ₁ < ρ₂)
(hρ₂ : ρ₂ ≤ 1)
:
theorem
HCPolySupport.CoarseCaccioppoliBoundaryCanonicalScalarPositiveFactors.acirc1_pos
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q)}
{Acirc1 AcircS : ℝ → ℝ → ℝ}
(hpos : CoarseCaccioppoliBoundaryCanonicalScalarPositiveFactors Q a w Acirc1 AcircS)
{ρ₁ ρ₂ : ℝ}
(hρ₁ : 1 / 3 ≤ ρ₁)
(hlt : ρ₁ < ρ₂)
(hρ₂ : ρ₂ ≤ 1)
:
theorem
HCPolySupport.CoarseCaccioppoliBoundaryCanonicalScalarPositiveFactors.acirc1_nonneg
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q)}
{Acirc1 AcircS : ℝ → ℝ → ℝ}
(hpos : CoarseCaccioppoliBoundaryCanonicalScalarPositiveFactors Q a w Acirc1 AcircS)
{ρ₁ ρ₂ : ℝ}
(hρ₁ : 1 / 3 ≤ ρ₁)
(hlt : ρ₁ < ρ₂)
(hρ₂ : ρ₂ ≤ 1)
:
theorem
HCPolySupport.CoarseCaccioppoliBoundaryCanonicalScalarPositiveFactors.acircS_nonneg
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q)}
{Acirc1 AcircS : ℝ → ℝ → ℝ}
(hpos : CoarseCaccioppoliBoundaryCanonicalScalarPositiveFactors Q a w Acirc1 AcircS)
{ρ₁ ρ₂ : ℝ}
(hρ₁ : 1 / 3 ≤ ρ₁)
(hlt : ρ₁ < ρ₂)
(hρ₂ : ρ₂ ≤ 1)
:
theorem
HCPolySupport.CoarseCaccioppoliBoundaryCanonicalScalarPositiveFactors.energySqrt_pos
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q)}
{Acirc1 AcircS : ℝ → ℝ → ℝ}
(hpos : CoarseCaccioppoliBoundaryCanonicalScalarPositiveFactors Q a w Acirc1 AcircS)
{ρ₁ ρ₂ : ℝ}
(hρ₁ : 1 / 3 ≤ ρ₁)
(hlt : ρ₁ < ρ₂)
(hρ₂ : ρ₂ ≤ 1)
:
theorem
HCPolySupport.CoarseCaccioppoliBoundaryCanonicalProjectedPoincareCircBounds.projectedPoincare
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{s C : ℝ}
{w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q)}
{g : ℝ → ℝ → Vec d → ℝ}
{Acirc1 AcircS : ℝ → ℝ → ℝ}
(hctrl : CoarseCaccioppoliBoundaryCanonicalProjectedPoincareCircBounds Q a s C w g Acirc1 AcircS)
{ρ₁ ρ₂ : ℝ}
(hρ₁ : 1 / 3 ≤ ρ₁)
(hlt : ρ₁ < ρ₂)
(hρ₂ : ρ₂ ≤ 1)
(N : ℕ)
:
CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C (cubeFluctuation Q fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x)
(g ρ₁ ρ₂) N
theorem
HCPolySupport.CoarseCaccioppoliBoundaryCanonicalProjectedPoincareCircBounds.circPartialNorm_one_le
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{s C : ℝ}
{w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q)}
{g : ℝ → ℝ → Vec d → ℝ}
{Acirc1 AcircS : ℝ → ℝ → ℝ}
(hctrl : CoarseCaccioppoliBoundaryCanonicalProjectedPoincareCircBounds Q a s C w g Acirc1 AcircS)
{ρ₁ ρ₂ : ℝ}
(hρ₁ : 1 / 3 ≤ ρ₁)
(hlt : ρ₁ < ρ₂)
(hρ₂ : ρ₂ ≤ 1)
(N : ℕ)
:
cubeBesovCircPartialNorm Q 1 2 1 N (g ρ₁ ρ₂) ≤ Acirc1 ρ₁ ρ₂ * √(cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
theorem
HCPolySupport.CoarseCaccioppoliBoundaryCanonicalProjectedPoincareCircBounds.circPartialNorm_one_sub_le
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{s C : ℝ}
{w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q)}
{g : ℝ → ℝ → Vec d → ℝ}
{Acirc1 AcircS : ℝ → ℝ → ℝ}
(hctrl : CoarseCaccioppoliBoundaryCanonicalProjectedPoincareCircBounds Q a s C w g Acirc1 AcircS)
{ρ₁ ρ₂ : ℝ}
(hρ₁ : 1 / 3 ≤ ρ₁)
(hlt : ρ₁ < ρ₂)
(hρ₂ : ρ₂ ≤ 1)
(N : ℕ)
:
cubeBesovCircPartialNorm Q (1 - s) 2 1 N (g ρ₁ ρ₂) ≤ AcircS ρ₁ ρ₂ * √(cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
theorem
HCPolySupport.CoarseCaccioppoliBoundaryCanonicalProjectedPoincareCircBounds.of_component_negativeVectorBounds
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(s C : ℝ)
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(G : ℝ → ℝ → Vec d → Vec d)
(i : Fin d)
(Acirc1 AcircS : ℝ → ℝ → ℝ)
(hproj :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
∀ (N : ℕ),
CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C
(cubeFluctuation Q fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) (fun (x : Vec d) => G ρ₁ ρ₂ x i) N)
(hneg1 :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
∀ (N : ℕ),
cubeBesovScaleWeight (-1) Q * cubeBesovNegativeVectorPartialSeminorm Q 1 N (G ρ₁ ρ₂) ≤ Acirc1 ρ₁ ρ₂ * √(cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x))
(hnegS :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
∀ (N : ℕ),
cubeBesovScaleWeight (-(1 - s)) Q * cubeBesovNegativeVectorPartialSeminorm Q (1 - s) N (G ρ₁ ρ₂) ≤ AcircS ρ₁ ρ₂ * √(cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x))
:
CoarseCaccioppoliBoundaryCanonicalProjectedPoincareCircBounds Q a s C w (fun (ρ₁ ρ₂ : ℝ) (x : Vec d) => G ρ₁ ρ₂ x i)
Acirc1 AcircS
Build the projected-Poincare/circ package when the scalar auxiliary
field is one component of a vector field whose negative Besov partial seminorms
already dominate the desired circ factors. This is the local scalarization
bridge used before the final concrete choice of g is fixed.
theorem
HCPolySupport.CoarseCaccioppoliBoundaryCanonicalProjectedPoincareCircBounds.of_component_gradientEnergyControl
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(s C : ℝ)
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(G : ℝ → ℝ → Vec d → Vec d)
(i : Fin d)
(Acirc1 AcircS : ℝ → ℝ → ℝ)
(hs1 : s < 1)
(henergy_nonneg :
∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → ∀ x ∈ cubeSet Q, 0 ≤ scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(henergy_int :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
MeasureTheory.IntegrableOn (fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) (cubeSet Q)
MeasureTheory.volume)
(hgrad :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
CubeAverageGradientEnergyControl Q a (G ρ₁ ρ₂) 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) => G ρ₁ ρ₂ 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) => G ρ₁ ρ₂ x i)
Acirc1 AcircS
Build the projected-Poincare/circ package for a component of a vector
field whose descendant gradient-energy controls supply the note's lambdaSq
factors. This is the concrete gradient-side scalarization bridge; the
projected mean-zero Poincare family remains as the analytic input.
theorem
HCPolySupport.CoarseCaccioppoliBoundaryCanonicalProjectedPoincareCircBounds.of_harmonicGradientComponent
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(s C : ℝ)
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(i : Fin d)
(Acirc1 AcircS : ℝ → ℝ → ℝ)
(hs1 : s < 1)
(henergy_nonneg :
∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → ∀ x ∈ cubeSet Q, 0 ≤ scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(henergy_int :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
MeasureTheory.IntegrableOn (fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) (cubeSet Q)
MeasureTheory.volume)
(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 version of
CoarseCaccioppoliBoundaryCanonicalProjectedPoincareCircBounds.of_component_gradientEnergyControl.
Once the projected mean-zero Poincare family is available for the component
∂ᵢ w, the gradient-energy bridge supplies both scalar circ estimates for
that same component.
theorem
HCPolySupport.CoarseCaccioppoliBoundaryCanonicalScalarControlFactors.of_positiveFactors_of_projectedPoincareCircBounds
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(s C : ℝ)
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(g : ℝ → ℝ → Vec d → ℝ)
(Acirc1 AcircS : ℝ → ℝ → ℝ)
(hpos : CoarseCaccioppoliBoundaryCanonicalScalarPositiveFactors Q a w Acirc1 AcircS)
(hctrl : CoarseCaccioppoliBoundaryCanonicalProjectedPoincareCircBounds Q a s C w g Acirc1 AcircS)
:
CoarseCaccioppoliBoundaryCanonicalScalarControlFactors Q a s C w g Acirc1 AcircS
theorem
HCPolySupport.CoarseCaccioppoliBoundaryCanonicalScalarControlFactors.of_positiveFactors_gradientComponent
{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)
(henergy_nonneg :
∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → ∀ x ∈ cubeSet Q, 0 ≤ scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(henergy_int :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
MeasureTheory.IntegrableOn (fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) (cubeSet Q)
MeasureTheory.volume)
(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 the concrete scalar field partial_i w.
This is the Phase 2 bridge used by the final Caccioppoli wrappers once the
projected mean-zero Poincare estimate for partial_i w has been supplied.
theorem
HCPolySupport.CoarseCaccioppoliBoundaryCanonicalScalarControlFactors.to_scalarCutoffControls
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
{s C ρ₁ ρ₂ : ℝ}
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(g : ℝ → ℝ → Vec d → ℝ)
(Acirc1 AcircS : ℝ → ℝ → ℝ)
(hfactors : CoarseCaccioppoliBoundaryCanonicalScalarControlFactors Q a s C w g Acirc1 AcircS)
(hs0 : 0 < s)
(hs1 : s < 1)
(hC : 0 < C)
(hρ₁ : 1 / 3 ≤ ρ₁)
(hlt : ρ₁ < ρ₂)
(hρ₂ : ρ₂ ≤ 1)
:
CoarseCaccioppoliScalarCutoffControls Q s (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) (g ρ₁ ρ₂)
(scalarCutoffGradientField (QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂))
(fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) (Acirc1 ρ₁ ρ₂) (AcircS ρ₁ ρ₂)
(coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ ρ₂) C
theorem
HCPolySupport.CoarseCaccioppoliBoundaryCanonicalScalarControlFactors.acirc1_nonneg
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
{s C ρ₁ ρ₂ : ℝ}
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(g : ℝ → ℝ → Vec d → ℝ)
(Acirc1 AcircS : ℝ → ℝ → ℝ)
(hfactors : CoarseCaccioppoliBoundaryCanonicalScalarControlFactors Q a s C w g Acirc1 AcircS)
(hρ₁ : 1 / 3 ≤ ρ₁)
(hlt : ρ₁ < ρ₂)
(hρ₂ : ρ₂ ≤ 1)
:
theorem
HCPolySupport.CoarseCaccioppoliBoundaryCanonicalScalarControlFactors.acircS_nonneg
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
{s C ρ₁ ρ₂ : ℝ}
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(g : ℝ → ℝ → Vec d → ℝ)
(Acirc1 AcircS : ℝ → ℝ → ℝ)
(hfactors : CoarseCaccioppoliBoundaryCanonicalScalarControlFactors Q a s C w g Acirc1 AcircS)
(hρ₁ : 1 / 3 ≤ ρ₁)
(hlt : ρ₁ < ρ₂)
(hρ₂ : ρ₂ ≤ 1)
:
theorem
HCPolySupport.coarseCaccioppoli_boundary_qone_of_quantitativeCutoff_of_of_scalarControlFactors
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(k : ℝ → ℝ → ℕ)
{F : ℝ → ℝ}
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(g : ℝ → ℝ → Vec 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 ρ₂)
(hgMem : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → MeasureTheory.MemLp (g ρ₁ ρ₂) 2 (normalizedCubeMeasure Q))
(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)
(hscalarFactors : CoarseCaccioppoliBoundaryCanonicalScalarControlFactors Q a s C w g Acirc1 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 from primitive scalar-control factors, without exposing the raw scalar-control bundle or exact cutoff-size positivity hypotheses.
theorem
HCPolySupport.coarseCaccioppoli_interior_qone_of_quantitativeCutoff_of_of_scalarControlFactors
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(k : ℝ → ℝ → ℕ)
{F G₀ : ℝ → ℝ}
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(g : ℝ → ℝ → Vec 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₀ ρ₂)
(hgMem : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → MeasureTheory.MemLp (g ρ₁ ρ₂) 2 (normalizedCubeMeasure Q))
(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)
(hscalarFactors : CoarseCaccioppoliBoundaryCanonicalScalarControlFactors Q a s C w g Acirc1 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 from primitive scalar-control factors, without exposing the raw scalar-control bundle or exact cutoff-size positivity hypotheses.
theorem
HCPolySupport.coarseCaccioppoli_boundary_qone_of_quantitativeCutoff_of_projectedPoincareBounds
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(k : ℝ → ℝ → ℕ)
{F : ℝ → ℝ}
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(g : ℝ → ℝ → Vec 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 ρ₂)
(hgMem : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → MeasureTheory.MemLp (g ρ₁ ρ₂) 2 (normalizedCubeMeasure Q))
(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)
(hprojectedCirc : CoarseCaccioppoliBoundaryCanonicalProjectedPoincareCircBounds Q a s C w g Acirc1 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 from the split Phase 2 scalar
inputs: nondegenerate positive factors plus the genuine projected-Poincare
and circ bounds.
theorem
HCPolySupport.coarseCaccioppoli_interior_qone_of_quantitativeCutoff_of_projectedPoincareBounds
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(k : ℝ → ℝ → ℕ)
{F G₀ : ℝ → ℝ}
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(g : ℝ → ℝ → Vec 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₀ ρ₂)
(hgMem : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → MeasureTheory.MemLp (g ρ₁ ρ₂) 2 (normalizedCubeMeasure Q))
(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)
(hprojectedCirc : CoarseCaccioppoliBoundaryCanonicalProjectedPoincareCircBounds Q a s C w g Acirc1 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 from the split Phase 2 scalar
inputs: nondegenerate positive factors plus the genuine projected-Poincare
and circ bounds.