Coarse-graining support: Support.Deterministic.CoarsePoincareRHS.ForceLocalization

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

theorem HCPolySupport.coarsePoincareRHSLocalCoeff_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s : ℝ} (hs : 0 < s) : 0 ≤ coarsePoincareRHSLocalCoeff Q a s

theorem HCPolySupport.coarsePoincareRHSLocalCenteredForceSeminorm_eq_uncentered_of_mem {d : ℕ} {Q R : TriadicCube d} (g : Vec d → Vec d) (s : ℝ) {n : ℕ} (hR : R ∈ descendantsAtDepth Q n) (hmem : ∀ (j : ℕ), ∀ S ∈ descendantsAtDepth Q j, MeasureTheory.MemLp g 2 (normalizedCubeMeasure S)) : coarsePoincareRHSLocalCenteredForceSeminorm R g s = cubeBesovPositiveVectorSeminormTwo R s g

theorem HCPolySupport.descendantsAverage_sq_coarsePoincareRHSLocalCenteredForceSeminorm_eq_of_mem {d : ℕ} (Q : TriadicCube d) (g : Vec d → Vec d) (s : ℝ) (n : ℕ) (hmem : ∀ (j : ℕ), ∀ S ∈ descendantsAtDepth Q j, MeasureTheory.MemLp g 2 (normalizedCubeMeasure S)) : (descendantsAverage Q n fun (R : TriadicCube d) => coarsePoincareRHSLocalCenteredForceSeminorm R g s ^ 2) = descendantsAverage Q n fun (R : TriadicCube d) => cubeBesovPositiveVectorSeminormTwo R s g ^ 2

theorem HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo_bddAbove_of_parent_bddAbove {d : ℕ} {Q R : TriadicCube d} {n : ℕ} (s : ℝ) (u : Vec d → Vec d) (hR : R ∈ descendantsAtDepth Q n) (hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N u)) : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N u)

theorem HCPolySupport.tendsto_cubeBesovPositiveVectorPartialSeminormTwo_atTop {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (hBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N u)) : Filter.Tendsto (fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N u) Filter.atTop (nhds (cubeBesovPositiveVectorSeminormTwo Q s u))

theorem HCPolySupport.tendsto_sq_scaled_cubeBesovPositiveVectorPartialSeminormTwo_atTop {d : ℕ} (Q : TriadicCube d) (s c : ℝ) (u : Vec d → Vec d) (hBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N u)) : Filter.Tendsto (fun (N : ℕ) => (c * cubeBesovPositiveVectorPartialSeminormTwo Q s N u) ^ 2) Filter.atTop (nhds ((c * cubeBesovPositiveVectorSeminormTwo Q s u) ^ 2))

theorem HCPolySupport.tendsto_descendantsAverage_sq_scaled_cubeBesovPositiveVectorPartialSeminormTwo_atTop {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (n : ℕ) (hLocalBdd : ∀ R ∈ descendantsAtDepth Q n, BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N u)) : Filter.Tendsto (fun (N : ℕ) => descendantsAverage Q n fun (R : TriadicCube d) => (Real.rpow 3 (s * ↑n) * cubeBesovPositiveVectorPartialSeminormTwo R s N u) ^ 2) Filter.atTop (nhds (descendantsAverage Q n fun (R : TriadicCube d) => (Real.rpow 3 (s * ↑n) * cubeBesovPositiveVectorSeminormTwo R s u) ^ 2))

theorem HCPolySupport.descendantsAverage_sq_scaled_cubeBesovPositiveVectorSeminormTwo_le {d : ℕ} (Q : TriadicCube d) (g : Vec d → Vec d) (s : ℝ) (n : ℕ) (hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (hLocalBdd : ∀ R ∈ descendantsAtDepth Q n, BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N g)) : (descendantsAverage Q n fun (R : TriadicCube d) => (Real.rpow 3 (s * ↑n) * cubeBesovPositiveVectorSeminormTwo R s g) ^ 2) ≤ cubeBesovPositiveVectorSeminormTwo Q s g ^ 2

