Coarse-graining support: Support.Deterministic.CoarsePoincareRHS.GlobalIteration #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.coarsePoincareRHSSn_terminal_tendsto_of_bddAbove
{d : ℕ}
(Q : TriadicCube d)
(u : Vec d → Vec d)
{s θ : ℝ}
(m : ℕ)
(hr_nonneg : 0 ≤ coarsePoincareRHSFiniteSumRatio s θ)
(hr_lt_one : coarsePoincareRHSFiniteSumRatio s θ < 1)
(hS_bdd : BddAbove (Set.range fun (n : ℕ) => coarsePoincareRHSSn Q s u n))
:
Filter.Tendsto (fun (N : ℕ) => coarsePoincareRHSScaledStepCoeff s θ ^ N * coarsePoincareRHSSn Q s u (m + N))
Filter.atTop (nhds 0)
theorem
HCPolySupport.coarsePoincareRHSSn_le_intrinsicGlobalEnergy_add_globalForce_of_terminal_tendsto
{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 : ℕ)
{E F : ℝ}
(hterminal :
Filter.Tendsto (fun (N : ℕ) => coarsePoincareRHSScaledStepCoeff s θ ^ N * coarsePoincareRHSSn Q s u (m + N))
Filter.atTop (nhds 0))
(hEbound : ∀ (N : ℕ), coarsePoincareRHSSIntrinsicWeightedGlobalEnergyErrorSum Q a u s θ CE m N ≤ E)
(hFbound : ∀ (N : ℕ), coarsePoincareRHSSIntrinsicWeightedGlobalForceErrorSum Q a g s θ CF m N ≤ F)
:
theorem
HCPolySupport.coarsePoincareRHSSn_le_intrinsicGlobalEnergyForce_noteStep_of_bddAbove
{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θ : (1 - coarsePoincareRHSAbsorbedRnCoeff η)⁻¹ * coarsePoincareRHSDiscount s ≤ coarsePoincareRHSNoteStepCoeff 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))
(hS_bdd : BddAbove (Set.range fun (n : ℕ) => coarsePoincareRHSSn Q s u 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 : ℕ)
:
theorem
HCPolySupport.coarsePoincareRHSSn_le_intrinsicGlobalEnergyForce_noteConstants
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
(a : CoeffField d)
(g u : Vec d → Vec d)
{s lam Lam : ℝ}
(hs : 0 < s)
(hs_le : s ≤ 1)
(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)
(hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q))
(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 (coarsePoincareRHSNoteEta s))
(m : ℕ)
:
coarsePoincareRHSSn Q s u m ≤ coarsePoincareRHSSIntrinsicGlobalEnergyBase Q a u s 5 m * (5 * s⁻¹) + coarsePoincareRHSSIntrinsicGlobalForceBase Q a g s (120 * s⁻¹) m * (5 * s⁻¹)