Mean-zero identities for the Section 5 residual terms.

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularityMeans.meanZeroOn_vecDiv_of_contDiff_periodic {F : Homogenization.Vec 2 → Homogenization.Vec 2} (hF : ContDiff ℝ (↑⊤) F) (hper : IsZ2Periodic F) : Homogenization.MeanZeroOn unitCube fun (x : Homogenization.Vec 2) => vecDiv F x

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularityMeans.vecDiv_scalar_mul {q : Homogenization.Vec 2 → ℝ} {F : Homogenization.Vec 2 → Homogenization.Vec 2} {x : Homogenization.Vec 2} (hq : ContDiff ℝ (↑⊤) q) (hF : ContDiff ℝ (↑⊤) F) : vecDiv (fun (y : Homogenization.Vec 2) => q y • F y) x = Homogenization.vecDot (spaceGrad q x) (F x) + q x * vecDiv F x

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularityMeans.sigmaGrad_div_zero {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (x : Homogenization.Vec 2) : vecDiv (fun (y : Homogenization.Vec 2) => sigmaMat.mulVec (spaceGrad f y)) x = 0

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularityMeans.chiMK_div_zero {β : ℝ} (I : Ingredients β) (m : ℕ) (κ : ℝ) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) : vecDiv (fun (y : Homogenization.Vec 2) => I.chiMK κ m k t y) x = 0