theorem HCPolySupport.descendantsAverage_sq_cubeBesovPositiveVectorSeminormTwo_le_parent_of_bddAbove {d : ℕ} (Q : TriadicCube d) (g : Vec d → Vec d) {s : ℝ} (n : ℕ) (hs : 0 ≤ s) (hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (hLocalBdd : ∀ R ∈ descendantsAtDepth Q n, BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N g)) : (descendantsAverage Q n fun (R : TriadicCube d) => cubeBesovPositiveVectorSeminormTwo R s g ^ 2) ≤ cubeBesovPositiveVectorSeminormTwo Q s g ^ 2

Unscaled parent-seminorm corollary of descendantsAverage_sq_scaled_cubeBesovPositiveVectorSeminormTwo_le.

theorem HCPolySupport.descendantsAverage_sq_cubeBesovPositiveVectorSeminormTwo_le_global_scaled {d : ℕ} (Q : TriadicCube d) (g : Vec d → Vec d) (s : ℝ) (n : ℕ) (hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (hLocalBdd : ∀ R ∈ descendantsAtDepth Q n, BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N g)) : (descendantsAverage Q n fun (R : TriadicCube d) => cubeBesovPositiveVectorSeminormTwo R s g ^ 2) ≤ coarsePoincareRHSGlobalForceBound Q g s n

noncomputable def HCPolySupport.localizedPositiveBesovForcingSeminormTwoAtDepth {d : ℕ} (Q : TriadicCube d) (s : ℝ) (n : ℕ) (g : Vec d → Vec d) : ℝ

Localized descendant L² average of the positive forcing seminorm at a fixed depth. This is the quantity whose parent-cube control carries the small factor 3^{-s n}.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.sqrt_coarsePoincareRHSGlobalForceBound_eq_depthWeight_inv_mul_parent_of_bddAbove {d : ℕ} (Q : TriadicCube d) (g : Vec d → Vec d) (s : ℝ) (n : ℕ) (hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) : √(coarsePoincareRHSGlobalForceBound Q g s n) = (Real.rpow 3 (s * ↑n))⁻¹ * cubeBesovPositiveVectorSeminormTwo Q s g

The square root of the global force bound is the inverse depth weight times the parent positive-Besov seminorm.

theorem HCPolySupport.localizedPositiveBesovForcingSeminormTwoAtDepth_le_depthWeight_inv_mul_parent_of_bddAbove {d : ℕ} (Q : TriadicCube d) (g : Vec d → Vec d) (s : ℝ) (n : ℕ) (hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (hLocalBdd : ∀ R ∈ descendantsAtDepth Q n, BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N g)) : localizedPositiveBesovForcingSeminormTwoAtDepth Q s n g ≤ (Real.rpow 3 (s * ↑n))⁻¹ * cubeBesovPositiveVectorSeminormTwo Q s g

Scale-sharp localization of the positive forcing seminorm: averaging the descendant forcing seminorms costs the inverse positive depth weight, not the positive depth weight.

theorem HCPolySupport.coarsePoincareRHSIntrinsicLocalForceError_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) (s : ℝ) : 0 ≤ coarsePoincareRHSIntrinsicLocalForceError Q a g s

theorem HCPolySupport.coarsePoincareRHSIntrinsicForceErrorAverage_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) (s : ℝ) (n : ℕ) : 0 ≤ coarsePoincareRHSIntrinsicForceErrorAverage Q a g s n

theorem HCPolySupport.coarsePoincareRHSIntrinsicEnergyErrorAverage_le_of_localCoeffBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (u : Vec d → Vec d) (s : ℝ) (n : ℕ) {C : ℝ} (hcoeff : ∀ R ∈ descendantsAtDepth Q n, coarsePoincareRHSLocalCoeff R a s ≤ C) (havg_nonneg : ∀ R ∈ descendantsAtDepth Q n, 0 ≤ cubeAverage R (coefficientEnergyDensity a u)) : coarsePoincareRHSIntrinsicEnergyErrorAverage Q a u s n ≤ 2 * C * descendantsAverage Q n fun (R : TriadicCube d) => cubeAverage R (coefficientEnergyDensity a u)

