Documentation

LeanPool.HighContrastHomogenization.Support.Deterministic.WeakFluxRHS.AbsorbedGlobalIteration

Coarse-graining support: Support.Deterministic.WeakFluxRHS.AbsorbedGlobalIteration #

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

source
theorem HCPolySupport.weakFluxRhs_scaledAverage_sq_le_correctorEnergyError {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (u : Vec d → Vec d) (z : TriadicCube d → Vec d → Vec d) (hs : 0 < s) (hlocal : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage R 1 fun (S : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo S s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2) + weakFluxRHSCorrectorEnergyLocalError R a u (z R) s) (m : ℕ) {B : ℝ} (hBdd : BddAbove (Set.range fun (n : ℕ) => weakFluxRHSScaledAveragedSeminormSq Q a s u n)) (hB_nonneg : 0 ≤ B) (hterm : ∀ (k : ℕ), (coarsePoincareRHSDepthWeight s (m + k) * descendantsAverage Q (m + k) fun (R : TriadicCube d) => weakFluxRHSCorrectorEnergyLocalError R a u (z R) s) ≤ B) :
weakFluxRHSScaledAveragedSeminormSq Q a s u m ≤ B * (1 - Real.rpow 3 (-s))⁻¹

Scaled bounded-tail weak-flux iteration with the explicit corrector-energy local error as the recurrence error.

source
theorem HCPolySupport.weakFluxRHSScaledAveragedSeminormSq_le_correctorEnergyComponents_base_mul_inv_one_sub_of_bddAbove {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (u : Vec d → Vec d) (z : TriadicCube d → Vec d → Vec d) (hs : 0 < s) (hlocal : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage R 1 fun (S : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo S s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2) + weakFluxRHSCorrectorEnergyLocalError R a u (z R) s) (m : ℕ) {Bcoeff Bcorr : ℝ} (hBdd : BddAbove (Set.range fun (n : ℕ) => weakFluxRHSScaledAveragedSeminormSq Q a s u n)) (hBcoeff_nonneg : 0 ≤ Bcoeff) (hBcorr_nonneg : 0 ≤ Bcorr) (hcoeff : ∀ (k : ℕ), coarsePoincareRHSDepthWeight s (m + k) * weakFluxRHSLocalCoefficientEnergyErrorAverage Q a u s (m + k) ≤ Bcoeff) (hcorr : ∀ (k : ℕ), coarsePoincareRHSDepthWeight s (m + k) * weakFluxRHSLocalCorrectorEnergyErrorAverage Q a z s (m + k) ≤ Bcorr) :
weakFluxRHSScaledAveragedSeminormSq Q a s u m ≤ (Bcoeff + Bcorr) * (1 - Real.rpow 3 (-s))⁻¹

Scaled bounded-tail weak-flux iteration where the corrector-energy local error is controlled by separate averaged coefficient-energy bases.

source
theorem HCPolySupport.negativeBesovFluxAverage_matrixVectorMultiply_le_sqrt_of_boundedCorrectorError {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (u : Vec d → Vec d) (z : TriadicCube d → Vec d → Vec d) (hs : 0 < s) (hlocal : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage R 1 fun (S : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo S s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2) + weakFluxRHSCorrectorEnergyLocalError R a u (z R) s) (m : ℕ) {B : ℝ} (hBdd : BddAbove (Set.range fun (n : ℕ) => weakFluxRHSScaledAveragedSeminormSq Q a s u n)) (hB_nonneg : 0 ≤ B) (hterm : ∀ (k : ℕ), (coarsePoincareRHSDepthWeight s (m + k) * descendantsAverage Q (m + k) fun (R : TriadicCube d) => weakFluxRHSCorrectorEnergyLocalError R a u (z R) s) ≤ B) :
localizedFluxDefectNegativeBesovAverageTwo Q s (fun (x : Vec d) => matVecMul (a x) (u x)) m ≤ √((coarsePoincareRHSDepthWeight s m)⁻¹ * (B * (1 - Real.rpow 3 (-s))⁻¹))

Localized flux-defect form of the scaled bounded-tail weak-flux iteration with the explicit corrector-energy local-error envelope.

source
theorem HCPolySupport.negativeBesovFluxAverage_matrixVectorMultiply_le_sqrt_of_boundedAbove {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (u : Vec d → Vec d) (z : TriadicCube d → Vec d → Vec d) (hs : 0 < s) (hlocal : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage R 1 fun (S : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo S s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2) + weakFluxRHSCorrectorEnergyLocalError R a u (z R) s) (m : ℕ) {Bcoeff Bcorr : ℝ} (hBdd : BddAbove (Set.range fun (n : ℕ) => weakFluxRHSScaledAveragedSeminormSq Q a s u n)) (hBcoeff_nonneg : 0 ≤ Bcoeff) (hBcorr_nonneg : 0 ≤ Bcorr) (hcoeff : ∀ (k : ℕ), coarsePoincareRHSDepthWeight s (m + k) * weakFluxRHSLocalCoefficientEnergyErrorAverage Q a u s (m + k) ≤ Bcoeff) (hcorr : ∀ (k : ℕ), coarsePoincareRHSDepthWeight s (m + k) * weakFluxRHSLocalCorrectorEnergyErrorAverage Q a z s (m + k) ≤ Bcorr) :
localizedFluxDefectNegativeBesovAverageTwo Q s (fun (x : Vec d) => matVecMul (a x) (u x)) m ≤ √((coarsePoincareRHSDepthWeight s m)⁻¹ * ((Bcoeff + Bcorr) * (1 - Real.rpow 3 (-s))⁻¹))

Localized flux-defect form with separate corrector-energy component bases.

source
theorem HCPolySupport.weakFluxRHSScaledAveragedSeminormSq_le_absorbedLocalError_base_mul_inv_one_sub_of_bddAbove {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s η : ℝ) (u g : Vec d → Vec d) (v : TriadicCube d → Vec d → Vec d) (hs : 0 < s) (hlocal : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage R 1 fun (S : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo S s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2) + weakFluxRHSAbsorbedLocalError R a g u (v R) s η) (m : ℕ) {B : ℝ} (hBdd : BddAbove (Set.range fun (n : ℕ) => weakFluxRHSScaledAveragedSeminormSq Q a s u n)) (hB_nonneg : 0 ≤ B) (hterm : ∀ (k : ℕ), (coarsePoincareRHSDepthWeight s (m + k) * descendantsAverage Q (m + k) fun (R : TriadicCube d) => weakFluxRHSAbsorbedLocalError R a g u (v R) s η) ≤ B) :
weakFluxRHSScaledAveragedSeminormSq Q a s u m ≤ B * (1 - Real.rpow 3 (-s))⁻¹

Scaled bounded-tail weak-flux iteration with the explicit absorbed local error as the recurrence error.

source
theorem HCPolySupport.weakFluxRHSScaledAveragedSeminormSq_le_absorbedComponents_base_mul_inv_one_sub_of_bddAbove {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s η : ℝ) (u g : Vec d → Vec d) (v : TriadicCube d → Vec d → Vec d) (hs : 0 < s) (hlocal : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage R 1 fun (S : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo S s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2) + weakFluxRHSAbsorbedLocalError R a g u (v R) s η) (m : ℕ) {Bcoeff Bu Bv Bforce : ℝ} (hBdd : BddAbove (Set.range fun (n : ℕ) => weakFluxRHSScaledAveragedSeminormSq Q a s u n)) (hBcoeff_nonneg : 0 ≤ Bcoeff) (hBu_nonneg : 0 ≤ Bu) (hBv_nonneg : 0 ≤ Bv) (hBforce_nonneg : 0 ≤ Bforce) (hcoeff : ∀ (k : ℕ), coarsePoincareRHSDepthWeight s (m + k) * weakFluxRHSLocalCoefficientEnergyErrorAverage Q a u s (m + k) ≤ Bcoeff) (hu : ∀ (k : ℕ), coarsePoincareRHSDepthWeight s (m + k) * weakFluxRHSLocalUSeminormErrorAverage Q u s η (m + k) ≤ Bu) (hv : ∀ (k : ℕ), coarsePoincareRHSDepthWeight s (m + k) * weakFluxRHSLocalHarmonicSeminormErrorAverage Q v s η (m + k) ≤ Bv) (hforce : ∀ (k : ℕ), coarsePoincareRHSDepthWeight s (m + k) * weakFluxRHSLocalForceErrorAverage Q a g s η (m + k) ≤ Bforce) :
weakFluxRHSScaledAveragedSeminormSq Q a s u m ≤ (Bcoeff + Bu + Bv + Bforce) * (1 - Real.rpow 3 (-s))⁻¹

Scaled bounded-tail weak-flux iteration where the absorbed local error is controlled by separate averaged component bases.

source
theorem HCPolySupport.localizedFluxDefect_negativeBesovAverage_le_sqrt_absorbedError {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s η : ℝ) (u g : Vec d → Vec d) (v : TriadicCube d → Vec d → Vec d) (hs : 0 < s) (hlocal : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage R 1 fun (S : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo S s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2) + weakFluxRHSAbsorbedLocalError R a g u (v R) s η) (m : ℕ) {B : ℝ} (hBdd : BddAbove (Set.range fun (n : ℕ) => weakFluxRHSScaledAveragedSeminormSq Q a s u n)) (hB_nonneg : 0 ≤ B) (hterm : ∀ (k : ℕ), (coarsePoincareRHSDepthWeight s (m + k) * descendantsAverage Q (m + k) fun (R : TriadicCube d) => weakFluxRHSAbsorbedLocalError R a g u (v R) s η) ≤ B) :
localizedFluxDefectNegativeBesovAverageTwo Q s (fun (x : Vec d) => matVecMul (a x) (u x)) m ≤ √((coarsePoincareRHSDepthWeight s m)⁻¹ * (B * (1 - Real.rpow 3 (-s))⁻¹))

Localized flux-defect form of the scaled bounded-tail weak-flux iteration with the explicit absorbed local-error envelope.

source
theorem HCPolySupport.localizedFluxDefect_negativeBesovAverage_le_sqrt_absorbedComponents {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s η : ℝ) (u g : Vec d → Vec d) (v : TriadicCube d → Vec d → Vec d) (hs : 0 < s) (hlocal : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage R 1 fun (S : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo S s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2) + weakFluxRHSAbsorbedLocalError R a g u (v R) s η) (m : ℕ) {Bcoeff Bu Bv Bforce : ℝ} (hBdd : BddAbove (Set.range fun (n : ℕ) => weakFluxRHSScaledAveragedSeminormSq Q a s u n)) (hBcoeff_nonneg : 0 ≤ Bcoeff) (hBu_nonneg : 0 ≤ Bu) (hBv_nonneg : 0 ≤ Bv) (hBforce_nonneg : 0 ≤ Bforce) (hcoeff : ∀ (k : ℕ), coarsePoincareRHSDepthWeight s (m + k) * weakFluxRHSLocalCoefficientEnergyErrorAverage Q a u s (m + k) ≤ Bcoeff) (hu : ∀ (k : ℕ), coarsePoincareRHSDepthWeight s (m + k) * weakFluxRHSLocalUSeminormErrorAverage Q u s η (m + k) ≤ Bu) (hv : ∀ (k : ℕ), coarsePoincareRHSDepthWeight s (m + k) * weakFluxRHSLocalHarmonicSeminormErrorAverage Q v s η (m + k) ≤ Bv) (hforce : ∀ (k : ℕ), coarsePoincareRHSDepthWeight s (m + k) * weakFluxRHSLocalForceErrorAverage Q a g s η (m + k) ≤ Bforce) :
localizedFluxDefectNegativeBesovAverageTwo Q s (fun (x : Vec d) => matVecMul (a x) (u x)) m ≤ √((coarsePoincareRHSDepthWeight s m)⁻¹ * ((Bcoeff + Bu + Bv + Bforce) * (1 - Real.rpow 3 (-s))⁻¹))

Localized flux-defect form with separate absorbed component bases.

source
theorem HCPolySupport.weakFluxRHSScaledAveragedSeminormSq_le_absorbedLocalizedBases_mul_inv_one_sub_of_bddAbove {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s η : ℝ) (u g : Vec d → Vec d) (v : TriadicCube d → Vec d → Vec d) {lam Lam : ℝ} (hs : 0 < s) (hη : 0 < η) (hlocal : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage R 1 fun (S : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo S s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2) + weakFluxRHSAbsorbedLocalError R a g u (v R) s η) (m : ℕ) {BU BV : ℝ} (hBdd : BddAbove (Set.range fun (n : ℕ) => weakFluxRHSScaledAveragedSeminormSq Q a s u n)) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : OpenCubeDescendantDeterministicCoarseData Q a) (hsum_half : Summable fun (l : ℕ) => geometricWeight (s / 2) 2 l * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑l) a).rpow 1) (havg_parent_nonneg : 0 ≤ cubeAverage Q (coefficientEnergyDensity a u)) (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)) (hBU_nonneg : 0 ≤ BU) (hBV_nonneg : 0 ≤ BV) (hu : ∀ (k : ℕ), coarsePoincareRHSSn Q s u (m + k) ≤ BU) (hv : ∀ (k : ℕ), weakFluxRHSHarmonicRemainderScaledAveragedSeminormSq Q s v (m + k) ≤ BV) :
weakFluxRHSScaledAveragedSeminormSq Q a s u m ≤ (weakFluxRHSWeightedCoefficientEnergyBase Q a u s + η * BU + η * BV + weakFluxRHSWeightedGlobalForceBase Q a g s η m) * (1 - Real.rpow 3 (-s))⁻¹

