Coarse-graining support: #
Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.QuantitativeCutoffInputs.Setup.Canonical
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Quantitative cutoff inputs: canonical cutoff packages #
theorem
HCPolySupport.coarseCaccioppoliQuantitativeCutoffHessianBound_nonneg
{d : ℕ}
(Q : TriadicCube d)
{ρ₁ ρ₂ : ℝ}
(η : QuantitativeCubeCutoff Q ρ₁ ρ₂)
:
theorem
HCPolySupport.coarseCaccioppoliQuantitativeCutoffHessianBound_pos
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
{ρ₁ ρ₂ : ℝ}
(hlt : ρ₁ < ρ₂)
:
noncomputable def
HCPolySupport.coarseCaccioppoliCanonicalQuantitativeCutoff
{d : ℕ}
(Q : TriadicCube d)
{ρ₁ ρ₂ : ℝ}
(hρ₁ : 1 / 3 ≤ ρ₁)
(hlt : ρ₁ < ρ₂)
:
QuantitativeCubeCutoff Q ρ₁ ρ₂
Canonical quantitative cube cutoff at an admissible radius pair
(ρ₁, ρ₂) with ρ₁ ≥ 1/3 and ρ₁ < ρ₂.
Equations
Instances For
theorem
HCPolySupport.coarseCaccioppoliCanonicalQuantitativeCutoff_tsupport_subset_openCubeSet_of_lt_one
{d : ℕ}
(Q : TriadicCube d)
{ρ₁ ρ₂ : ℝ}
(hρ₁ : 1 / 3 ≤ ρ₁)
(hlt : ρ₁ < ρ₂)
(hρ₂_lt_one : ρ₂ < 1)
:
tsupport (coarseCaccioppoliCanonicalQuantitativeCutoff Q hρ₁ hlt).toFun ⊆ openCubeSet Q
theorem
HCPolySupport.coarseCaccioppoliCanonicalQuantitativeCutoff_tsupport_subset_openCubeSet_on_radiusSequence
{d : ℕ}
(Q : TriadicCube d)
(n : ℕ)
:
theorem
HCPolySupport.CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalAnalyticInputs.of_quantitativeCubeCutoff
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(s C : ℝ)
(k h : ℝ → ℝ → ℝ)
(F : ℝ → ℝ)
(flux : ℝ → ℝ → Vec d → Vec d)
(u g energy : ℝ → ℝ → Vec d → ℝ)
(η : (ρ₁ ρ₂ : ℝ) → QuantitativeCubeCutoff Q ρ₁ ρ₂)
(Acirc1 AcircS U A1 AS : ℝ → ℝ → ℝ)
(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)
(hC : 0 ≤ 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 ρ₁ ρ₂)
:
CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalAnalyticInputs Q a s C k h F flux u g
(fun (ρ₁ ρ₂ : ℝ) => scalarCutoffGradientField (η ρ₁ ρ₂).toFun) energy Acirc1 AcircS
(coarseCaccioppoliQuantitativeCutoffHessianBound Q) U (coarseCaccioppoliQuantitativeCutoffGradientBound Q)
(coarseCaccioppoliQuantitativeCutoffHessianBound Q) A1 AS
A quantitative cube cutoff upgrades the external testing/flux/Poincare
hypotheses to the split canonical local analytic inputs used by the final
coarse Caccioppoli wrappers. The cutoff contributes the vector field
ξ = ∇η, its L^∞ control, and the component derivative bound.
theorem
HCPolySupport.CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalVectorAnalyticInputs.of_quantitativeCubeCutoff
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(s C : ℝ)
(k h : ℝ → ℝ → ℝ)
(F : ℝ → ℝ)
(flux : ℝ → ℝ → Vec d → Vec d)
(u : ℝ → ℝ → Vec d → ℝ)
(G : ℝ → ℝ → Vec d → Vec d)
(energy : ℝ → ℝ → Vec d → ℝ)
(η : (ρ₁ ρ₂ : ℝ) → QuantitativeCubeCutoff Q ρ₁ ρ₂)
(Acirc1 AcircS U A1 AS : ℝ → ℝ → ℝ)
(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 → ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G ρ₁ ρ₂ x i) 2 (normalizedCubeMeasure Q))
(hfluxEnergy :
∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliFluxEnergyControls Q a s (flux ρ₁ ρ₂) (energy ρ₁ ρ₂))
(hvector :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
CoarseCaccioppoliVectorCutoffControls Q s (u ρ₁ ρ₂) (G ρ₁ ρ₂) (scalarCutoffGradientField (η ρ₁ ρ₂).toFun)
(energy ρ₁ ρ₂) (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 (u ρ₁ ρ₂) ≤ U ρ₁ ρ₂)
(hA1 : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → Acirc1 ρ₁ ρ₂ ≤ A1 ρ₁ ρ₂)
(hAS : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → AcircS ρ₁ ρ₂ ≤ AS ρ₁ ρ₂)
:
CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalVectorAnalyticInputs Q a s C k h F flux u G
(fun (ρ₁ ρ₂ : ℝ) => scalarCutoffGradientField (η ρ₁ ρ₂).toFun) energy Acirc1 AcircS
(coarseCaccioppoliQuantitativeCutoffHessianBound Q) U (coarseCaccioppoliQuantitativeCutoffGradientBound Q)
(coarseCaccioppoliQuantitativeCutoffHessianBound Q) A1 AS
Vector-Poincare version of
CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalAnalyticInputs.of_quantitativeCubeCutoff.
The cutoff again supplies ξ = ∇η; the analytic package keeps the vector
cutoff controls rather than scalarizing to one gradient component.
theorem
HCPolySupport.CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalVectorAnalyticInputs.of_quantitativeCubeCutoff_of_aHarmonicFamily
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(s C : ℝ)
{lam Lam : ℝ}
(k h : ℝ → ℝ → ℝ)
(F : ℝ → ℝ)
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(G : ℝ → ℝ → Vec d → Vec d)
(η : (ρ₁ ρ₂ : ℝ) → QuantitativeCubeCutoff Q ρ₁ ρ₂)
(Acirc1 AcircS U A1 AS : ℝ → ℝ → ℝ)
(hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a)
(hlower :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
F ρ₁ ≤ cubeAverage Q fun (x : Vec d) => (η ρ₁ ρ₂).toFun x * scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(hη_tsupport : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → tsupport (η ρ₁ ρ₂).toFun ⊆ openCubeSet Q)
(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 → ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G ρ₁ ρ₂ x i) 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)
(hvector :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
CoarseCaccioppoliVectorCutoffControls Q s (fun (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) (G ρ₁ ρ₂)
(scalarCutoffGradientField (η ρ₁ ρ₂).toFun)
(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 ρ₁ ρ₂)
:
CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalVectorAnalyticInputs Q a s C k h F
(fun (ρ₁ ρ₂ : ℝ) (x : Vec d) => matVecMul (a x) ((w ρ₁ ρ₂).toH1.grad x))
(fun (ρ₁ ρ₂ : ℝ) (x : Vec d) => (w ρ₁ ρ₂).toH1.toFun x) G
(fun (ρ₁ ρ₂ : ℝ) => scalarCutoffGradientField (η ρ₁ ρ₂).toFun)
(fun (ρ₁ ρ₂ : ℝ) (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) Acirc1 AcircS
(coarseCaccioppoliQuantitativeCutoffHessianBound Q) U (coarseCaccioppoliQuantitativeCutoffGradientBound Q)
(coarseCaccioppoliQuantitativeCutoffHessianBound Q) A1 AS
Harmonic-family builder for the vector canonical analytic inputs. The weak-testing bridge supplies the testing inequality from the weighted energy lower bound, while the caller supplies the vector cutoff controls.