theorem HCPolySupport.coarsePoincareRHSIntrinsicEnergyErrorAverage_le_globalAverage_of_localCoeffBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (u : Vec d → Vec d) (s : ℝ) (n : ℕ) {C : ℝ} (hcoeff : ∀ R ∈ descendantsAtDepth Q n, coarsePoincareRHSLocalCoeff R a s ≤ C) (havg_nonneg : ∀ R ∈ descendantsAtDepth Q n, 0 ≤ cubeAverage R (coefficientEnergyDensity a u)) (hint : MeasureTheory.IntegrableOn (coefficientEnergyDensity a u) (cubeSet Q) MeasureTheory.volume) : coarsePoincareRHSIntrinsicEnergyErrorAverage Q a u s n ≤ 2 * C * cubeAverage Q (coefficientEnergyDensity a u)

theorem HCPolySupport.coarsePoincareRHSLocalCoeff_le_parentHalfLambda_of_mem_descendantsAtDepth {d : ℕ} [NeZero d] {Q R : TriadicCube d} (a : CoeffField d) {s lam Lam : ℝ} (n : ℕ) (hs : 0 < s) (hR : R ∈ descendantsAtDepth Q n) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : ∀ j ≤ Q.scale, ∀ S ∈ descendantsAtScale Q j, ∃ (sigmaS : Mat d) (sigmaStarS : Mat d) (kappaS : Mat d), IsCoarseBlockMatrix (openCubeSet S) a (deterministicCoarseBlockMatrix (openCubeSet S) a) ∧ IsSigmaStarCoarse (openCubeSet S) a sigmaStarS ∧ IsKappaCoarse (openCubeSet S) a sigmaStarS kappaS ∧ IsSigmaCoarse (openCubeSet S) a sigmaS sigmaStarS kappaS ∧ IsUnit (Matrix.det sigmaStarS)) (hsum_half : Summable fun (m : ℕ) => geometricWeight (s / 2) 2 m * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑m) a).rpow 1) : coarsePoincareRHSLocalCoeff R a s ≤ (geometricDiscount s 2)⁻¹ * (Real.rpow 3 (s * ↑n) * (lambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)⁻¹)

theorem HCPolySupport.coarsePoincareRHSIntrinsicEnergyErrorAverage_le_parentHalfCoeff_globalAverage {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (u : Vec d → Vec d) {s lam Lam : ℝ} (n : ℕ) (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : ∀ j ≤ Q.scale, ∀ S ∈ descendantsAtScale Q j, ∃ (sigmaS : Mat d) (sigmaStarS : Mat d) (kappaS : Mat d), IsCoarseBlockMatrix (openCubeSet S) a (deterministicCoarseBlockMatrix (openCubeSet S) a) ∧ IsSigmaStarCoarse (openCubeSet S) a sigmaStarS ∧ IsKappaCoarse (openCubeSet S) a sigmaStarS kappaS ∧ IsSigmaCoarse (openCubeSet S) a sigmaS sigmaStarS kappaS ∧ IsUnit (Matrix.det sigmaStarS)) (hsum_half : Summable fun (m : ℕ) => geometricWeight (s / 2) 2 m * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑m) a).rpow 1) (havg_nonneg : ∀ R ∈ descendantsAtDepth Q n, 0 ≤ cubeAverage R (coefficientEnergyDensity a u)) (hint : MeasureTheory.IntegrableOn (coefficientEnergyDensity a u) (cubeSet Q) MeasureTheory.volume) : coarsePoincareRHSIntrinsicEnergyErrorAverage Q a u s n ≤ 2 * coarsePoincareRHSParentHalfCoeff Q a s n * cubeAverage Q (coefficientEnergyDensity a u)

theorem HCPolySupport.coarsePoincareRHSIntrinsicForceErrorAverage_le_of_multiplierSqBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) (s : ℝ) (n : ℕ) {K2 : ℝ} (hmult : ∀ R ∈ descendantsAtDepth Q n, coarsePoincareRHSIntrinsicLocalForceMultiplier R a s ^ 2 ≤ K2) : coarsePoincareRHSIntrinsicForceErrorAverage Q a g s n ≤ K2 * descendantsAverage Q n fun (R : TriadicCube d) => coarsePoincareRHSLocalCenteredForceSeminorm R g s ^ 2

