Structural coarse-coefficient interface for

The polynomial family is linear in K and κ and quadratic in F. Its two scalar coefficients are bounded by one. Both the left-Jacobian coefficient and its Infra candidate belong to this family; no analytic estimate is assumed.

@[reducible, inline]

abbrev AVenhance.Infra.Section4.CoarseMatrix : Type

Real two-by-two matrices used for the coarse effective coefficients.

Equations

• AVenhance.Infra.Section4.CoarseMatrix = Matrix (Fin 2) (Fin 2) ℝ

def AVenhance.Infra.Section4.coarseCoeffPolynomial (a b κ : ℝ) (K F : CoarseMatrix) : CoarseMatrix

Polynomial combining the coarse matrix, flow matrix, diffusivity, and cutoff weights.

Equations

• AVenhance.Infra.Section4.coarseCoeffPolynomial a b κ K F = a • (K * (F - 1)) + b • ((Matrix.transpose F - 1) * (K - κ • 1) * F)

noncomputable def AVenhance.Infra.Section4.coarseCoeffWindow {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ a b t : ℝ) (x : Homogenization.Vec 2) : CoarseMatrix

The split form is meaningful even at m = 0, where no cutoff partition hypothesis is available. At positive m it is the single polynomial window sum.

Equations

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

structure AVenhance.Infra.Section4.CoarseCoeffForm {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (s : ℝ → Homogenization.Vec 2 → CoarseMatrix) : Prop

A structural polynomial description, not an assumption of regularity or bounds.

• window_form : ∃ (a : ℝ) (b : ℝ), |a| ≤ 1 ∧ |b| ≤ 1 ∧ ∀ (t : ℝ) (x : Homogenization.Vec 2), s t x = coarseCoeffWindow I hΦ m κ a b t x

theorem AVenhance.Infra.Section4.sMat_eq_coarseCoeffWindow {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ t : ℝ) (x : Homogenization.Vec 2) : I.sMat hΦ m κ t x = coarseCoeffWindow I hΦ m κ 1 1 t x

coefficient as the quadratic structural window.

theorem AVenhance.Infra.Section4.sMat_coarseCoeffForm {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) : CoarseCoeffForm I hΦ m κ (I.sMat hΦ m κ)

sMat instance of the common interface.