Fixed-time spatial regularity and zero-mean gradient of the summed corrector.

noncomputable def AVenhance.Infra.Section3.ChiMRegularity.chiMIndexFinset {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (t : ℝ) : Finset ℤ

Finite set of corrector cutoff indices active at a specified time.

Equations

• AVenhance.Infra.Section3.ChiMRegularity.chiMIndexFinset I hm t = ⋯.toFinset

theorem AVenhance.Infra.Section3.chiM_eq_finset_sum {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ t : ℝ) (x : Homogenization.Vec 2) : I.chiM κ m t x = ∑ k ∈ ChiMRegularity.chiMIndexFinset I hm t, I.xiMK m k t • I.chiMK κ m k t x

At fixed time the corrector series is an ordinary finite sum.

theorem AVenhance.Infra.Section3.chiM_component_contDiff {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ t : ℝ) (i : Fin 2) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => I.chiM κ m t x i

Each fixed-time coordinate of the summed corrector is smooth in space.

theorem AVenhance.Infra.Section3.ChiMRegularity.cos_integer_frequency_periodic (ε : ℝ) {N : ℕ} (hεinv : ε⁻¹ = ↑N) (x : ℝ) (n : ℤ) : Real.cos (2 * Real.pi * (x + ↑n) / ε) = Real.cos (2 * Real.pi * x / ε)

theorem AVenhance.Infra.Section3.ChiMRegularity.uShear_z2_periodic {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (k : ℤ) : IsZ2Periodic fun (x : Homogenization.Vec 2) => uShear β I.Λ m k x

theorem AVenhance.Infra.Section3.chiM_component_z2_periodic {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ t : ℝ) (i : Fin 2) : IsZ2Periodic fun (x : Homogenization.Vec 2) => I.chiM κ m t x i

Each fixed-time coordinate of the summed corrector is integer-periodic.

def AVenhance.Infra.Section3.ChiMRegularity.closedUnitSquare : Set (Homogenization.Vec 2)

Closed spatial unit cell used for compactness and periodic integration.

Equations

• AVenhance.Infra.Section3.ChiMRegularity.closedUnitSquare = Set.univ.pi fun (x : Fin 2) => Set.Icc 0 1

theorem AVenhance.Infra.Section3.ChiMRegularity.real_integrableOn_unitCell {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) : MeasureTheory.IntegrableOn f (Torus.unitCell 2) MeasureTheory.volume

theorem AVenhance.Infra.Section3.spaceAvg_chiM_component_deriv_eq_zero {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ t : ℝ) (i j : Fin 2) : (spaceAvg fun (x : Homogenization.Vec 2) => spaceGrad (fun (y : Homogenization.Vec 2) => I.chiM κ m t y i) x j) = 0

Every coordinate derivative of the fixed-time summed corrector has zero mean over the spatial torus.