Coarse-graining support: Support.Deterministic.CoarsePoincare.QTwo

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

theorem HCPolySupport.rpow_neg_two_mul_s_nat_eq_inv_geometricDiscount_mul_geometricWeight_two {s : ℝ} (hs : 0 < s) (j : ℕ) : Real.rpow 3 (-2 * s * ↑j) = (geometricDiscount s 2)⁻¹ * geometricWeight s 2 j

theorem HCPolySupport.sq_coarsePoincare_gradient_qtwo_partial_of_cubeAverageEnergyControl {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (hs : 0 < s) (g : Vec d → Vec d) (energy : Vec d → ℝ) (N : ℕ) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) (hgrad : CubeAverageGradientEnergyControl Q a g energy) (hsum : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a) : cubeBesovNegativeVectorPartialSeminormTwo Q s N g ^ 2 ≤ (geometricDiscount s 2)⁻¹ * (lambdaSq Q s (MultiscaleExponent.finite 2) a)⁻¹ * cubeAverage Q energy

theorem HCPolySupport.coarsePoincare_gradient_qtwo_partial_of_cubeAverageEnergyControl {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (hs : 0 < s) (g : Vec d → Vec d) (energy : Vec d → ℝ) (N : ℕ) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) (hgrad : CubeAverageGradientEnergyControl Q a g energy) (hsum : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a) : cubeBesovNegativeVectorPartialSeminormTwo Q s N g ≤ (geometricDiscount s 2).rpow (-1 / 2) * (lambdaSq Q s (MultiscaleExponent.finite 2) a).rpow (-1 / 2) * √(cubeAverage Q energy)

theorem HCPolySupport.coarsePoincare_gradient_qtwo_of_cubeAverageEnergyControl {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (hs : 0 < s) (g : Vec d → Vec d) (energy : Vec d → ℝ) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) (hgrad : CubeAverageGradientEnergyControl Q a g energy) (hsum : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a) : cubeBesovNegativeVectorSeminormTwo Q s g ≤ (geometricDiscount s 2).rpow (-1 / 2) * (lambdaSq Q s (MultiscaleExponent.finite 2) a).rpow (-1 / 2) * √(cubeAverage Q energy)

Note-facing q = 2 gradient coarse Poincare inequality under descendant cube-average energy control.

theorem HCPolySupport.sq_coarsePoincare_flux_qtwo_partial_of_cubeAverageEnergyControl {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (hs : 0 < s) (flux : Vec d → Vec d) (energy : Vec d → ℝ) (N : ℕ) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) (hflux : CubeAverageFluxEnergyControl Q a flux energy) (hsum : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a) : cubeBesovNegativeVectorPartialSeminormTwo Q s N flux ^ 2 ≤ (geometricDiscount s 2)⁻¹ * LambdaSq Q s (MultiscaleExponent.finite 2) a * cubeAverage Q energy

Squared finite-depth q = 2 flux coarse Poincare inequality under descendant cube-average energy control.

theorem HCPolySupport.coarsePoincare_flux_qtwo_partial_of_cubeAverageEnergyControl {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (hs : 0 < s) (flux : Vec d → Vec d) (energy : Vec d → ℝ) (N : ℕ) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) (hflux : CubeAverageFluxEnergyControl Q a flux energy) (hsum : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a) : cubeBesovNegativeVectorPartialSeminormTwo Q s N flux ≤ (geometricDiscount s 2).rpow (-1 / 2) * (LambdaSq Q s (MultiscaleExponent.finite 2) a).rpow (1 / 2) * √(cubeAverage Q energy)

Note-facing q = 2 finite-depth flux coarse Poincare inequality under descendant cube-average energy control.

theorem HCPolySupport.coarsePoincare_flux_qtwo_of_cubeAverageEnergyControl {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (hs : 0 < s) (flux : Vec d → Vec d) (energy : Vec d → ℝ) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) (hflux : CubeAverageFluxEnergyControl Q a flux energy) (hsum : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a) : cubeBesovNegativeVectorSeminormTwo Q s flux ≤ (geometricDiscount s 2).rpow (-1 / 2) * (LambdaSq Q s (MultiscaleExponent.finite 2) a).rpow (1 / 2) * √(cubeAverage Q energy)

Note-facing q = 2 flux coarse Poincare inequality under descendant cube-average energy control.

theorem HCPolySupport.coarsePoincare_qtwo_note_bounds_of_cubeAverageEnergyControl {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (hs : 0 < s) (g flux : Vec d → Vec d) (energy : Vec d → ℝ) (henergy_nonneg : ∀ x ∈ cubeSet Q, 0 ≤ energy x) (henergy_int : MeasureTheory.IntegrableOn energy (cubeSet Q) MeasureTheory.volume) (hgrad : CubeAverageGradientEnergyControl Q a g energy) (hflux : CubeAverageFluxEnergyControl Q a flux energy) (hsum_grad : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a) (hsum_flux : Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a) : cubeBesovNegativeVectorSeminormTwo Q s g ≤ (geometricDiscount s 2).rpow (-1 / 2) * (lambdaSq Q s (MultiscaleExponent.finite 2) a).rpow (-1 / 2) * √(cubeAverage Q energy) ∧ cubeBesovNegativeVectorSeminormTwo Q s flux ≤ (geometricDiscount s 2).rpow (-1 / 2) * (LambdaSq Q s (MultiscaleExponent.finite 2) a).rpow (1 / 2) * √(cubeAverage Q energy)

Note-facing q = 2 gradient and flux coarse Poincare bounds under direct descendant cube-average energy control.

theorem HCPolySupport.coarsePoincare_qtwo_note_bounds_of_aHarmonicFunction {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) {lam Lam : ℝ} (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (u : AHarmonicFunction a (cubeSet Q)) : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => u.toH1.grad x) ≤ (geometricDiscount s 2).rpow (-1 / 2) * (lambdaSq Q s (MultiscaleExponent.finite 2) a).rpow (-1 / 2) * √(cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a u x) ∧ (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (a x) (u.toH1.grad x)) ≤ (geometricDiscount s 2).rpow (-1 / 2) * (LambdaSq Q s (MultiscaleExponent.finite 2) a).rpow (1 / 2) * √(cubeAverage Q fun (x : Vec d) => scalarVariationEnergyIntegrand a u x)

Note-facing q = 2 gradient and flux coarse Poincare bounds for one harmonic field on the parent cube.