noncomputable def AVenhance.Infra.Section5.Integration.BigBoundRegularityMeans.chiPushforwardFlux {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (k : ℤ) (t : ℝ) : Homogenization.Vec 2 → Homogenization.Vec 2

Corrector flux in flow coordinates used in the mean-value regularity estimates.

Equations

• AVenhance.Infra.Section5.Integration.BigBoundRegularityMeans.chiPushforwardFlux I hΦ m κ k t x = (I.flowGrad hΦ m (AVenhance.lIdx β I.Λ m k) t x).transpose.mulVec (I.chiTilde hΦ m κ k t x)

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularityMeans.chiTilde_isZ2Periodic {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (k : ℤ) (t : ℝ) : IsZ2Periodic (I.chiTilde hΦ m κ k t)

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularityMeans.chiPushforwardFlux_regular {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (k : ℤ) (t : ℝ) : ContDiff ℝ (↑⊤) (chiPushforwardFlux I hΦ m κ k t) ∧ IsZ2Periodic (chiPushforwardFlux I hΦ m κ k t) ∧ ∀ (x : Homogenization.Vec 2), vecDiv (chiPushforwardFlux I hΦ m κ k t) x = 0

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularityMeans.meanZeroOn_finite_weighted_divergence {ι : Type u_1} (U : Finset ι) (c : ι → ℝ) (F : ι → Homogenization.Vec 2 → Homogenization.Vec 2) (hFsm : ∀ i ∈ U, ContDiff ℝ (↑⊤) (F i)) (hFper : ∀ i ∈ U, IsZ2Periodic (F i)) : Homogenization.MeanZeroOn unitCube fun (x : Homogenization.Vec 2) => vecDiv (fun (y : Homogenization.Vec 2) => ∑ i ∈ U, c i • F i y) x

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularityMeans.meanZeroOn_weighted_grad_pairing {ι : Type u_1} (U : Finset ι) (c : ι → ℝ) (q : ι → Homogenization.Vec 2 → ℝ) (P : ι → Homogenization.Vec 2 → Homogenization.Vec 2) (hqsm : ∀ i ∈ U, ContDiff ℝ (↑⊤) (q i)) (hqper : ∀ i ∈ U, IsZ2Periodic (q i)) (hPsm : ∀ i ∈ U, ContDiff ℝ (↑⊤) (P i)) (hPper : ∀ i ∈ U, IsZ2Periodic (P i)) (hPdiv : ∀ i ∈ U, ∀ (x : Homogenization.Vec 2), vecDiv (P i) x = 0) : Homogenization.MeanZeroOn unitCube fun (x : Homogenization.Vec 2) => ∑ i ∈ U, c i * Homogenization.vecDot (spaceGrad (q i) x) (P i x)

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularityMeans.xFlowInv_right_inverse {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) (x : Homogenization.Vec 2) : I.xFlow hΦ m l t (I.xFlowInv hΦ m l t x) = x

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularityMeans.vecDot_matrixMulVec_transpose (A : Matrix (Fin 2) (Fin 2) ℝ) (u v : Homogenization.Vec 2) : Homogenization.vecDot u (A.mulVec v) = Homogenization.vecDot (A.transpose.mulVec u) v

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularityMeans.vecDot_comm (u v : Homogenization.Vec 2) : Homogenization.vecDot u v = Homogenization.vecDot v u

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularityMeans.G_pairing_pushforward {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (hT : ContDiff ℝ 1 (T t)) : Homogenization.vecDot (I.chiTilde hΦ m κ k t x) (G I hΦ m T (lIdx β I.Λ m k) t x) = Homogenization.vecDot (chiPushforwardFlux I hΦ m κ k t x) (spaceGrad (T t) x)

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularityMeans.vecDiv_contDiff_infty {F : Homogenization.Vec 2 → Homogenization.Vec 2} (hF : ContDiff ℝ (↑⊤) F) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => vecDiv F x

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularityMeans.vecDiv_isZ2Periodic {F : Homogenization.Vec 2 → Homogenization.Vec 2} (hF : ContDiff ℝ (↑⊤) F) (hper : IsZ2Periodic F) : IsZ2Periodic fun (x : Homogenization.Vec 2) => vecDiv F x

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularityMeans.flowGradK_contDiff_infty {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (k : ℤ) (t : ℝ) : ContDiff ℝ (↑⊤) (flowGradK I hΦ m k t)

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularityMeans.flowGradK_isZ2Periodic {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (k : ℤ) (t : ℝ) : IsZ2Periodic (flowGradK I hΦ m k t)

noncomputable def AVenhance.Infra.Section5.Integration.BigBoundRegularityMeans.chiMKTimeDerivative {β : ℝ} (I : Ingredients β) (m : ℕ) (κ : ℝ) (k : ℤ) (t : ℝ) : Homogenization.Vec 2 → Homogenization.Vec 2

Componentwise time derivative of the cell corrector for the mean-value estimates.

Equations

• AVenhance.Infra.Section5.Integration.BigBoundRegularityMeans.chiMKTimeDerivative I m κ k t y j = deriv (fun (s : ℝ) => I.chiMK κ m k s y j) t

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularityMeans.chiMKTimeDerivative_eq_shear {β : ℝ} (I : Ingredients β) (m : ℕ) (κ : ℝ) (k : ℤ) (t : ℝ) : chiMKTimeDerivative I m κ k t = fun (y : Homogenization.Vec 2) => -(I.zetaProd m k t - 4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2 * I.corrTime κ m k t) • uShear β I.Λ m k y

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularityMeans.chiMKTimeDerivative_regular {β : ℝ} (I : Ingredients β) (m : ℕ) (κ : ℝ) (k : ℤ) (t : ℝ) : ContDiff ℝ (↑⊤) (chiMKTimeDerivative I m κ k t) ∧ IsZ2Periodic (chiMKTimeDerivative I m κ k t) ∧ ∀ (x : Homogenization.Vec 2), vecDiv (chiMKTimeDerivative I m κ k t) x = 0

noncomputable def AVenhance.Infra.Section5.Integration.BigBoundRegularityMeans.chiTimePushforwardFlux {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (k : ℤ) (t : ℝ) : Homogenization.Vec 2 → Homogenization.Vec 2

Corrector time derivative in flow coordinates for the mean-value estimates.

Equations

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

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularityMeans.chiTimePushforwardFlux_regular {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (k : ℤ) (t : ℝ) : ContDiff ℝ (↑⊤) (chiTimePushforwardFlux I hΦ m κ k t) ∧ IsZ2Periodic (chiTimePushforwardFlux I hΦ m κ k t) ∧ ∀ (x : Homogenization.Vec 2), vecDiv (chiTimePushforwardFlux I hΦ m κ k t) x = 0

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularityMeans.timeDerivative_pairing_pushforward {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (hT : ContDiff ℝ 1 (T t)) : Homogenization.vecDot (chiMKTimeDerivative I m κ k t (I.xFlowInv hΦ m (lIdx β I.Λ m k) t x)) (G I hΦ m T (lIdx β I.Λ m k) t x) = Homogenization.vecDot (chiTimePushforwardFlux I hΦ m κ k t x) (spaceGrad (T t) x)

noncomputable def AVenhance.Infra.Section5.Integration.BigBoundRegularityMeans.oddPreimageFinset (S : Finset ℤ) : Finset { k : ℤ // Odd k }

Finite set of odd indices whose underlying integer belongs to a supplied finite set.

Equations

• AVenhance.Infra.Section5.Integration.BigBoundRegularityMeans.oddPreimageFinset S = ⋯.toFinset

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularityMeans.oddTsum_eq_preimage_sum (S : Finset ℤ) (F : { k : ℤ // Odd k } → ℝ) (hzero : ∀ (k : { k : ℤ // Odd k }), ↑k ∉ S → F k = 0) : ∑' (k : { k : ℤ // Odd k }), F k = ∑ k ∈ oddPreimageFinset S, F k

theorem AVenhance.Infra.Section5.Integration.cutoff1_meanZero_of_slice {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) {t : ℝ} (hTsm : ContDiff ℝ (↑⊤) (T t)) (hTper : IsZ2Periodic (T t)) : Homogenization.MeanZeroOn unitCube (cutoff1 I hΦ m κ T t)

The cutoff derivative term has zero mean because every mode pairs a pulled gradient with a divergence-free Piola push-forward of its shear.

theorem AVenhance.Infra.Section5.Integration.twistie1_meanZero_of_slice {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) {t : ℝ} (hTsm : ContDiff ℝ (↑⊤) (T t)) (hTper : IsZ2Periodic (T t)) : Homogenization.MeanZeroOn unitCube (twistie1 I hΦ m κ T t)

The transport term is a finite weighted divergence of Q P_k, where Q = div((K+s)∇T) and each Piola field P_k is divergence free.

theorem AVenhance.Infra.Section5.Integration.tiny_meanZero_of_slice {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κ : ℝ) (d e : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) {t : ℝ} (hdsm : ContDiff ℝ (↑⊤) (d t)) (hdper : IsZ2Periodic (d t)) (hesm : ContDiff ℝ (↑⊤) (e t)) (heper : IsZ2Periodic (e t)) : Homogenization.MeanZeroOn unitCube (tiny I hΦ m κ d e t)

The forcing term is the divergence of d+e+Σ ξ_k (div e)P_k; no separate mean condition on either source error is needed.