Coarse-graining support: #
Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.QuantitativeCutoffInputs.Standard
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalAnalyticInputs.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 → ℝ)
(η : (ρ₁ ρ₂ : ℝ) → 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 → 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 (η ρ₁ ρ₂).toFun) (coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ ρ₂))
(hBgCent :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
0 ≤ coarseCaccioppoliCenteredCutoffSize Q s (scalarCutoffGradientField (η ρ₁ ρ₂).toFun) (Acirc1 ρ₁ ρ₂)
(AcircS ρ₁ ρ₂) (√(cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x))
(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 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 ρ₁ ρ₂)
:
CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalAnalyticInputs 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
Specialized analytic-input builder for the actual coarse Caccioppoli
harmonic family. This removes the external htest hypothesis once the caller
supplies the weighted-energy lower bound and the cutoff topological-support
condition needed by the weak-testing bridge.
theorem
HCPolySupport.CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalAnalyticInputs.of_cutoff_scalarControls
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(s C : ℝ)
{lam Lam : ℝ}
(k h : ℝ → ℝ → ℝ)
(F : ℝ → ℝ)
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(g : ℝ → ℝ → 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 → 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 (η ρ₁ ρ₂).toFun)
(fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) (Acirc1 ρ₁ ρ₂) (AcircS ρ₁ ρ₂)
(coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ ρ₂) C)
(hC : 0 ≤ 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 ρ₁ ρ₂)
:
CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalAnalyticInputs 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
theorem
HCPolySupport.CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalAnalyticInputs.of_harmonicFamily
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(s C : ℝ)
{lam Lam : ℝ}
(k h : ℝ → ℝ → ℝ)
(F : ℝ → ℝ)
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(g : ℝ → ℝ → 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)
(houter : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → ρ₂ < 1)
(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 (η ρ₁ ρ₂).toFun) (coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ ρ₂))
(hBgCent :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
0 ≤ coarseCaccioppoliCenteredCutoffSize Q s (scalarCutoffGradientField (η ρ₁ ρ₂).toFun) (Acirc1 ρ₁ ρ₂)
(AcircS ρ₁ ρ₂) (√(cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x))
(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 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 ρ₁ ρ₂)
:
CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalAnalyticInputs 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
theorem
HCPolySupport.CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalAnalyticInputs.of_cutoff_outerRadius
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(s C : ℝ)
{lam Lam : ℝ}
(k h : ℝ → ℝ → ℝ)
(F : ℝ → ℝ)
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(g : ℝ → ℝ → 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)
(houter : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → ρ₂ < 1)
(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 (η ρ₁ ρ₂).toFun)
(fun (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) (Acirc1 ρ₁ ρ₂) (AcircS ρ₁ ρ₂)
(coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ ρ₂) C)
(hC : 0 ≤ 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 ρ₁ ρ₂)
:
CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalAnalyticInputs 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
Quantitative-cutoff harmonic analytic inputs with the scalar cutoff package
bundled as CoarseCaccioppoliScalarCutoffControls.
theorem
HCPolySupport.CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalAnalyticInputs.of_harmonicCutoff
{d : ℕ}
(Q : TriadicCube d)
(a : CoeffField d)
(s C : ℝ)
{lam Lam : ℝ}
(k h : ℝ → ℝ → ℝ)
(F : ℝ → ℝ)
(w : ℝ → ℝ → AHarmonicFunction a (openCubeSet Q))
(g : ℝ → ℝ → Vec d → ℝ)
(Acirc1 AcircS U A1 AS : ℝ → ℝ → ℝ)
(hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a)
(hlower :
∀ ⦃ρ₁ ρ₂ : ℝ⦄,
1 / 3 ≤ ρ₁ →
ρ₁ < ρ₂ →
ρ₂ ≤ 1 →
F ρ₁ ≤ cubeAverage Q fun (x : Vec d) =>
QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂ x * scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x)
(houter : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → ρ₂ < 1)
(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)
(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 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 ρ₁ ρ₂)
:
CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalAnalyticInputs 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 (QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂))
(fun (ρ₁ ρ₂ : ℝ) (x : Vec d) => scalarVariationEnergyIntegrand a (w ρ₁ ρ₂) x) Acirc1 AcircS
(coarseCaccioppoliQuantitativeCutoffHessianBound Q) U (coarseCaccioppoliQuantitativeCutoffGradientBound Q)
(coarseCaccioppoliQuantitativeCutoffHessianBound Q) A1 AS
Canonical analytic-input builder for the actual harmonic family using the
chapter-3 canonical quantitative cube cutoff. The cutoff data are discharged
from the canonical smooth formula plus the strict outer-radius condition
ρ₂ < 1.