Scaled bounded-tail weak-flux iteration with all localized absorbed component bases supplied by the coefficient, u, harmonic-remainder, and forcing base estimates.

source
theorem HCPolySupport.negativeBesovFluxAverage_matrixVectorMultiply_le_sqrt {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s η : ℝ) (u g : Vec d → Vec d) (v : TriadicCube d → Vec d → Vec d) {lam Lam : ℝ} (hs : 0 < s) (hη : 0 < η) (hlocal : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage R 1 fun (S : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo S s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2) + weakFluxRHSAbsorbedLocalError R a g u (v R) s η) (m : ℕ) {BU BV : ℝ} (hBdd : BddAbove (Set.range fun (n : ℕ) => weakFluxRHSScaledAveragedSeminormSq Q a s u n)) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : OpenCubeDescendantDeterministicCoarseData Q a) (hsum_half : Summable fun (l : ℕ) => geometricWeight (s / 2) 2 l * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑l) a).rpow 1) (havg_parent_nonneg : 0 ≤ cubeAverage Q (coefficientEnergyDensity a u)) (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)) (hBU_nonneg : 0 ≤ BU) (hBV_nonneg : 0 ≤ BV) (hu : ∀ (k : ℕ), coarsePoincareRHSSn Q s u (m + k) ≤ BU) (hv : ∀ (k : ℕ), weakFluxRHSHarmonicRemainderScaledAveragedSeminormSq Q s v (m + k) ≤ BV) :
localizedFluxDefectNegativeBesovAverageTwo Q s (fun (x : Vec d) => matVecMul (a x) (u x)) m ≤ √((coarsePoincareRHSDepthWeight s m)⁻¹ * ((weakFluxRHSWeightedCoefficientEnergyBase Q a u s + η * BU + η * BV + weakFluxRHSWeightedGlobalForceBase Q a g s η m) * (1 - Real.rpow 3 (-s))⁻¹))

Localized flux-defect form with all localized absorbed component bases supplied by the coefficient, u, harmonic-remainder, and forcing base estimates.