Coarse-graining support: #
Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.HarmonicCoefficientBounds
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Harmonic canonical cutoff coefficient localization #
This file removes the direct raw-coefficient hypothesis from the strongest canonical harmonic wrappers by rebuilding it from the note-shaped ingredients: single-cube coefficient bounds plus the localized multiscale ellipticity comparison.
theorem
HCPolySupport.CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalRawCoefficientBounds.of_coefficientBounds_of_multiscaleEllipticity_of_localizedExplicitHeightOfScaleChoice
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(k : ℝ → ℝ → ℕ)
(U Xi D A1 AS : ℝ → ℝ → ℝ)
(hC : 0 ≤ C)
(hs : 0 < s)
(ht : 0 < t)
(hst : s + t < 1)
(hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂)
(hcoeff :
CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalCoefficientBounds Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂))
(coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) U Xi D 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))
(hBsum_s :
Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
(hSigmaSum_t :
Summable fun (n : ℕ) =>
geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
:
CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalRawCoefficientBounds Q a s t C uL2Sq
(coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) U Xi D A1 AS
Canonical raw coefficient bounds from the note's single-cube coefficient bounds and localized explicit-height coefficient localization.
theorem
HCPolySupport.coarseCaccioppoli_boundary_qone_of_quantitativeCutoff_of_of_scalarCutoffControls
{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 ρ₂)
(hfluxMem :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
MeasureTheory.MemLp (fun (x : Vec d) => matVecMul (a x) ((w ρ₁ ρ₂).toH1.grad x)) 2 (normalizedCubeMeasure Q))
(huMem :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ → ρ₂ ≤ 1 → MeasureTheory.MemLp (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) 2 (normalizedCubeMeasure Q))
(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)
(hscalar :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 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)
(hAcirc1_nonneg : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → 0 ≤ Acirc1 ρ₁ ρ₂)
(hAcircS_nonneg : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → 0 ≤ 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))
(hBsum_s :
Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
(hSigmaSum_t :
Summable fun (n : ℕ) =>
geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
:
Boundary canonical harmonic Caccioppoli with the raw coefficient hypothesis rebuilt from localized multiscale coefficient data.
theorem
HCPolySupport.coarseCaccioppoli_interior_qone_of_quantitativeCutoff_of_of_scalarCutoffControls
{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₀ ρ₂)
(hfluxMem :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
MeasureTheory.MemLp (fun (x : Vec d) => matVecMul (a x) ((w ρ₁ ρ₂).toH1.grad x)) 2 (normalizedCubeMeasure Q))
(huMem :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ → ρ₂ ≤ 1 → MeasureTheory.MemLp (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) 2 (normalizedCubeMeasure Q))
(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)
(hscalar :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 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)
(hAcirc1_nonneg : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → 0 ≤ Acirc1 ρ₁ ρ₂)
(hAcircS_nonneg : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → 0 ≤ 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))
(hBsum_s :
Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
(hSigmaSum_t :
Summable fun (n : ℕ) =>
geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
:
Interior canonical harmonic Caccioppoli with the raw coefficient hypothesis rebuilt from localized multiscale coefficient data.
theorem
HCPolySupport.CoarseCaccioppoliScalarCutoffControls.of_canonicalQuantitativeCutoff
{d : ℕ}
(Q : TriadicCube d)
(s C : ℝ)
{ρ₁ ρ₂ : ℝ}
(hρ₁ : 1 / 3 ≤ ρ₁)
(hlt : ρ₁ < ρ₂)
(u g energy : Vec d → ℝ)
(Acirc1 AcircS : ℝ)
(hBgConst :
0 ≤ coarseCaccioppoliConstantCutoffSize Q u (scalarCutoffGradientField (QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂))
(coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ ρ₂))
(hBgCent :
0 ≤ coarseCaccioppoliCenteredCutoffSize Q s (scalarCutoffGradientField (QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂))
Acirc1 AcircS (√(cubeAverage Q energy)) (coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ ρ₂) C)
(hC : 0 ≤ C)
(hproj : ∀ (N : ℕ), CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C (cubeFluctuation Q u) g N)
(hgCirc1 : ∀ (N : ℕ), cubeBesovCircPartialNorm Q 1 2 1 N g ≤ Acirc1 * √(cubeAverage Q energy))
(hgCircS : ∀ (N : ℕ), cubeBesovCircPartialNorm Q (1 - s) 2 1 N g ≤ AcircS * √(cubeAverage Q energy))
:
CoarseCaccioppoliScalarCutoffControls Q s u g (scalarCutoffGradientField (QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂))
energy Acirc1 AcircS (coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ ρ₂) C
The canonical quantitative cutoff supplies the scalar cutoff-control
bundle once the projected Poincare and Besov circ bounds are available.
theorem
HCPolySupport.CoarseCaccioppoliScalarCutoffControls.of_canonicalQuantitativeCutoff_of_positiveFactors
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(s C : ℝ)
{ρ₁ ρ₂ : ℝ}
(hρ₁ : 1 / 3 ≤ ρ₁)
(hlt : ρ₁ < ρ₂)
(u g energy : Vec d → ℝ)
(Acirc1 AcircS : ℝ)
(hs0 : 0 < s)
(hs1 : s < 1)
(hu : 0 < cubeLpNorm Q 2 u)
(hAcirc1 : 0 < Acirc1)
(hAcircS : 0 ≤ AcircS)
(hE : 0 < √(cubeAverage Q energy))
(hC : 0 < C)
(hproj : ∀ (N : ℕ), CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C (cubeFluctuation Q u) g N)
(hgCirc1 : ∀ (N : ℕ), cubeBesovCircPartialNorm Q 1 2 1 N g ≤ Acirc1 * √(cubeAverage Q energy))
(hgCircS : ∀ (N : ℕ), cubeBesovCircPartialNorm Q (1 - s) 2 1 N g ≤ AcircS * √(cubeAverage Q energy))
:
CoarseCaccioppoliScalarCutoffControls Q s u g (scalarCutoffGradientField (QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂))
energy Acirc1 AcircS (coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ ρ₂) C
A positivity-factor version of the canonical scalar cutoff-control constructor. This replaces the raw strict-positivity hypotheses for the two exact cutoff sizes by simpler positive inputs.
theorem
HCPolySupport.CoarseCaccioppoliVectorCutoffControls.of_canonicalQuantitativeCutoff_of_positiveFactors
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(s C : ℝ)
{ρ₁ ρ₂ : ℝ}
(hρ₁ : 1 / 3 ≤ ρ₁)
(hlt : ρ₁ < ρ₂)
(u energy : Vec d → ℝ)
(G : Vec d → Vec d)
(Acirc1 AcircS : ℝ)
(hs0 : 0 < s)
(hs1 : s < 1)
(hu : 0 < cubeLpNorm Q 2 u)
(hAcirc1 : 0 < Acirc1)
(hAcircS : 0 ≤ AcircS)
(hE : 0 < √(cubeAverage Q energy))
(hC : 0 < C)
(hproj : ∀ (N : ℕ), CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate Q C (cubeFluctuation Q u) G N)
(hGcirc1 :
∀ (i : Fin d) (N : ℕ),
(cubeBesovCircPartialNorm Q 1 2 1 N fun (x : Vec d) => G x i) ≤ Acirc1 * √(cubeAverage Q energy))
(hGcircS :
∀ (i : Fin d) (N : ℕ),
(cubeBesovCircPartialNorm Q (1 - s) 2 1 N fun (x : Vec d) => G x i) ≤ AcircS * √(cubeAverage Q energy))
:
CoarseCaccioppoliVectorCutoffControls Q s u G (scalarCutoffGradientField (QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂))
energy Acirc1 AcircS (coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ ρ₂) C
Vector-Poincare analogue of
CoarseCaccioppoliScalarCutoffControls.of_canonicalQuantitativeCutoff_of_positiveFactors.
The strict positivity of the centered cutoff size uses the effective
scalar-facing constant (Fintype.card (Fin d) : ℝ) * C.
theorem
HCPolySupport.coarseCaccioppoli_boundary_qone_of_quantitativeCutoff_of_harmonicFamily
{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 ρ₂)
(hfluxMem :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
MeasureTheory.MemLp (fun (x : Vec d) => matVecMul (a x) ((w ρ₁ ρ₂).toH1.grad x)) 2 (normalizedCubeMeasure Q))
(huMem :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ → ρ₂ ≤ 1 → MeasureTheory.MemLp (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) 2 (normalizedCubeMeasure Q))
(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)
(hBgConst :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
0 ≤ coarseCaccioppoliConstantCutoffSize Q (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x)
(scalarCutoffGradientField (QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂))
(coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ ρ₂))
(hBgCent :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
0 ≤ coarseCaccioppoliCenteredCutoffSize Q s
(scalarCutoffGradientField (QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂)) (Acirc1 ρ₁ ρ₂) (AcircS ρ₁ ρ₂)
(√(cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x))
(coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ ρ₂) C)
(hAcirc1_nonneg : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → 0 ≤ Acirc1 ρ₁ ρ₂)
(hAcircS_nonneg : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → 0 ≤ AcircS ρ₁ ρ₂)
(hproj :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
∀ (N : ℕ),
CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C
(cubeFluctuation Q fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) (g ρ₁ ρ₂) N)
(hgCirc1 :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
∀ (N : ℕ),
cubeBesovCircPartialNorm Q 1 2 1 N (g ρ₁ ρ₂) ≤ Acirc1 ρ₁ ρ₂ * √(cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x))
(hgCircS :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
∀ (N : ℕ),
cubeBesovCircPartialNorm Q (1 - s) 2 1 N (g ρ₁ ρ₂) ≤ AcircS ρ₁ ρ₂ * √(cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x))
(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))
(hBsum_s :
Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
(hSigmaSum_t :
Summable fun (n : ℕ) =>
geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
:
Boundary canonical harmonic Caccioppoli with the scalar cutoff-control bundle rebuilt from the canonical cutoff-product/Poincare inputs.
theorem
HCPolySupport.coarseCaccioppoli_interior_qone_of_quantitativeCutoff_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))
(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₀ ρ₂)
(hfluxMem :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
MeasureTheory.MemLp (fun (x : Vec d) => matVecMul (a x) ((w ρ₁ ρ₂).toH1.grad x)) 2 (normalizedCubeMeasure Q))
(huMem :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ → ρ₂ ≤ 1 → MeasureTheory.MemLp (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) 2 (normalizedCubeMeasure Q))
(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)
(hBgConst :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
0 ≤ coarseCaccioppoliConstantCutoffSize Q (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x)
(scalarCutoffGradientField (QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂))
(coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ ρ₂))
(hBgCent :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
0 ≤ coarseCaccioppoliCenteredCutoffSize Q s
(scalarCutoffGradientField (QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂)) (Acirc1 ρ₁ ρ₂) (AcircS ρ₁ ρ₂)
(√(cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x))
(coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ ρ₂) C)
(hAcirc1_nonneg : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → 0 ≤ Acirc1 ρ₁ ρ₂)
(hAcircS_nonneg : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → 0 ≤ AcircS ρ₁ ρ₂)
(hproj :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
∀ (N : ℕ),
CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C
(cubeFluctuation Q fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) (g ρ₁ ρ₂) N)
(hgCirc1 :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
∀ (N : ℕ),
cubeBesovCircPartialNorm Q 1 2 1 N (g ρ₁ ρ₂) ≤ Acirc1 ρ₁ ρ₂ * √(cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x))
(hgCircS :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
∀ (N : ℕ),
cubeBesovCircPartialNorm Q (1 - s) 2 1 N (g ρ₁ ρ₂) ≤ AcircS ρ₁ ρ₂ * √(cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x))
(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))
(hBsum_s :
Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
(hSigmaSum_t :
Summable fun (n : ℕ) =>
geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
:
Interior canonical harmonic Caccioppoli with the scalar cutoff-control bundle rebuilt from the canonical cutoff-product/Poincare inputs.