Coarse-graining support: Support.Book.Ch05.Theorems.Section57.HomogenizationAssemblyRHS

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

Deterministic RHS compression for the Section 5.7 assembly

This file takes the controlled factors supplied by HomogenizationAssembly.lean and substitutes them into the deterministic Ch3 coarse-graining RHS.

noncomputable def HCPolySupport.Book.Ch05.Section57.assemblyLowerEllipticityEnvelopeOfScalar {d : ℕ} (σ0 α τ r : ℝ) (X : RegCoeffField d → ℝ) (aω : RegCoeffField d) (m : ℕ) : ℝ

Square-root lower-ellipticity envelope scaled by the inverse of the supplied homogenized scalar.

Equations

• HCPolySupport.Book.Ch05.Section57.assemblyLowerEllipticityEnvelopeOfScalar σ0 α τ r X aω m = √(σ0⁻¹ * HCPolySupport.Book.Ch05.Section57.assemblyEllipticityEnvelope α τ r X aω m)

noncomputable def HCPolySupport.Book.Ch05.Section57.assemblyLowerEllipticityEnvelope {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (_hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) (α τ r : ℝ) (X : RegCoeffField d → ℝ) (aω : RegCoeffField d) (m : ℕ) : ℝ

Lower-ellipticity envelope specialized to the law's limiting scalar coefficient.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section57.assemblyCompressedTwoExponentRHSOfScalar {d : ℕ} (σ0 : ℝ) (hσ0 : 0 < σ0) (Ccg α τ s r r₂ : ℝ) (X : RegCoeffField d → ℝ) (aω : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField aω) (m j : ℕ) (g : Vec d → Vec d) (w : assemblyComparisonDatumOfScalar σ0 hσ0 aω ha m g) : ℝ

Scale-separated Ch3 RHS after substituting the collapsed minimal-scale bounds. The local coefficient/ellipticity factors are controlled at exponent r, while the forcing is measured at exponent r₂ and carries the inverse depth weight from the repaired Ch3 estimate.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section57.assemblyCompressedTwoExponentRHS {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) (Ccg α τ s r r₂ : ℝ) (X : RegCoeffField d → ℝ) (aω : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField aω) (m j : ℕ) (g : Vec d → Vec d) (w : assemblyComparisonDatum hP hStruct hΓ aω ha m g) : ℝ

Finite-sigma wrapper for the scale-separated compressed Ch3 RHS.

Equations

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

theorem HCPolySupport.Book.Ch05.Section57.poincareLowerEllipticityFactor_finite_two_eq_sqrt_inv {d : ℕ} (Q : TriadicCube d) (a : Ch02.TriadicCoeffFamily d) {s : ℝ} (_hs : 0 < s) : Ch03.poincareLowerEllipticityFactor Q a s (Ch02.MultiscaleExponent.finite 2) = √(Ch02.lambdaSq Q s (Ch02.MultiscaleExponent.finite 2) a)⁻¹

theorem HCPolySupport.Book.Ch05.Section57.poincareUpperEllipticityFactor_finite_two_eq_sqrt {d : ℕ} (Q : TriadicCube d) (a : Ch02.TriadicCoeffFamily d) {s : ℝ} (_hs : 0 < s) : Ch03.poincareUpperEllipticityFactor Q a s (Ch02.MultiscaleExponent.finite 2) = √(Ch02.LambdaSq Q s (Ch02.MultiscaleExponent.finite 2) a)

theorem HCPolySupport.Book.Ch05.Section57.lambdaSq_finite_two_rpow_neg_one_eq_inv {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : Ch02.TriadicCoeffFamily d) {s : ℝ} (hs : 0 < s) : (Ch02.lambdaSq Q s (Ch02.MultiscaleExponent.finite 2) a).rpow (-1) = (Ch02.lambdaSq Q s (Ch02.MultiscaleExponent.finite 2) a)⁻¹

theorem HCPolySupport.Book.Ch05.Section57.coarseGrainingHomogenizationErrorAtDepth_nonneg {d : ℕ} (Q : TriadicCube d) (a : Ch02.TriadicCoeffFamily d) (a0 : Ch03.ConstantCoeffMatrix d) {s : ℝ} (hs : 0 < s) (j : ℕ) : 0 ≤ Ch03.coarseGrainingHomogenizationErrorAtDepth Q a a0 s j

theorem HCPolySupport.Book.Ch05.Section57.assemblyLowerEllipticityFactor_le_ofScalar {d : ℕ} [NeZero d] {σ0 : ℝ} (hσ0 : 0 < σ0) {α τ r : ℝ} {X : RegCoeffField d → ℝ} {aω : RegCoeffField d} {m : ℕ} (ha : Ch04.AELocallyUniformlyEllipticField aω) (hr : 0 < r) (hlambda : (Ch02.lambdaSq (assemblyOriginCube d m) (r / 2) (Ch02.MultiscaleExponent.finite 2) (assemblyCoeffFamily aω ha))⁻¹ ≤ σ0⁻¹ * assemblyEllipticityEnvelope α τ r X aω m) : Ch03.poincareLowerEllipticityFactor (assemblyOriginCube d m) (assemblyCoeffFamily aω ha) (r / 2) (Ch02.MultiscaleExponent.finite 2) ≤ assemblyLowerEllipticityEnvelopeOfScalar σ0 α τ r X aω m

theorem HCPolySupport.Book.Ch05.Section57.assemblyLowerEllipticityFactor_le {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) {α τ r : ℝ} {X : RegCoeffField d → ℝ} {aω : RegCoeffField d} {m : ℕ} (ha : Ch04.AELocallyUniformlyEllipticField aω) (hr : 0 < r) (hlambda : (Ch02.lambdaSq (assemblyOriginCube d m) (r / 2) (Ch02.MultiscaleExponent.finite 2) (assemblyCoeffFamily aω ha))⁻¹ ≤ (barSigmaLimit hP hStruct)⁻¹ * assemblyEllipticityEnvelope α τ r X aω m) : Ch03.poincareLowerEllipticityFactor (assemblyOriginCube d m) (assemblyCoeffFamily aω ha) (r / 2) (Ch02.MultiscaleExponent.finite 2) ≤ assemblyLowerEllipticityEnvelope hP hStruct hΓ α τ r X aω m

theorem HCPolySupport.Book.Ch05.Section57.assemblyControlledFactors_lhs_le_compressedTwoExponentRHS_ofScalar {d : ℕ} [NeZero d] {σ0 : ℝ} (hσ0 : 0 < σ0) {Ccg α τ s r r₂ : ℝ} {X : RegCoeffField d → ℝ} {aω : RegCoeffField d} (ha : Ch04.AELocallyUniformlyEllipticField aω) {m j : ℕ} {g : Vec d → Vec d} (w : assemblyComparisonDatumOfScalar σ0 hσ0 aω ha m g) (hCcg : 0 < Ccg) (hs : 0 < s) (hr : 0 < r) (hrs : r < s / 2) (hs_lt_one : s < 1) (hg : Ch03.ForceBesovRegularity (assemblyOriginCube d m) r₂ g) (hctrl : assemblyControlledFactorsTwoExponentConclusionOfScalar σ0 hσ0 Ccg α τ s r r₂ X aω ha m j g w) : Ch03.homogenizationComparisonNegativeBesovLHS (assemblyOriginCube d m) (assemblyCoeffFamily aω ha) (assemblyConstantCoeffMatrixOfScalar σ0 hσ0) s w.u w.v ≤ assemblyCompressedTwoExponentRHSOfScalar σ0 hσ0 Ccg α τ s r r₂ X aω ha m j g w

Substitute the controlled factors into the repaired scale-separated Ch3 deterministic RHS.

theorem HCPolySupport.Book.Ch05.Section57.assemblyControlledFactors_lhs_le_compressedTwoExponentRHS {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) {Ccg α τ s r r₂ : ℝ} {X : RegCoeffField d → ℝ} {aω : RegCoeffField d} (ha : Ch04.AELocallyUniformlyEllipticField aω) {m j : ℕ} {g : Vec d → Vec d} (w : assemblyComparisonDatum hP hStruct hΓ aω ha m g) (hCcg : 0 < Ccg) (hs : 0 < s) (hr : 0 < r) (hrs : r < s / 2) (hs_lt_one : s < 1) (hg : Ch03.ForceBesovRegularity (assemblyOriginCube d m) r₂ g) (hctrl : assemblyControlledFactorsTwoExponentConclusion hP hStruct hΓ Ccg α τ s r r₂ X aω ha m j g w) : Ch03.homogenizationComparisonNegativeBesovLHS (assemblyOriginCube d m) (assemblyCoeffFamily aω ha) (assemblyConstantCoeffMatrix hP hStruct hΓ) s w.u w.v ≤ assemblyCompressedTwoExponentRHS hP hStruct hΓ Ccg α τ s r r₂ X aω ha m j g w

theorem HCPolySupport.Book.Ch05.Section57.ae_homogenizationComparison_compressedTwoExponentRHSOfScalar_of_ae_controlledFactors {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} {σ0 : ℝ} (hσ0 : 0 < σ0) {Ccg α τ s r r₂ : ℝ} {X : RegCoeffField d → ℝ} (hCcg : 0 < Ccg) (hs : 0 < s) (hr : 0 < r) (hrs : r < s / 2) (hs_lt_one : s < 1) (hctrl : ∀ᵐ (aω : RegCoeffField d) ∂P, ∀ (ha : Ch04.AELocallyUniformlyEllipticField aω) {m j : ℕ} {g : Vec d → Vec d} (w : assemblyComparisonDatumOfScalar σ0 hσ0 aω ha m g), X aω ≤ 3 ^ m → Ch03.ForceBesovRegularity (assemblyOriginCube d m) r₂ g → assemblyControlledFactorsTwoExponentConclusionOfScalar σ0 hσ0 Ccg α τ s r r₂ X aω ha m j g w) : ∀ᵐ (aω : RegCoeffField d) ∂P, ∀ (ha : Ch04.AELocallyUniformlyEllipticField aω) {m j : ℕ} {g : Vec d → Vec d} (w : assemblyComparisonDatumOfScalar σ0 hσ0 aω ha m g), X aω ≤ 3 ^ m → Ch03.ForceBesovRegularity (assemblyOriginCube d m) r₂ g → Ch03.homogenizationComparisonNegativeBesovLHS (assemblyOriginCube d m) (assemblyCoeffFamily aω ha) (assemblyConstantCoeffMatrixOfScalar σ0 hσ0) s w.u w.v ≤ assemblyCompressedTwoExponentRHSOfScalar σ0 hσ0 Ccg α τ s r r₂ X aω ha m j g w

Sigma-agnostic a.e. handoff for the repaired two-exponent Ch3 assembly.

theorem HCPolySupport.Book.Ch05.Section57.exists_homogenizationComparison_compressedTwoExponentRHS_interpolated_expLogSq {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Ccg : ℝ) (α : ℝ), 0 < Ccg ∧ 0 < α ∧ α < max params.sUpper params.sLower ∧ ∀ {σ τ s r r₂ : ℝ}, 0 < σ → max params.sUpper params.sLower < τ / 2 → α < τ / 2 → τ ≤ 1 → 0 < s → 0 < r → r < s / 2 → s < 1 → τ < r → r ≤ r₂ → have ηJ := finiteQuenchedTailExponent d σ τ; have ηU := finiteQuenchedTailExponent d σ (τ / 2); have η := min ηJ ηU; ∃ (Cscale : ℝ), 0 < Cscale ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct), hΓ.sigma = σ → hΓ.params = params → ∃ (X : RegCoeffField d → ℝ), IndependentSums.IsBigO P (IndependentSums.gammaSigma η) X (Real.exp (Cscale * Real.log (2 + hΓ.thetaHat) ^ 2)) ∧ (∀ (aω : RegCoeffField d), 1 ≤ X aω) ∧ ∀ᵐ (aω : RegCoeffField d) ∂P, ∀ (ha : Ch04.AELocallyUniformlyEllipticField aω) {m j : ℕ} {g : Vec d → Vec d} (w : assemblyComparisonDatum hP hStruct hΓ aω ha m g), X aω ≤ 3 ^ m → Ch03.ForceBesovRegularity (assemblyOriginCube d m) r₂ g → Ch03.homogenizationComparisonNegativeBesovLHS (assemblyOriginCube d m) (assemblyCoeffFamily aω ha) (assemblyConstantCoeffMatrix hP hStruct hΓ) s w.u w.v ≤ assemblyCompressedTwoExponentRHS hP hStruct hΓ Ccg α τ s r r₂ X aω ha m j g w

Finite-sigma homogenization comparison above one collapsed minimal scale, using the repaired scale-separated forcing exponent.