Coarse-graining support: Support.Deterministic.CoarsePoincareRHS.LocalizedIteration #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.coarsePoincareRHSRn_iterate_le_intrinsicLocalizedEnergyForce_of_forceAverageBound
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(g u : Vec d → Vec d)
{s lam Lam η θ CE CF : ℝ}
(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)
(habs : 0 < 1 - coarsePoincareRHSAbsorbedRnCoeff η)
(hθ_nonneg : 0 ≤ θ)
(hθ : (1 - coarsePoincareRHSAbsorbedRnCoeff η)⁻¹ * coarsePoincareRHSDiscount s ≤ θ)
(hEcoeff : (1 - coarsePoincareRHSAbsorbedRnCoeff η)⁻¹ * coarsePoincareRHSAbsorbedEnergyCoeff η ≤ CE)
(hFcoeff : (1 - coarsePoincareRHSAbsorbedRnCoeff η)⁻¹ * coarsePoincareRHSAbsorbedForceCoeff η ≤ CF)
(hCE_nonneg : 0 ≤ CE)
(hCF_nonneg : 0 ≤ CF)
(havg_nonneg : ∀ (n : ℕ), ∀ R ∈ descendantsAtDepth Q n, 0 ≤ cubeAverage R (coefficientEnergyDensity a u))
(hint : MeasureTheory.IntegrableOn (coefficientEnergyDensity a u) (cubeSet Q) MeasureTheory.volume)
(hmem : ∀ (j : ℕ), ∀ S ∈ descendantsAtDepth Q j, MeasureTheory.MemLp g 2 (normalizedCubeMeasure S))
(hforceAvg :
∀ (n : ℕ), (descendantsAverage Q n fun (R : TriadicCube d) => cubeBesovPositiveVectorSeminormTwo R s g ^ 2) ≤ B n)
(hlocal :
∀ (n : ℕ),
∀ R ∈ descendantsAtDepth Q n,
cubeBesovNegativeVectorSeminormTwo R s u ^ 2 ≤ coarsePoincareRHSDiscount s * coarsePoincareRHSRn R s u 1 + coarsePoincareRHSIntrinsicAbsorbedLocalError R a g u s η)
(m N : ℕ)
:
coarsePoincareRHSRn Q s u m ≤ θ ^ N * coarsePoincareRHSRn Q s u (m + N) + coarsePoincareRHSIntrinsicWeightedLocalizedEnergyForceErrorSum Q a u s θ CE CF B m N
theorem
HCPolySupport.coarsePoincareRHSSn_iterate_le_intrinsicLocalizedEnergyForce_of_forceAverageBound
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(g u : Vec d → Vec d)
{s lam Lam η θ CE CF : ℝ}
(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)
(habs : 0 < 1 - coarsePoincareRHSAbsorbedRnCoeff η)
(hθ_nonneg : 0 ≤ θ)
(hθ : (1 - coarsePoincareRHSAbsorbedRnCoeff η)⁻¹ * coarsePoincareRHSDiscount s ≤ θ)
(hEcoeff : (1 - coarsePoincareRHSAbsorbedRnCoeff η)⁻¹ * coarsePoincareRHSAbsorbedEnergyCoeff η ≤ CE)
(hFcoeff : (1 - coarsePoincareRHSAbsorbedRnCoeff η)⁻¹ * coarsePoincareRHSAbsorbedForceCoeff η ≤ CF)
(hCE_nonneg : 0 ≤ CE)
(hCF_nonneg : 0 ≤ CF)
(havg_nonneg : ∀ (n : ℕ), ∀ R ∈ descendantsAtDepth Q n, 0 ≤ cubeAverage R (coefficientEnergyDensity a u))
(hint : MeasureTheory.IntegrableOn (coefficientEnergyDensity a u) (cubeSet Q) MeasureTheory.volume)
(hmem : ∀ (j : ℕ), ∀ S ∈ descendantsAtDepth Q j, MeasureTheory.MemLp g 2 (normalizedCubeMeasure S))
(hforceAvg :
∀ (n : ℕ), (descendantsAverage Q n fun (R : TriadicCube d) => cubeBesovPositiveVectorSeminormTwo R s g ^ 2) ≤ B n)
(hlocal :
∀ (n : ℕ),
∀ R ∈ descendantsAtDepth Q n,
cubeBesovNegativeVectorSeminormTwo R s u ^ 2 ≤ coarsePoincareRHSDiscount s * coarsePoincareRHSRn R s u 1 + coarsePoincareRHSIntrinsicAbsorbedLocalError R a g u s η)
(m N : ℕ)
:
coarsePoincareRHSSn Q s u m ≤ coarsePoincareRHSScaledStepCoeff s θ ^ N * coarsePoincareRHSSn Q s u (m + N) + coarsePoincareRHSSIntrinsicWeightedLocalizedEnergyForceErrorSum Q a u s θ CE CF B m N
theorem
HCPolySupport.coarsePoincareRHSSn_iterate_le_intrinsicLocalizedEnergyForce_of_globalForceBound
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(g u : Vec d → Vec d)
{s lam Lam η θ CE CF : ℝ}
(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)
(habs : 0 < 1 - coarsePoincareRHSAbsorbedRnCoeff η)
(hθ_nonneg : 0 ≤ θ)
(hθ : (1 - coarsePoincareRHSAbsorbedRnCoeff η)⁻¹ * coarsePoincareRHSDiscount s ≤ θ)
(hEcoeff : (1 - coarsePoincareRHSAbsorbedRnCoeff η)⁻¹ * coarsePoincareRHSAbsorbedEnergyCoeff η ≤ CE)
(hFcoeff : (1 - coarsePoincareRHSAbsorbedRnCoeff η)⁻¹ * coarsePoincareRHSAbsorbedForceCoeff η ≤ CF)
(hCE_nonneg : 0 ≤ CE)
(hCF_nonneg : 0 ≤ CF)
(havg_nonneg : ∀ (n : ℕ), ∀ R ∈ descendantsAtDepth Q n, 0 ≤ cubeAverage R (coefficientEnergyDensity a u))
(hint : MeasureTheory.IntegrableOn (coefficientEnergyDensity a u) (cubeSet Q) MeasureTheory.volume)
(hmem : ∀ (j : ℕ), ∀ S ∈ descendantsAtDepth Q j, MeasureTheory.MemLp g 2 (normalizedCubeMeasure S))
(hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g))
(hLocalBdd :
∀ (n : ℕ),
∀ R ∈ descendantsAtDepth Q n, BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N g))
(hlocal :
∀ (n : ℕ),
∀ R ∈ descendantsAtDepth Q n,
cubeBesovNegativeVectorSeminormTwo R s u ^ 2 ≤ coarsePoincareRHSDiscount s * coarsePoincareRHSRn R s u 1 + coarsePoincareRHSIntrinsicAbsorbedLocalError R a g u s η)
(m N : ℕ)
:
coarsePoincareRHSSn Q s u m ≤ coarsePoincareRHSScaledStepCoeff s θ ^ N * coarsePoincareRHSSn Q s u (m + N) + coarsePoincareRHSSIntrinsicWeightedLocalizedEnergyForceErrorSum Q a u s θ CE CF
(fun (n : ℕ) => coarsePoincareRHSGlobalForceBound Q g s n) m N
theorem
HCPolySupport.coarsePoincareRHSSn_iterate_le_intrinsicGlobalEnergy_add_globalForce
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(g u : Vec d → Vec d)
{s lam Lam η θ CE CF : ℝ}
(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)
(habs : 0 < 1 - coarsePoincareRHSAbsorbedRnCoeff η)
(hθ_nonneg : 0 ≤ θ)
(hθ : (1 - coarsePoincareRHSAbsorbedRnCoeff η)⁻¹ * coarsePoincareRHSDiscount s ≤ θ)
(hEcoeff : (1 - coarsePoincareRHSAbsorbedRnCoeff η)⁻¹ * coarsePoincareRHSAbsorbedEnergyCoeff η ≤ CE)
(hFcoeff : (1 - coarsePoincareRHSAbsorbedRnCoeff η)⁻¹ * coarsePoincareRHSAbsorbedForceCoeff η ≤ CF)
(hCE_nonneg : 0 ≤ CE)
(hCF_nonneg : 0 ≤ CF)
(havg_nonneg : ∀ (n : ℕ), ∀ R ∈ descendantsAtDepth Q n, 0 ≤ cubeAverage R (coefficientEnergyDensity a u))
(hint : MeasureTheory.IntegrableOn (coefficientEnergyDensity a u) (cubeSet Q) MeasureTheory.volume)
(hmem : ∀ (j : ℕ), ∀ S ∈ descendantsAtDepth Q j, MeasureTheory.MemLp g 2 (normalizedCubeMeasure S))
(hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g))
(hLocalBdd :
∀ (n : ℕ),
∀ R ∈ descendantsAtDepth Q n, BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N g))
(hlocal :
∀ (n : ℕ),
∀ R ∈ descendantsAtDepth Q n,
cubeBesovNegativeVectorSeminormTwo R s u ^ 2 ≤ coarsePoincareRHSDiscount s * coarsePoincareRHSRn R s u 1 + coarsePoincareRHSIntrinsicAbsorbedLocalError R a g u s η)
(m N : ℕ)
:
coarsePoincareRHSSn Q s u m ≤ coarsePoincareRHSScaledStepCoeff s θ ^ N * coarsePoincareRHSSn Q s u (m + N) + coarsePoincareRHSSIntrinsicWeightedGlobalEnergyErrorSum Q a u s θ CE m N + coarsePoincareRHSSIntrinsicWeightedGlobalForceErrorSum Q a g s θ CF m N