Coarse-graining support: #
Support.Deterministic.CoarseCaccioppoli.EnergyBridge.QuantitativeCutoff.NormalizedAndGradient
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.normalized_quantitativeCubeCutoff_canonicalFun_descendant_average_oscillation_controls
{d : ℕ}
(Q : TriadicCube d)
(j : ℕ)
:
have η := QuantitativeCubeCutoff.canonicalFun Q (1 / 2) (3 / 4);
have φ := fun (x : Vec d) => (cubeAverage Q η)⁻¹ * η x;
have B := (cubeAverage Q η)⁻¹;
have D := B * (quantitativeCubeCutoffGradientConst d / ((3 / 4 - 1 / 2) * cubeRadius Q));
(∀ R ∈ descendantsAtDepth Q j, |1 - cubeAverage R φ| ≤ 1 + B) ∧ ∀ R ∈ descendantsAtDepth Q j,
∀ᵐ (x : Vec d) ∂volumeMeasureOn (cubeSet R), |cubeAverage R φ - φ x| ≤ cubeScaleFactor R * D
theorem
HCPolySupport.cubeBesovDualTestNorm_normalized_quantitativeCubeCutoff_canonicalFun_le
{d : ℕ}
(Q : TriadicCube d)
{r : ℝ}
(hr_le_one : r ≤ 1)
(N : ℕ)
:
have η := QuantitativeCubeCutoff.canonicalFun Q (1 / 2) (3 / 4);
have φ := fun (x : Vec d) => (cubeAverage Q η)⁻¹ * η x;
have B := (cubeAverage Q η)⁻¹;
have D := B * (quantitativeCubeCutoffGradientConst d / ((3 / 4 - 1 / 2) * cubeRadius Q));
cubeBesovDualTestNorm Q r 2 1 N φ ≤ cubeBesovScaleWeight r Q * (cubeScaleFactor Q * D + B)
theorem
HCPolySupport.cubeBesovDualLocalMemLpGlobal_normalized_quantitativeCubeCutoff_canonicalFun
{d : ℕ}
(Q : TriadicCube d)
:
have η := QuantitativeCubeCutoff.canonicalFun Q (1 / 2) (3 / 4);
have φ := fun (x : Vec d) => (cubeAverage Q η)⁻¹ * η x;
CubeBesovDualLocalMemLpGlobal Q 2 φ
theorem
HCPolySupport.quantitativeCubeCutoff_memLp_top_gradientField
{d : ℕ}
(Q : TriadicCube d)
{ρ₁ ρ₂ : ℝ}
(η : QuantitativeCubeCutoff Q ρ₁ ρ₂)
:
theorem
HCPolySupport.quantitativeCubeCutoff_cubeLpNorm_infty_gradientField_le
{d : ℕ}
(Q : TriadicCube d)
{ρ₁ ρ₂ : ℝ}
(η : QuantitativeCubeCutoff Q ρ₁ ρ₂)
:
cubeLpNorm Q ⊤ (scalarCutoffGradientField η.toFun) ≤ quantitativeCubeCutoffGradientConst d / ((ρ₂ - ρ₁) * cubeRadius Q)
theorem
HCPolySupport.quantitativeCubeCutoff_component_fderiv_bound_on_cubeSet
{d : ℕ}
(Q : TriadicCube d)
{ρ₁ ρ₂ : ℝ}
(η : QuantitativeCubeCutoff Q ρ₁ ρ₂)
(i : Fin d)
(z : Vec d)
:
theorem
HCPolySupport.normalized_quantitativeCubeCutoff_canonicalFun_gradient_controls
{d : ℕ}
(Q : TriadicCube d)
:
have η := QuantitativeCubeCutoff.canonicalFun Q (1 / 2) (3 / 4);
have φ := fun (x : Vec d) => (cubeAverage Q η)⁻¹ * η x;
MeasureTheory.MemLp (scalarCutoffGradientField φ) ⊤ (normalizedCubeMeasure Q) ∧ (∀ (i : Fin d), ContDiff ℝ ↑⊤ fun (x : Vec d) => scalarCutoffGradientField φ x i) ∧ ∀ (i : Fin d),
∀ z ∈ cubeSet Q,
‖fderiv ℝ (fun (x : Vec d) => scalarCutoffGradientField φ x i) z‖ ≤ (cubeAverage Q η)⁻¹ * (quantitativeCubeCutoffHessianConst d / ((3 / 4 - 1 / 2) * cubeRadius Q) ^ 2)
theorem
HCPolySupport.cubeLpNorm_infty_scalarCutoffGradientField_normalized_quantitativeCubeCutoff_canonicalFun_le
{d : ℕ}
(Q : TriadicCube d)
:
have η := QuantitativeCubeCutoff.canonicalFun Q (1 / 2) (3 / 4);
have φ := fun (x : Vec d) => (cubeAverage Q η)⁻¹ * η x;
cubeLpNorm Q ⊤ (scalarCutoffGradientField φ) ≤ (cubeAverage Q η)⁻¹ * (quantitativeCubeCutoffGradientConst d / ((3 / 4 - 1 / 2) * cubeRadius Q))
L∞ bound for the scalar-gradient field of the normalized quantitative
cutoff. This extracts the gradient-size part of
normalized_quantitativeCubeCutoff_canonicalFun_gradient_controls; it is used
to bound the Section 5.3 cutoff-product coefficient.
theorem
HCPolySupport.quantitativeCubeCutoff_memLp_top_gradientField_on_descendant
{d : ℕ}
{Q R : TriadicCube d}
{j : ℕ}
(_hR : R ∈ descendantsAtDepth Q j)
{ρ₁ ρ₂ : ℝ}
(η : QuantitativeCubeCutoff Q ρ₁ ρ₂)
:
The gradient field of a quantitative cutoff built on a parent cube is
L∞ on every descendant cube. This is the small-cube version needed by the
Chapter 3 Caccioppoli argument.
theorem
HCPolySupport.quantitativeCubeCutoff_cubeLpNorm_infty_gradientField_le_on_descendant
{d : ℕ}
{Q R : TriadicCube d}
{j : ℕ}
(_hR : R ∈ descendantsAtDepth Q j)
{ρ₁ ρ₂ : ℝ}
(η : QuantitativeCubeCutoff Q ρ₁ ρ₂)
:
cubeLpNorm R ⊤ (scalarCutoffGradientField η.toFun) ≤ quantitativeCubeCutoffGradientConst d / ((ρ₂ - ρ₁) * cubeRadius Q)
Descendant-local L∞ bound for the gradient field of a parent-cube
quantitative cutoff.
theorem
HCPolySupport.quantitativeCubeCutoff_component_fderiv_bound_on_descendant
{d : ℕ}
{Q R : TriadicCube d}
{j : ℕ}
(hR : R ∈ descendantsAtDepth Q j)
{ρ₁ ρ₂ : ℝ}
(η : QuantitativeCubeCutoff Q ρ₁ ρ₂)
(i : Fin d)
(z : Vec d)
:
Descendant-local derivative bound for the cutoff-gradient field. The bound is still expressed with the parent cube radius, while later small-cube bookkeeping multiplies it by the descendant scale.
theorem
HCPolySupport.CoarseCaccioppoliScalarCutoffControls.of_quantitativeCubeCutoff
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
{ρ₁ ρ₂ : ℝ}
(u g energy : Vec d → ℝ)
(η : QuantitativeCubeCutoff Q ρ₁ ρ₂)
{Acirc1 AcircS C : ℝ}
(hB : 0 ≤ quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2)
(hBgConst :
0 ≤ coarseCaccioppoliConstantCutoffSize Q u (scalarCutoffGradientField η.toFun)
(quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2))
(hBgCent :
0 ≤ coarseCaccioppoliCenteredCutoffSize Q s (scalarCutoffGradientField η.toFun) Acirc1 AcircS (√(cubeAverage Q energy))
(quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2) 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 η.toFun) energy Acirc1 AcircS
(quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2) C
theorem
HCPolySupport.CoarseCaccioppoliScalarCutoffControls.of_quantitativeCubeCutoff_on_descendant
{d : ℕ}
{Q R : TriadicCube d}
{j : ℕ}
(hR : R ∈ descendantsAtDepth Q j)
(s : ℝ)
{ρ₁ ρ₂ : ℝ}
(u g energy : Vec d → ℝ)
(η : QuantitativeCubeCutoff Q ρ₁ ρ₂)
{Acirc1 AcircS C : ℝ}
(hB : 0 ≤ quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2)
(hBgConst :
0 ≤ coarseCaccioppoliConstantCutoffSize R u (scalarCutoffGradientField η.toFun)
(quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2))
(hBgCent :
0 ≤ coarseCaccioppoliCenteredCutoffSize R s (scalarCutoffGradientField η.toFun) Acirc1 AcircS (√(cubeAverage R energy))
(quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2) C)
(hC : 0 ≤ C)
(hproj : ∀ (N : ℕ), CubeDescendantProjectedDualMeanZeroPoincareEstimate R C (cubeFluctuation R u) g N)
(hgCirc1 : ∀ (N : ℕ), cubeBesovCircPartialNorm R 1 2 1 N g ≤ Acirc1 * √(cubeAverage R energy))
(hgCircS : ∀ (N : ℕ), cubeBesovCircPartialNorm R (1 - s) 2 1 N g ≤ AcircS * √(cubeAverage R energy))
:
CoarseCaccioppoliScalarCutoffControls R s u g (scalarCutoffGradientField η.toFun) energy Acirc1 AcircS
(quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2) C
Scalar cutoff-control package on a descendant cube, using a quantitative cutoff constructed on the parent cube.
theorem
HCPolySupport.CoarseCaccioppoliVectorCutoffControls.of_quantitativeCubeCutoff
{d : ℕ}
(Q : TriadicCube d)
(s : ℝ)
{ρ₁ ρ₂ : ℝ}
(u : Vec d → ℝ)
(G : Vec d → Vec d)
(energy : Vec d → ℝ)
(η : QuantitativeCubeCutoff Q ρ₁ ρ₂)
{Acirc1 AcircS C : ℝ}
(hB : 0 ≤ quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2)
(hAcircS : 0 ≤ AcircS)
(hBgConst :
0 ≤ coarseCaccioppoliConstantCutoffSize Q u (scalarCutoffGradientField η.toFun)
(quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2))
(hBgCent :
0 ≤ coarseCaccioppoliCenteredCutoffSize Q s (scalarCutoffGradientField η.toFun) Acirc1 AcircS (√(cubeAverage Q energy))
(quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2) (↑(Fintype.card (Fin d)) * C))
(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 η.toFun) energy Acirc1 AcircS
(quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2) C
Vector projected-Poincare version of
CoarseCaccioppoliScalarCutoffControls.of_quantitativeCubeCutoff.
The vector Poincare constant is C; the centered exact cutoff size is stated
with the effective scalar-facing constant (Fintype.card (Fin d) : ℝ) * C.
theorem
HCPolySupport.CoarseCaccioppoliVectorCutoffControls.of_quantitativeCubeCutoff_on_descendant
{d : ℕ}
{Q R : TriadicCube d}
{j : ℕ}
(hR : R ∈ descendantsAtDepth Q j)
(s : ℝ)
{ρ₁ ρ₂ : ℝ}
(u : Vec d → ℝ)
(G : Vec d → Vec d)
(energy : Vec d → ℝ)
(η : QuantitativeCubeCutoff Q ρ₁ ρ₂)
{Acirc1 AcircS C : ℝ}
(hB : 0 ≤ quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2)
(hAcircS : 0 ≤ AcircS)
(hBgConst :
0 ≤ coarseCaccioppoliConstantCutoffSize R u (scalarCutoffGradientField η.toFun)
(quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2))
(hBgCent :
0 ≤ coarseCaccioppoliCenteredCutoffSize R s (scalarCutoffGradientField η.toFun) Acirc1 AcircS (√(cubeAverage R energy))
(quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2) (↑(Fintype.card (Fin d)) * C))
(hC : 0 ≤ C)
(hproj : ∀ (N : ℕ), CubeDescendantProjectedDualMeanZeroVectorPoincareEstimate R C (cubeFluctuation R u) G N)
(hGcirc1 :
∀ (i : Fin d) (N : ℕ),
(cubeBesovCircPartialNorm R 1 2 1 N fun (x : Vec d) => G x i) ≤ Acirc1 * √(cubeAverage R energy))
(hGcircS :
∀ (i : Fin d) (N : ℕ),
(cubeBesovCircPartialNorm R (1 - s) 2 1 N fun (x : Vec d) => G x i) ≤ AcircS * √(cubeAverage R energy))
:
CoarseCaccioppoliVectorCutoffControls R s u G (scalarCutoffGradientField η.toFun) energy Acirc1 AcircS
(quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * cubeRadius Q) ^ 2) C
Vector projected-Poincare cutoff-control package on a descendant cube, using a quantitative cutoff constructed on the parent cube.