Coarse-graining support: Support.Deterministic.CoarsePoincareRHS.LocalNoteTerms.Bounded #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.sq_negativePartialSeminormTwo_succ_le_childMean_add_energy_add_YoungError_two
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ρ : ZeroTraceDirichletCorrectorData Q a g)
{u : Vec d → Vec d}
(w : AHarmonicFunction a (cubeSet Q))
{lam Lam : ℝ}
(s : ℝ)
{η : ℝ}
(hs : 0 < s)
(hη : 0 < η)
(N : ℕ)
(hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a)
(hu : MemVectorL2 (cubeSet Q) u)
(hgrad :
CubeAverageGradientEnergyControl Q a (fun (x : Vec d) => w.toH1.grad x)
(coefficientEnergyDensity a fun (x : Vec d) => w.toH1.grad x))
(hsum : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a)
(huw : ∀ x ∈ cubeSet Q, u x = w.toH1.grad x + ρ.toH10.grad x)
(hmem : MemVectorL2 (cubeSet Q) g)
(hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q))
(hgradρ : MeasureTheory.MemLp (fun (x : Vec d) => ρ.toH10.grad x) 2 (normalizedCubeMeasure Q))
(hBg : 0 ≤ cubeBesovPositiveVectorSeminormTwo Q s fun (x : Vec d) => g x - cubeAverageVec Q g)
(huBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N u))
(hwBdd :
BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => w.toH1.grad x))
(hgBdd :
BddAbove
(Set.range fun (N : ℕ) =>
cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => g x - cubeAverageVec Q g))
:
cubeBesovNegativeVectorPartialSeminormTwo Q s (N + 1) u ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage Q 1 fun (R : TriadicCube d) => cubeBesovNegativeVectorPartialSeminormTwo R s N u ^ 2) + 2 * ((geometricDiscount s 2)⁻¹ * (lambdaSq Q s (MultiscaleExponent.finite 2) a)⁻¹) * cubeAverage Q (coefficientEnergyDensity a u) + η * cubeBesovNegativeVectorSeminormTwo Q s u ^ 2 + η * (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => w.toH1.grad x) ^ 2 + 2 * η⁻¹ * ((geometricDiscount s 2)⁻¹ * (lambdaSq Q s (MultiscaleExponent.finite 2) a)⁻¹ * (↑d * (3 ^ (↑d + s) * √2)) * cubeBesovPositiveVectorSeminormTwo Q s fun (x : Vec d) => g x - cubeAverageVec Q g) ^ 2
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.sq_negativePartialSeminormTwo_harmonic_le_energy_add_correction_two
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ρ : ZeroTraceDirichletCorrectorData Q a g)
{u : Vec d → Vec d}
(w : AHarmonicFunction a (cubeSet Q))
{lam Lam : ℝ}
(s : ℝ)
(hs : 0 < s)
(N : ℕ)
(hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a)
(hu : MemVectorL2 (cubeSet Q) u)
(hgrad :
CubeAverageGradientEnergyControl Q a (fun (x : Vec d) => w.toH1.grad x)
(coefficientEnergyDensity a fun (x : Vec d) => w.toH1.grad x))
(hsum : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a)
(huw : ∀ x ∈ cubeSet Q, u x = w.toH1.grad x + ρ.toH10.grad x)
(hmem : MemVectorL2 (cubeSet Q) g)
(hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q))
(hgradρ : MeasureTheory.MemLp (fun (x : Vec d) => ρ.toH10.grad x) 2 (normalizedCubeMeasure Q))
(hBg : 0 ≤ cubeBesovPositiveVectorSeminormTwo Q s fun (x : Vec d) => g x - cubeAverageVec Q g)
(huBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N u))
(hwBdd :
BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => w.toH1.grad x))
(hgBdd :
BddAbove
(Set.range fun (N : ℕ) =>
cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => g x - cubeAverageVec Q g))
:
(cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => w.toH1.grad x) ^ 2 ≤ 2 * ((geometricDiscount s 2)⁻¹ * (lambdaSq Q s (MultiscaleExponent.finite 2) a)⁻¹) * cubeAverage Q (coefficientEnergyDensity a u) + 2 * ((geometricDiscount s 2)⁻¹ * (lambdaSq Q s (MultiscaleExponent.finite 2) a)⁻¹) * (↑d * (3 ^ (↑d + s) * (√2 * (cubeBesovNegativeVectorSeminormTwo Q s u + cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => w.toH1.grad x)) * cubeBesovPositiveVectorSeminormTwo Q s fun (x : Vec d) => g x - cubeAverageVec Q g))
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.sq_negativeBesovSeminormTwo_harmonic_le_energy_add_correction_two
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ρ : ZeroTraceDirichletCorrectorData Q a g)
{u : Vec d → Vec d}
(w : AHarmonicFunction a (cubeSet Q))
{lam Lam : ℝ}
(s : ℝ)
(hs : 0 < s)
(hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a)
(hu : MemVectorL2 (cubeSet Q) u)
(hgrad :
CubeAverageGradientEnergyControl Q a (fun (x : Vec d) => w.toH1.grad x)
(coefficientEnergyDensity a fun (x : Vec d) => w.toH1.grad x))
(hsum : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a)
(huw : ∀ x ∈ cubeSet Q, u x = w.toH1.grad x + ρ.toH10.grad x)
(hmem : MemVectorL2 (cubeSet Q) g)
(hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q))
(hgradρ : MeasureTheory.MemLp (fun (x : Vec d) => ρ.toH10.grad x) 2 (normalizedCubeMeasure Q))
(hBg : 0 ≤ cubeBesovPositiveVectorSeminormTwo Q s fun (x : Vec d) => g x - cubeAverageVec Q g)
(huBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N u))
(hwBdd :
BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => w.toH1.grad x))
(hgBdd :
BddAbove
(Set.range fun (N : ℕ) =>
cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => g x - cubeAverageVec Q g))
:
(cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => w.toH1.grad x) ^ 2 ≤ 2 * ((geometricDiscount s 2)⁻¹ * (lambdaSq Q s (MultiscaleExponent.finite 2) a)⁻¹) * cubeAverage Q (coefficientEnergyDensity a u) + 2 * ((geometricDiscount s 2)⁻¹ * (lambdaSq Q s (MultiscaleExponent.finite 2) a)⁻¹) * (↑d * (3 ^ (↑d + s) * (√2 * (cubeBesovNegativeVectorSeminormTwo Q s u + cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => w.toH1.grad x)) * cubeBesovPositiveVectorSeminormTwo Q s fun (x : Vec d) => g x - cubeAverageVec Q g))
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.sq_negativeBesovSeminormTwo_harmonic_le_energy_add_YoungError
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ρ : ZeroTraceDirichletCorrectorData Q a g)
{u : Vec d → Vec d}
(w : AHarmonicFunction a (cubeSet Q))
{lam Lam : ℝ}
(s : ℝ)
{η : ℝ}
(hs : 0 < s)
(hη : 0 < η)
(hη_lt : η < 1)
(hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a)
(hu : MemVectorL2 (cubeSet Q) u)
(hgrad :
CubeAverageGradientEnergyControl Q a (fun (x : Vec d) => w.toH1.grad x)
(coefficientEnergyDensity a fun (x : Vec d) => w.toH1.grad x))
(hsum : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a)
(huw : ∀ x ∈ cubeSet Q, u x = w.toH1.grad x + ρ.toH10.grad x)
(hmem : MemVectorL2 (cubeSet Q) g)
(hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q))
(hgradρ : MeasureTheory.MemLp (fun (x : Vec d) => ρ.toH10.grad x) 2 (normalizedCubeMeasure Q))
(hBg : 0 ≤ cubeBesovPositiveVectorSeminormTwo Q s fun (x : Vec d) => g x - cubeAverageVec Q g)
(huBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N u))
(hwBdd :
BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => w.toH1.grad x))
(hgBdd :
BddAbove
(Set.range fun (N : ℕ) =>
cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => g x - cubeAverageVec Q g))
:
(cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => w.toH1.grad x) ^ 2 ≤ (1 - η)⁻¹ * (2 * ((geometricDiscount s 2)⁻¹ * (lambdaSq Q s (MultiscaleExponent.finite 2) a)⁻¹) * cubeAverage Q (coefficientEnergyDensity a u) + η * cubeBesovNegativeVectorSeminormTwo Q s u ^ 2 + 2 * η⁻¹ * ((geometricDiscount s 2)⁻¹ * (lambdaSq Q s (MultiscaleExponent.finite 2) a)⁻¹ * (↑d * (3 ^ (↑d + s) * √2)) * cubeBesovPositiveVectorSeminormTwo Q s fun (x : Vec d) => g x - cubeAverageVec Q g) ^ 2)
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.sq_negativePartialSeminormTwo_succ_le_childMean_add_energy_add_error
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ρ : ZeroTraceDirichletCorrectorData Q a g)
{u : Vec d → Vec d}
(w : AHarmonicFunction a (cubeSet Q))
{lam Lam : ℝ}
(s : ℝ)
{η : ℝ}
(hs : 0 < s)
(hη : 0 < η)
(hη_lt : η < 1)
(N : ℕ)
(hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a)
(hu : MemVectorL2 (cubeSet Q) u)
(hgrad :
CubeAverageGradientEnergyControl Q a (fun (x : Vec d) => w.toH1.grad x)
(coefficientEnergyDensity a fun (x : Vec d) => w.toH1.grad x))
(hsum : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a)
(huw : ∀ x ∈ cubeSet Q, u x = w.toH1.grad x + ρ.toH10.grad x)
(hmem : MemVectorL2 (cubeSet Q) g)
(hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q))
(hgradρ : MeasureTheory.MemLp (fun (x : Vec d) => ρ.toH10.grad x) 2 (normalizedCubeMeasure Q))
(hBg : 0 ≤ cubeBesovPositiveVectorSeminormTwo Q s fun (x : Vec d) => g x - cubeAverageVec Q g)
(huBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N u))
(hwBdd :
BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => w.toH1.grad x))
(hgBdd :
BddAbove
(Set.range fun (N : ℕ) =>
cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => g x - cubeAverageVec Q g))
:
cubeBesovNegativeVectorPartialSeminormTwo Q s (N + 1) u ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage Q 1 fun (R : TriadicCube d) => cubeBesovNegativeVectorPartialSeminormTwo R s N u ^ 2) + 2 * ((geometricDiscount s 2)⁻¹ * (lambdaSq Q s (MultiscaleExponent.finite 2) a)⁻¹) * cubeAverage Q (coefficientEnergyDensity a u) + η * cubeBesovNegativeVectorSeminormTwo Q s u ^ 2 + η * ((1 - η)⁻¹ * (2 * ((geometricDiscount s 2)⁻¹ * (lambdaSq Q s (MultiscaleExponent.finite 2) a)⁻¹) * cubeAverage Q (coefficientEnergyDensity a u) + η * cubeBesovNegativeVectorSeminormTwo Q s u ^ 2 + 2 * η⁻¹ * ((geometricDiscount s 2)⁻¹ * (lambdaSq Q s (MultiscaleExponent.finite 2) a)⁻¹ * (↑d * (3 ^ (↑d + s) * √2)) * cubeBesovPositiveVectorSeminormTwo Q s fun (x : Vec d) => g x - cubeAverageVec Q g) ^ 2)) + 2 * η⁻¹ * ((geometricDiscount s 2)⁻¹ * (lambdaSq Q s (MultiscaleExponent.finite 2) a)⁻¹ * (↑d * (3 ^ (↑d + s) * √2)) * cubeBesovPositiveVectorSeminormTwo Q s fun (x : Vec d) => g x - cubeAverageVec Q g) ^ 2
theorem
HCPolySupport.ZeroTraceDirichletCorrectorData.sq_negativeBesovSeminormTwo_le_childMean_add_energy_add_error
{d : ℕ}
{Q : TriadicCube d}
{a : CoeffField d}
{g : Vec d → Vec d}
(ρ : ZeroTraceDirichletCorrectorData Q a g)
{u : Vec d → Vec d}
(w : AHarmonicFunction a (cubeSet Q))
{lam Lam : ℝ}
(s : ℝ)
{η : ℝ}
(Bchild : TriadicCube d → ℝ)
(hs : 0 < s)
(hη : 0 < η)
(hη_lt : η < 1)
(hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a)
(hu : MemVectorL2 (cubeSet Q) u)
(hgrad :
CubeAverageGradientEnergyControl Q a (fun (x : Vec d) => w.toH1.grad x)
(coefficientEnergyDensity a fun (x : Vec d) => w.toH1.grad x))
(hsum : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a)
(huw : ∀ x ∈ cubeSet Q, u x = w.toH1.grad x + ρ.toH10.grad x)
(hmem : MemVectorL2 (cubeSet Q) g)
(hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q))
(hgradρ : MeasureTheory.MemLp (fun (x : Vec d) => ρ.toH10.grad x) 2 (normalizedCubeMeasure Q))
(hBg : 0 ≤ cubeBesovPositiveVectorSeminormTwo Q s fun (x : Vec d) => g x - cubeAverageVec Q g)
(huBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N u))
(hwBdd :
BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => w.toH1.grad x))
(hgBdd :
BddAbove
(Set.range fun (N : ℕ) =>
cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => g x - cubeAverageVec Q g))
(hchild : ∀ R ∈ descendantsAtDepth Q 1, ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminormTwo R s N u ≤ Bchild R)
:
cubeBesovNegativeVectorSeminormTwo Q s u ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage Q 1 fun (R : TriadicCube d) => Bchild R ^ 2) + 2 * ((geometricDiscount s 2)⁻¹ * (lambdaSq Q s (MultiscaleExponent.finite 2) a)⁻¹) * cubeAverage Q (coefficientEnergyDensity a u) + η * cubeBesovNegativeVectorSeminormTwo Q s u ^ 2 + η * ((1 - η)⁻¹ * (2 * ((geometricDiscount s 2)⁻¹ * (lambdaSq Q s (MultiscaleExponent.finite 2) a)⁻¹) * cubeAverage Q (coefficientEnergyDensity a u) + η * cubeBesovNegativeVectorSeminormTwo Q s u ^ 2 + 2 * η⁻¹ * ((geometricDiscount s 2)⁻¹ * (lambdaSq Q s (MultiscaleExponent.finite 2) a)⁻¹ * (↑d * (3 ^ (↑d + s) * √2)) * cubeBesovPositiveVectorSeminormTwo Q s fun (x : Vec d) => g x - cubeAverageVec Q g) ^ 2)) + 2 * η⁻¹ * ((geometricDiscount s 2)⁻¹ * (lambdaSq Q s (MultiscaleExponent.finite 2) a)⁻¹ * (↑d * (3 ^ (↑d + s) * √2)) * cubeBesovPositiveVectorSeminormTwo Q s fun (x : Vec d) => g x - cubeAverageVec Q g) ^ 2