theorem HCPolySupport.coarsePoincareRHSIntrinsicLocalForceMultiplier_sq_le_of_localCoeffBound {d : ℕ} (R : TriadicCube d) (a : CoeffField d) {s C : ℝ} (hs : 0 < s) (hcoeff : coarsePoincareRHSLocalCoeff R a s ≤ C) : coarsePoincareRHSIntrinsicLocalForceMultiplier R a s ^ 2 ≤ (C * (↑d * (3 ^ (↑d + s) * √2))) ^ 2

theorem HCPolySupport.coarsePoincare_intrinsicForceMultiplier_sq_le_parentHalfLambda {d : ℕ} [NeZero d] {Q R : TriadicCube d} (a : CoeffField d) {s lam Lam : ℝ} (n : ℕ) (hs : 0 < s) (hR : R ∈ descendantsAtDepth Q n) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : ∀ j ≤ Q.scale, ∀ S ∈ descendantsAtScale Q j, ∃ (sigmaS : Mat d) (sigmaStarS : Mat d) (kappaS : Mat d), IsCoarseBlockMatrix (openCubeSet S) a (deterministicCoarseBlockMatrix (openCubeSet S) a) ∧ IsSigmaStarCoarse (openCubeSet S) a sigmaStarS ∧ IsKappaCoarse (openCubeSet S) a sigmaStarS kappaS ∧ IsSigmaCoarse (openCubeSet S) a sigmaS sigmaStarS kappaS ∧ IsUnit (Matrix.det sigmaStarS)) (hsum_half : Summable fun (m : ℕ) => geometricWeight (s / 2) 2 m * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑m) a).rpow 1) : coarsePoincareRHSIntrinsicLocalForceMultiplier R a s ^ 2 ≤ coarsePoincareRHSIntrinsicParentHalfForceMultiplier Q a s n ^ 2

theorem HCPolySupport.coarsePoincareRHSIntrinsicForceErrorAverage_le_of_multiplierSqBound_of_centeredForceAverageBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) (s : ℝ) (n : ℕ) {K2 B : ℝ} (hK2 : 0 ≤ K2) (hmult : ∀ R ∈ descendantsAtDepth Q n, coarsePoincareRHSIntrinsicLocalForceMultiplier R a s ^ 2 ≤ K2) (hforceAvg : (descendantsAverage Q n fun (R : TriadicCube d) => coarsePoincareRHSLocalCenteredForceSeminorm R g s ^ 2) ≤ B) : coarsePoincareRHSIntrinsicForceErrorAverage Q a g s n ≤ K2 * B

theorem HCPolySupport.coarsePoincareRHSIntrinsicForceErrorAverage_le_parentHalfLambda_of_centeredForceAverageBound {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) {s lam Lam : ℝ} (n : ℕ) {B : ℝ} (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : ∀ j ≤ Q.scale, ∀ S ∈ descendantsAtScale Q j, ∃ (sigmaS : Mat d) (sigmaStarS : Mat d) (kappaS : Mat d), IsCoarseBlockMatrix (openCubeSet S) a (deterministicCoarseBlockMatrix (openCubeSet S) a) ∧ IsSigmaStarCoarse (openCubeSet S) a sigmaStarS ∧ IsKappaCoarse (openCubeSet S) a sigmaStarS kappaS ∧ IsSigmaCoarse (openCubeSet S) a sigmaS sigmaStarS kappaS ∧ IsUnit (Matrix.det sigmaStarS)) (hsum_half : Summable fun (m : ℕ) => geometricWeight (s / 2) 2 m * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑m) a).rpow 1) (hforceAvg : (descendantsAverage Q n fun (R : TriadicCube d) => coarsePoincareRHSLocalCenteredForceSeminorm R g s ^ 2) ≤ B) : coarsePoincareRHSIntrinsicForceErrorAverage Q a g s n ≤ coarsePoincareRHSIntrinsicParentHalfForceMultiplier Q a s n ^ 2 * B