Regularity fields for one big-bound estimate instance, excluding the scalar mean fields.

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularity.lmn_contDiff_top_any {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (n : ℕ) : ContDiff ℝ (↑⊤) (I.LMN κ m n)

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularity.amnr_seedMultiplier_contDiff_any {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (n N : ℕ) (j k i p : Fin 2) : ContDiff ℝ (↑N) (Section4.amnrSeedMultiplier I hΦ m κ n j k i p)

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularity.amnr_actual_contDiffOn_any {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (n r ord : ℕ) (i j k : Fin 2) : ContDiffOn ℝ (↑ord) (fun (z : Section4.AmnrSpace) => I.Amnr hΦ m κm n (T (Nstar β)) r z.1 z.2 i j k) (Set.Ioi 0 ×ˢ Set.univ)

The AMNR recursion has every finite joint order for an actual terminal iterate. The source-order cap is needed for estimates, not for this qualitative regularity statement.

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularity.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.amnr_slice_contDiff_infty {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (n r : ℕ) (i j k : Fin 2) {t : ℝ} (ht : 0 < t) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => I.Amnr hΦ m κm n (T (Nstar β)) r t x i j k

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularity.hm_slice_contDiff_infty {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) {t : ℝ} (ht : 0 < t) : ContDiff ℝ (↑⊤) (I.Hm hΦ m κm (T (Nstar β)) t)

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularity.amnr_time_differentiable_at {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (n r : ℕ) (i j k : Fin 2) {t : ℝ} (ht : 0 < t) (x : Homogenization.Vec 2) : DifferentiableAt ℝ (fun (s : ℝ) => I.Amnr hΦ m κm n (T (Nstar β)) r s x i j k) t

theorem AVenhance.Infra.Section5.Integration.amnr_periodic_of_iterates {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (r : ℕ) (t : ℝ) : 0 < t → ∀ (n : ℕ) (z : Fin 2 → ℤ) (x : Homogenization.Vec 2) (i j k : Fin 2), I.Amnr hΦ m κm n (T (Nstar β)) r t (x + latticeShift z) i j k = I.Amnr hΦ m κm n (T (Nstar β)) r t x i j k

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularity.hm_periodic_of_iterates {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) {t : ℝ} (ht : 0 < t) : IsZ2Periodic (I.Hm hΦ m κm (T (Nstar β)) t)

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularity.matrixMulVec_contDiff_infty {A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {v : Homogenization.Vec 2 → Homogenization.Vec 2} (hA : ContDiff ℝ (↑⊤) A) (hv : ContDiff ℝ (↑⊤) v) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => (A x).mulVec (v x)

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularity.psi_contDiff_infty {β : ℝ} (I : Ingredients β) (m : ℕ) (k : ℤ) : ContDiff ℝ (↑⊤) (psi β I.Λ m k)

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularity.psi_isZ2Periodic {β : ℝ} (I : Ingredients β) {m : ℕ} (k : ℤ) : IsZ2Periodic (psi β I.Λ m k)

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularity.psiTilde_contDiff_infty {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (t : ℝ) : ContDiff ℝ (↑⊤) (psiTilde I hΦ m t)

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularity.psiTilde_isZ2Periodic {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (_hm : 1 ≤ m) (t : ℝ) : IsZ2Periodic (psiTilde I hΦ m t)

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularity.diffusionMatrix_contDiff_infty {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm t : ℝ) : ContDiff ℝ (↑⊤) (diffusionMatrix I hΦ m κm t)

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularity.diffusionMatrix_isZ2Periodic {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κm t : ℝ) : IsZ2Periodic (diffusionMatrix I hΦ m κm t)

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

theorem AVenhance.Infra.Section5.Integration.G_contDiff_infty {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (l : ℤ) (hT : ContDiff ℝ (↑⊤) (T t)) : ContDiff ℝ (↑⊤) (G I hΦ m T l t)

theorem AVenhance.Infra.Section5.Integration.G_isZ2Periodic {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (l : ℤ) (hTper : IsZ2Periodic (T t)) (hTsm : ContDiff ℝ 1 (T t)) : IsZ2Periodic (G I hΦ m T l t)

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularity.gradG_contDiff_infty {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (l : ℤ) (hT : ContDiff ℝ (↑⊤) (T t)) : ContDiff ℝ (↑⊤) (gradG I hΦ m T l t)

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularity.gradG_isZ2Periodic {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (l : ℤ) (hGper : IsZ2Periodic (G I hΦ m T l t)) (hGsm : ContDiff ℝ (↑⊤) (G I hΦ m T l t)) : IsZ2Periodic (gradG I hΦ m T l t)

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularity.normie2Flux_smooth_of_iterates {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κm κprev : ℝ) {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) {t : ℝ} (ht : 0 < t) : ContDiff ℝ (↑⊤) (normie2Flux I hΦ m κm (T (Nstar β)) t)

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

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularity.chiGradG_contDiff_infty {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (k : ℤ) (t : ℝ) (hT : ContDiff ℝ (↑⊤) (T t)) : ContDiff ℝ (↑⊤) (chiGradG I hΦ m κm T k t)

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularity.chiGradG_isZ2Periodic {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (k : ℤ) (t : ℝ) (hχ : IsZ2Periodic (I.chiTilde hΦ m κm k t)) (hG : IsZ2Periodic (gradG I hΦ m T (lIdx β I.Λ m k) t)) : IsZ2Periodic (chiGradG I hΦ m κm T k t)

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularity.twistie3Flux_regular_of_iterates {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κm κprev : ℝ) {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) {t : ℝ} (ht : 0 < t) : ContDiff ℝ (↑⊤) (twistie3Flux I hΦ m κm (T (Nstar β)) t) ∧ IsZ2Periodic (twistie3Flux I hΦ m κm (T (Nstar β)) t)

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularity.normie1Flux_regular_of_iterates {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κm κprev : ℝ) {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) {t : ℝ} (ht : 0 < t) : ContDiff ℝ (↑⊤) (normie1Flux I hΦ m κm (T (Nstar β)) t) ∧ IsZ2Periodic (normie1Flux I hΦ m κm (T (Nstar β)) t)

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularity.normie2Flux_periodic_of_iterates {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κm κprev : ℝ) {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) {t : ℝ} (ht : 0 < t) : IsZ2Periodic (normie2Flux I hΦ m κm (T (Nstar β)) t)

theorem AVenhance.Infra.Section5.Integration.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

A smooth periodic divergence has zero integral on the unit cell. This is the u = 1 case of torus integration by parts.

theorem AVenhance.Infra.Section5.Integration.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

Product rule for the divergence of a scalar times a vector field.

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularity.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.BigBoundRegularity.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.BigBoundRegularity.chiPushforwardFlux {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (k : ℤ) (t : ℝ) : Homogenization.Vec 2 → Homogenization.Vec 2

Corrector flux transformed by the transposed flow Jacobian.

Equations

• AVenhance.Infra.Section5.Integration.BigBoundRegularity.chiPushforwardFlux I hΦ m κ k t x = (AVenhance.Infra.Section5.flowGradK I hΦ m k t x).transpose.mulVec (I.chiTilde hΦ m κ k t x)

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularity.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)

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularity.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.BigBoundRegularity.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

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularity.chiPushforwardFlux_div_zero {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) : vecDiv (chiPushforwardFlux I hΦ m κ k t) x = 0

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

Time derivative of each component of the cell corrector.

Equations

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

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularity.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.BigBoundRegularity.chiMKTimeDerivative_regular {β : ℝ} (I : Ingredients β) {m : ℕ} (_hm : 1 ≤ 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.chiTimePushforwardFlux {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (k : ℤ) (t : ℝ) : Homogenization.Vec 2 → Homogenization.Vec 2

Time derivative of the corrector transformed by the transposed flow Jacobian.

Equations

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

theorem AVenhance.Infra.Section5.Integration.chiTimePushforwardFlux_regular {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ 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.BigBoundRegularity.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.BigBoundRegularity.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.BigBoundRegularity.matrixMul_contDiff_infty {A B : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} (hA : ContDiff ℝ (↑⊤) A) (hB : ContDiff ℝ (↑⊤) B) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => A x * B x

theorem AVenhance.Infra.Section5.Integration.BigBoundRegularity.matrixMul_isZ2Periodic {A B : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} (hA : IsZ2Periodic A) (hB : IsZ2Periodic B) : IsZ2Periodic fun (x : Homogenization.Vec 2) => A x * B x

theorem AVenhance.Infra.Section5.Integration.correctorFlux_regular_of_mode {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κ : ℝ) (k : ℤ) (t : ℝ) (hk : Odd k) (hxi : I.xiMK m k t ≠ 0) : ContDiff ℝ (↑⊤) (correctorFlux I hΦ m κ k t) ∧ IsZ2Periodic (correctorFlux I hΦ m κ k t)

Each localized corrector flux is smooth and periodic on its active cutoff mode.