Coarse-graining support: Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.FinalWrappers #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.coarseCaccioppoli_boundary_qone_of_radiusEnergyBridgeFactorInputs
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(k : ℝ → ℝ → ℕ)
{F : ℝ → ℝ}
(flux : ℝ → ℝ → Vec d → Vec d)
(u g : ℝ → ℝ → Vec d → ℝ)
(ξ : ℝ → ℝ → Vec d → Vec d)
(energy : ℝ → ℝ → Vec d → ℝ)
(Acirc1 AcircS B A G X Y : ℝ → ℝ → ℝ)
(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 ρ₁ ρ₂) ρ₁ ρ₂)
(hinputs :
CoarseCaccioppoliBoundaryRadiusEnergyBridgeFactorInputs Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂))
(coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) F flux u g ξ energy Acirc1 AcircS B A G
X Y)
(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 coarse Caccioppoli from the separated radius-indexed factor inputs, localized explicit height, and standard multiscale ellipticity data.
theorem
HCPolySupport.coarseCaccioppoli_boundary_qone_of_radiusEnergyBridgeSeparatedFactorInputs
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(k : ℝ → ℝ → ℕ)
{F : ℝ → ℝ}
(flux : ℝ → ℝ → Vec d → Vec d)
(u g : ℝ → ℝ → Vec d → ℝ)
(ξ : ℝ → ℝ → Vec d → Vec d)
(energy : ℝ → ℝ → Vec d → ℝ)
(Acirc1 AcircS B AavgConst AavgCent Aflux1 AfluxS U Xi D 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 ρ₁ ρ₂) ρ₁ ρ₂)
(hinputs :
CoarseCaccioppoliBoundaryRadiusEnergyBridgeSeparatedFactorInputs Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂))
(coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) F flux u g ξ energy Acirc1 AcircS B
AavgConst AavgCent Aflux1 AfluxS 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))
:
Boundary coarse Caccioppoli from primitive separated radius-indexed factor inputs, localized explicit height, and standard multiscale ellipticity data.
theorem
HCPolySupport.coarseCaccioppoli_boundary_qone_of_radiusEnergyBridgeCanonicalFactorInputs
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(k : ℝ → ℝ → ℕ)
{F : ℝ → ℝ}
(flux : ℝ → ℝ → Vec d → Vec d)
(u g : ℝ → ℝ → Vec d → ℝ)
(ξ : ℝ → ℝ → Vec d → Vec d)
(energy : ℝ → ℝ → Vec d → ℝ)
(Acirc1 AcircS B U Xi D 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 ρ₁ ρ₂) ρ₁ ρ₂)
(hinputs :
CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalFactorInputs Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂))
(coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) F flux u g ξ energy Acirc1 AcircS B 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))
:
Boundary coarse Caccioppoli from canonical LambdaSq factor inputs,
localized explicit height, and standard multiscale ellipticity data.
theorem
HCPolySupport.coarseCaccioppoli_interior_qone_of_radiusEnergyBridgeFactorInputs
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(k : ℝ → ℝ → ℕ)
{F G₀ : ℝ → ℝ}
(flux : ℝ → ℝ → Vec d → Vec d)
(u g : ℝ → ℝ → Vec d → ℝ)
(ξ : ℝ → ℝ → Vec d → Vec d)
(energy : ℝ → ℝ → Vec d → ℝ)
(Acirc1 AcircS B A G X Y : ℝ → ℝ → ℝ)
(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 ρ₁ ρ₂) ρ₁ ρ₂)
(hinputs :
CoarseCaccioppoliBoundaryRadiusEnergyBridgeFactorInputs Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂))
(coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) G₀ flux u g ξ energy Acirc1 AcircS B A G
X Y)
(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 coarse Caccioppoli from the separated radius-indexed factor inputs, localized explicit height, radius agreement, and standard multiscale ellipticity data.
theorem
HCPolySupport.coarseCaccioppoli_interior_qone_of_radiusEnergyBridgeSeparatedFactorInputs
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(k : ℝ → ℝ → ℕ)
{F G₀ : ℝ → ℝ}
(flux : ℝ → ℝ → Vec d → Vec d)
(u g : ℝ → ℝ → Vec d → ℝ)
(ξ : ℝ → ℝ → Vec d → Vec d)
(energy : ℝ → ℝ → Vec d → ℝ)
(Acirc1 AcircS B AavgConst AavgCent Aflux1 AfluxS U Xi D 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 ρ₁ ρ₂) ρ₁ ρ₂)
(hinputs :
CoarseCaccioppoliBoundaryRadiusEnergyBridgeSeparatedFactorInputs Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂))
(coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) G₀ flux u g ξ energy Acirc1 AcircS B
AavgConst AavgCent Aflux1 AfluxS 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))
:
Interior coarse Caccioppoli from primitive separated radius-indexed factor inputs, localized explicit height, radius agreement, and standard multiscale ellipticity data.
theorem
HCPolySupport.coarseCaccioppoli_interior_qone_of_radiusEnergyBridgeCanonicalFactorInputs
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(k : ℝ → ℝ → ℕ)
{F G₀ : ℝ → ℝ}
(flux : ℝ → ℝ → Vec d → Vec d)
(u g : ℝ → ℝ → Vec d → ℝ)
(ξ : ℝ → ℝ → Vec d → Vec d)
(energy : ℝ → ℝ → Vec d → ℝ)
(Acirc1 AcircS B U Xi D 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 ρ₁ ρ₂) ρ₁ ρ₂)
(hinputs :
CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalFactorInputs Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂))
(coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) G₀ flux u g ξ energy Acirc1 AcircS B 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))
:
Interior coarse Caccioppoli from canonical LambdaSq factor inputs,
localized explicit height, radius agreement, and standard multiscale
ellipticity data.
theorem
HCPolySupport.coarseCaccioppoli_boundary_qone_of_radiusEnergyAnalyticInputs
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(k : ℝ → ℝ → ℕ)
{F : ℝ → ℝ}
(flux : ℝ → ℝ → Vec d → Vec d)
(u g : ℝ → ℝ → Vec d → ℝ)
(ξ : ℝ → ℝ → Vec d → Vec d)
(energy : ℝ → ℝ → Vec d → ℝ)
(Acirc1 AcircS B U Xi D 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 ρ₁ ρ₂) ρ₁ ρ₂)
(hanalytic :
CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalAnalyticInputs Q a s C (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂))
(coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) F flux u g ξ energy Acirc1 AcircS B U Xi
D A1 AS)
(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))
:
Boundary coarse Caccioppoli from the split canonical interface: local analytic/cutoff inputs plus the two remaining canonical coefficient bounds. This is the narrowest current final theorem surface before constructing the actual Chapter 3 cutoff family.
theorem
HCPolySupport.coarseCaccioppoli_interior_qone_of_radiusEnergyAnalyticInputs
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(k : ℝ → ℝ → ℕ)
{F G₀ : ℝ → ℝ}
(flux : ℝ → ℝ → Vec d → Vec d)
(u g : ℝ → ℝ → Vec d → ℝ)
(ξ : ℝ → ℝ → Vec d → Vec d)
(energy : ℝ → ℝ → Vec d → ℝ)
(Acirc1 AcircS B U Xi D 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 ρ₁ ρ₂) ρ₁ ρ₂)
(hanalytic :
CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalAnalyticInputs Q a s C (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂))
(coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) G₀ flux u g ξ energy Acirc1 AcircS B U
Xi D A1 AS)
(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))
:
Interior coarse Caccioppoli from the split canonical interface, transported across the radius agreement used for the centered interior quantity.
theorem
HCPolySupport.coarseCaccioppoli_boundary_qone_of_quantitativeCutoff_of_coefficientBounds
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(k : ℝ → ℝ → ℕ)
{F : ℝ → ℝ}
(flux : ℝ → ℝ → Vec d → Vec d)
(u g energy : ℝ → ℝ → Vec d → ℝ)
(η : (ρ₁ ρ₂ : ℝ) → QuantitativeCubeCutoff Q ρ₁ ρ₂)
(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 ρ₁ ρ₂) ρ₁ ρ₂)
(htest :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
F ρ₁ ≤ |cubeAverage Q fun (x : Vec d) =>
vecDot (flux ρ₁ ρ₂ x) (u ρ₁ ρ₂ x • scalarCutoffGradientField (η ρ₁ ρ₂).toFun x)|)
(henergyAvg : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → cubeAverage Q (energy ρ₁ ρ₂) = F ρ₂)
(hfluxMem : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → MeasureTheory.MemLp (flux ρ₁ ρ₂) 2 (normalizedCubeMeasure Q))
(huMem : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → MeasureTheory.MemLp (u ρ₁ ρ₂) 2 (normalizedCubeMeasure Q))
(hgMem : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → MeasureTheory.MemLp (g ρ₁ ρ₂) 2 (normalizedCubeMeasure Q))
(hfluxEnergy :
∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliFluxEnergyControls Q a s (flux ρ₁ ρ₂) (energy ρ₁ ρ₂))
(hBgConst :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
0 ≤ coarseCaccioppoliConstantCutoffSize Q (u ρ₁ ρ₂) (scalarCutoffGradientField (η ρ₁ ρ₂).toFun)
(coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ ρ₂))
(hBgCent :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
0 ≤ coarseCaccioppoliCenteredCutoffSize Q s (scalarCutoffGradientField (η ρ₁ ρ₂).toFun) (Acirc1 ρ₁ ρ₂)
(AcircS ρ₁ ρ₂) (√(cubeAverage Q (energy ρ₁ ρ₂))) (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 (u ρ₁ ρ₂)) (g ρ₁ ρ₂) N)
(hgCirc1 :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
∀ (N : ℕ), cubeBesovCircPartialNorm Q 1 2 1 N (g ρ₁ ρ₂) ≤ Acirc1 ρ₁ ρ₂ * √(cubeAverage Q (energy ρ₁ ρ₂)))
(hgCircS :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
∀ (N : ℕ),
cubeBesovCircPartialNorm Q (1 - s) 2 1 N (g ρ₁ ρ₂) ≤ AcircS ρ₁ ρ₂ * √(cubeAverage Q (energy ρ₁ ρ₂)))
(hU : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → cubeLpNorm Q 2 (u ρ₁ ρ₂) ≤ 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 coarse Caccioppoli from a quantitative cutoff family, the split
canonical coefficient bounds, localized explicit height, and the standard
multiscale ellipticity data. This packages the cutoff-generated vector field
ξ = ∇η and its canonical L^∞/derivative bounds automatically.
theorem
HCPolySupport.coarseCaccioppoli_interior_qone_of_quantitativeCutoff_of_coefficientBounds
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(s t C uL2Sq : ℝ)
{lam Lam : ℝ}
(k : ℝ → ℝ → ℕ)
{F G₀ : ℝ → ℝ}
(flux : ℝ → ℝ → Vec d → Vec d)
(u g energy : ℝ → ℝ → Vec d → ℝ)
(η : (ρ₁ ρ₂ : ℝ) → QuantitativeCubeCutoff Q ρ₁ ρ₂)
(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 ρ₁ ρ₂) ρ₁ ρ₂)
(htest :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
G₀ ρ₁ ≤ |cubeAverage Q fun (x : Vec d) =>
vecDot (flux ρ₁ ρ₂ x) (u ρ₁ ρ₂ x • scalarCutoffGradientField (η ρ₁ ρ₂).toFun x)|)
(henergyAvg : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → cubeAverage Q (energy ρ₁ ρ₂) = G₀ ρ₂)
(hfluxMem : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → MeasureTheory.MemLp (flux ρ₁ ρ₂) 2 (normalizedCubeMeasure Q))
(huMem : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → MeasureTheory.MemLp (u ρ₁ ρ₂) 2 (normalizedCubeMeasure Q))
(hgMem : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → MeasureTheory.MemLp (g ρ₁ ρ₂) 2 (normalizedCubeMeasure Q))
(hfluxEnergy :
∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliFluxEnergyControls Q a s (flux ρ₁ ρ₂) (energy ρ₁ ρ₂))
(hBgConst :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
0 ≤ coarseCaccioppoliConstantCutoffSize Q (u ρ₁ ρ₂) (scalarCutoffGradientField (η ρ₁ ρ₂).toFun)
(coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ ρ₂))
(hBgCent :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
0 ≤ coarseCaccioppoliCenteredCutoffSize Q s (scalarCutoffGradientField (η ρ₁ ρ₂).toFun) (Acirc1 ρ₁ ρ₂)
(AcircS ρ₁ ρ₂) (√(cubeAverage Q (energy ρ₁ ρ₂))) (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 (u ρ₁ ρ₂)) (g ρ₁ ρ₂) N)
(hgCirc1 :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
∀ (N : ℕ), cubeBesovCircPartialNorm Q 1 2 1 N (g ρ₁ ρ₂) ≤ Acirc1 ρ₁ ρ₂ * √(cubeAverage Q (energy ρ₁ ρ₂)))
(hgCircS :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
∀ (N : ℕ),
cubeBesovCircPartialNorm Q (1 - s) 2 1 N (g ρ₁ ρ₂) ≤ AcircS ρ₁ ρ₂ * √(cubeAverage Q (energy ρ₁ ρ₂)))
(hU : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → cubeLpNorm Q 2 (u ρ₁ ρ₂) ≤ 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 coarse Caccioppoli from a quantitative cutoff family, the split canonical coefficient bounds, localized explicit height, radius agreement, and the standard multiscale ellipticity data.