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

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

First assembly tools for the public quenched homogenization theorem

This file begins Phase 4 of the public theorem plan. The first result upgrades the parent-cube finite-q homogenization-error estimate to the Ch3 depth-localized quantity coarseGrainingHomogenizationErrorAtDepth.

def HCPolySupport.Book.Ch05.Section57.scalarConstantCoeffMatrix {d : ℕ} (σ : ℝ) (hσ : 0 < σ) : Ch03.ConstantCoeffMatrix d

The scalar constant-coefficient package used by the Ch3 deterministic homogenization theorem.

Equations

• HCPolySupport.Book.Ch05.Section57.scalarConstantCoeffMatrix σ hσ = { matrix := HCPolySupport.scalarMatrix σ, isSymm := ⋯, lam := σ, Lam := σ, lam_pos := hσ, lam_le_Lam := ⋯, elliptic := ⋯ }

theorem HCPolySupport.Book.Ch05.Section57.scalarConstantCoeffMatrix_matrix {d : ℕ} {σ : ℝ} (hσ : 0 < σ) : (scalarConstantCoeffMatrix σ hσ).matrix = scalarMatrix σ

theorem HCPolySupport.Book.Ch05.Section57.scalarConstantCoeffMatrix_isPositiveScalarMatrix {d : ℕ} {σ : ℝ} (hσ : 0 < σ) : IsPositiveScalarMatrix (scalarConstantCoeffMatrix σ hσ).matrix

theorem HCPolySupport.Book.Ch05.Section57.sqrt_rpow_neg_div_mono_of_le {A X Y α : ℝ} (hA : 0 < A) (hX : 0 < X) (hY : 0 < Y) (hXY : X ≤ Y) (hα : 0 < α) : √((A / X) ^ (-α)) ≤ √((A / Y) ^ (-α))

theorem HCPolySupport.Book.Ch05.Section57.isBigO_gammaSigma_max_two_expLogSq {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {η C₁ C₂ θ : ℝ} (hη : 0 < η) (hθ : 0 < θ) {X₁ X₂ : Ω → ℝ} (hX₁ : IndependentSums.IsBigO μ (IndependentSums.gammaSigma η) X₁ (Real.exp (C₁ * Real.log (2 + θ) ^ 2))) (hX₂ : IndependentSums.IsBigO μ (IndependentSums.gammaSigma η) X₂ (Real.exp (C₂ * Real.log (2 + θ) ^ 2))) : have C := 4 * max 0 (Real.log ((3 * Real.log 2) ^ η⁻¹)) + max C₁ C₂; IndependentSums.IsBigO μ (IndependentSums.gammaSigma η) (fun (ω : Ω) => max (X₁ ω) (X₂ ω)) (Real.exp (C * Real.log (2 + θ) ^ 2))

Combine two already-collapsed random scales without making the stochastic prefactor depend on the law.

theorem HCPolySupport.Book.Ch05.Section57.coarseGrainingHomogenizationErrorAtDepth_le_depthWeight_mul_parent {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : Ch02.TriadicCoeffFamily d) (a0 : Ch03.ConstantCoeffMatrix d) {s : ℝ} (hs : 0 < s) (j : ℕ) : Ch03.coarseGrainingHomogenizationErrorAtDepth Q a a0 s j ≤ Ch03.coarseGrainingDepthWeight s j * Ch02.HomogenizationErrorOnCube Q s Ch02.MultiscaleExponent.infinity (Ch02.MultiscaleExponent.finite 1) a a0.matrix

A depth-j Ch3 homogenization-error envelope is controlled by the parent cube's Ch2 q = 1 homogenization error with the expected geometric depth weight.

theorem HCPolySupport.Book.Ch05.Section57.exists_coarseGrainingHomogenizationErrorAtDepth_interpolated_expLogSq {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (α : ℝ), 0 < α ∧ ∀ {σ τ r : ℝ}, 0 < σ → max params.sUpper params.sLower < τ / 2 → α < τ / 2 → τ ≤ 1 → 0 ≤ r → 0 < r - τ / 2 → 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 : ℕ}, X aω ≤ 3 ^ m → have F := Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField aω ha; let σ0 := barSigmaLimit hP hStruct; have hσ0 := ⋯; have a0 := scalarConstantCoeffMatrix σ0 hσ0; have Cresp := √(4 * ↑(Fintype.card (BlockCoord d)) * ↑(Fintype.card (NormalizedProbeIndex d))); have Cneg := (Ch02.geometricDiscount (τ / 2) 1)⁻¹ * (2 * √(↑(Fintype.card (BlockCoord d)) ^ 2)); have A := max Cresp Cneg * Real.rpow 3 (τ / 2); have G := (Ch02.geometricDiscount r 1 * (Ch02.geometricDiscount (r - τ / 2) 1)⁻¹).rpow (1 / 1); Ch03.coarseGrainingHomogenizationErrorAtDepth (originCube d ↑m) F a0 r j ≤ Ch03.coarseGrainingDepthWeight r j * (G * A * √((3 ^ m / X aω) ^ (-α)))

Finite-sigma control of the Ch3 depth-localized homogenization-error quantity above the same collapsed minimal-scale envelope.

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch05.Section57.assemblyCoeffFamily {d : ℕ} (aω : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField aω) : Ch02.TriadicCoeffFamily d

The random coefficient family attached to an a.e. uniformly elliptic coefficient field.

Equations

• HCPolySupport.Book.Ch05.Section57.assemblyCoeffFamily aω ha = HCPolySupport.Book.Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField aω ha

@[reducible, inline]

abbrev HCPolySupport.Book.Ch05.Section57.assemblyOriginCube (d m : ℕ) : TriadicCube d

Origin cube at the natural-number generation used by the homogenization assembly.

Equations

• HCPolySupport.Book.Ch05.Section57.assemblyOriginCube d m = HCPolySupport.originCube d ↑m

def HCPolySupport.Book.Ch05.Section57.assemblyConstantCoeffMatrixOfScalar {d : ℕ} (σ0 : ℝ) (hσ0 : 0 < σ0) : Ch03.ConstantCoeffMatrix d

The scalar homogenized matrix used in the Ch3 comparison datum, with the background scalar passed explicitly. This is the sigma-agnostic Ch3 assembly surface; finite-sigma and endpoint hypotheses only have to supply the scalar and its positivity.

Equations

• HCPolySupport.Book.Ch05.Section57.assemblyConstantCoeffMatrixOfScalar σ0 hσ0 = HCPolySupport.Book.Ch05.Section57.scalarConstantCoeffMatrix σ0 hσ0

@[reducible, inline]

abbrev HCPolySupport.Book.Ch05.Section57.assemblyComparisonDatumOfScalar {d : ℕ} (σ0 : ℝ) (hσ0 : 0 < σ0) (aω : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField aω) (m : ℕ) (g : Vec d → Vec d) : Type

Coarse-graining comparison data on the origin cube for the supplied scalar homogenized matrix.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section57.assemblyConstantCoeffMatrix {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) : Ch03.ConstantCoeffMatrix d

Constant coefficient matrix built from the law's positive limiting scalar coefficient.

Equations

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

@[reducible, inline]

abbrev HCPolySupport.Book.Ch05.Section57.assemblyComparisonDatum {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) (aω : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField aω) (m : ℕ) (g : Vec d → Vec d) : Type

Coarse-graining comparison data 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.assemblyResponseConstant (d : ℕ) : ℝ

Response constant determined by the cardinalities of block coordinates and normalized probes.

Equations

• HCPolySupport.Book.Ch05.Section57.assemblyResponseConstant d = √(4 * ↑(Fintype.card (HCPolySupport.BlockCoord d)) * ↑(Fintype.card (HCPolySupport.Book.Ch05.Section57.NormalizedProbeIndex d)))

noncomputable def HCPolySupport.Book.Ch05.Section57.assemblyNegativeConstant (d : ℕ) (τ : ℝ) : ℝ

Negative-order constant combining the geometric discount with the block-coordinate cardinality.

Equations

• HCPolySupport.Book.Ch05.Section57.assemblyNegativeConstant d τ = (HCPolySupport.Book.Ch02.geometricDiscount (τ / 2) 1)⁻¹ * (2 * √(↑(Fintype.card (HCPolySupport.BlockCoord d)) ^ 2))

noncomputable def HCPolySupport.Book.Ch05.Section57.assemblyAmplitude (d : ℕ) (τ : ℝ) : ℝ

Maximum of the response and negative-order constants, scaled by 3 ^ (τ / 2).

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section57.assemblyMinimalScaleDecay {d : ℕ} (α : ℝ) (X : RegCoeffField d → ℝ) (aω : RegCoeffField d) (m : ℕ) : ℝ

Square-root minimal-scale decay at generation m and coefficient-dependent scale X aω.

Equations

• HCPolySupport.Book.Ch05.Section57.assemblyMinimalScaleDecay α X aω m = √((3 ^ m / X aω) ^ (-α))

noncomputable def HCPolySupport.Book.Ch05.Section57.assemblyErrorDiscount (τ r : ℝ) : ℝ

Geometric discount ratio used to transfer the weak-error estimate to exponent r.

Equations

• HCPolySupport.Book.Ch05.Section57.assemblyErrorDiscount τ r = (HCPolySupport.Book.Ch02.geometricDiscount r 1 * (HCPolySupport.Book.Ch02.geometricDiscount (r - τ / 2) 1)⁻¹).rpow (1 / 1)

noncomputable def HCPolySupport.Book.Ch05.Section57.assemblyEllipticityDiscount (τ r : ℝ) : ℝ

Square-root geometric discount ratio used in ellipticity estimates at exponent r / 2.

Equations

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

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

Weak-error envelope obtained from its discount, the assembly amplitude and the minimal-scale decay.

Equations

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

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

Ellipticity-error envelope obtained from its discount, the assembly amplitude and the minimal-scale decay.

Equations

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

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

Ellipticity bound combining the squared ellipticity-error envelope with the dimensional factor.

Equations

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

def HCPolySupport.Book.Ch05.Section57.assemblyControlledFactorsConclusionOfScalar {d : ℕ} (σ0 : ℝ) (hσ0 : 0 < σ0) (Ccg α τ s 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) : Prop

The controlled-factor conclusion used by the Phase 4 assembly theorem, with the scalar background passed explicitly.

Equations

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

def HCPolySupport.Book.Ch05.Section57.assemblyControlledFactorsConclusion {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) (Ccg α τ s 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) : Prop

Controlled-factor assembly conclusion specialized to the law's limiting scalar coefficient.

Equations

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

def HCPolySupport.Book.Ch05.Section57.assemblyControlledFactorsTwoExponentConclusionOfScalar {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) : Prop

Two-exponent controlled-factor conclusion for the repaired Ch3 coarse-graining estimate. The response quantities are still localized at exponent r, while the forcing is measured at the stronger exponent r₂.

Equations

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

def HCPolySupport.Book.Ch05.Section57.assemblyControlledFactorsTwoExponentConclusion {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) : Prop

Controlled-factor assembly conclusion with separate response and forcing exponents for the law's limiting scalar coefficient.

Equations

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

theorem HCPolySupport.Book.Ch05.Section57.exists_homogenizationComparison_controlledFactors_interpolated_expLogSq {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (Ccg : ℝ) (α : ℝ), 0 < Ccg ∧ 0 < α ∧ α < max params.sUpper params.sLower ∧ ∀ {σ τ s r : ℝ}, 0 < σ → max params.sUpper params.sLower < τ / 2 → α < τ / 2 → τ ≤ 1 → 0 < s → 0 < r → r < s / 2 → s < 1 → τ < 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 → assemblyControlledFactorsConclusion hP hStruct hΓ Ccg α τ s r X aω ha m j g w

Finite-sigma assembly of the Ch3 comparison theorem with the collapsed minimal-scale controls needed to bound every random coefficient in its RHS.

This is the internal Phase 4 handoff: one random scale X controls both the depth-localized q = 1 homogenization error and the q = 2 ellipticity factors appearing in the deterministic Ch3 theorem.

theorem HCPolySupport.Book.Ch05.Section57.exists_homogenizationComparison_controlledFactors_twoExponent_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 → assemblyControlledFactorsTwoExponentConclusion hP hStruct hΓ Ccg α τ s r r₂ X aω ha m j g w

Finite-sigma two-exponent assembly of the repaired Ch3 comparison theorem. The stochastic scale and local coefficient controls are inherited from the one-exponent controlled-factor package; only the Ch3 comparison conjunct is replaced by the scale-separated theorem.