Slice regularity of the tiny pieces

For the actual iterates and t > 0: the source error d_m, the last-iterate error e_{m-1} and the nondivergence part of tiny are continuous; d + e is C^∞ and ℤ²-periodic; the mean of the nondivergence part follows from the mean of tiny. Also a measurability helper for slice energies of fields jointly continuous on (0,1) × ℝ².

theorem AVenhance.Infra.Section5.Contracts.sc_slice_contDiff {F : ℝ → Homogenization.Vec 2 → ℝ} (hF : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => F p.1 p.2) tcU) {t : ℝ} (ht : 0 < t) : ContDiff ℝ (↑⊤) (F t)

A jointly C^∞ field on the open half space has C^∞ slices.

theorem AVenhance.Infra.Section5.Contracts.sc_integral_vecDiv_eq_zero {F : Homogenization.Vec 2 → Homogenization.Vec 2} (hF : ContDiff ℝ (↑⊤) F) (hp : IsZ2Periodic F) : ∫ (x : Homogenization.Vec 2) in unitCube, vecDiv F x = 0

The mean of the divergence of a smooth periodic field over the unit cube vanishes.

Measurability of slice energies

theorem AVenhance.Infra.Section5.Contracts.TermSourcesTinyRegular.sc_unitCube_ae_eq_closed : unitCube =ᵐ[MeasureTheory.volume] Set.univ.pi fun (x : Fin 2) => Set.Icc 0 1

theorem AVenhance.Infra.Section5.Contracts.sc_continuousOn_cubeIntegral {h : ℝ → Homogenization.Vec 2 → ℝ} (hh : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => h p.1 p.2) (Set.Ioo 0 1 ×ˢ Set.univ)) : ContinuousOn (fun (t : ℝ) => ∫ (x : Homogenization.Vec 2) in unitCube, h t x) (Set.Ioo 0 1)

Cube integrals of fields continuous on (0,1) × ℝ² are continuous in t ∈ (0,1).

theorem AVenhance.Infra.Section5.Contracts.sc_aemeasurable_cubeIntegral {h : ℝ → Homogenization.Vec 2 → ℝ} (hh : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => h p.1 p.2) (Set.Ioo 0 1 ×ˢ Set.univ)) : AEMeasurable (fun (t : ℝ) => ∫ (x : Homogenization.Vec 2) in unitCube, h t x) (MeasureTheory.volume.restrict (Set.Ioo 0 1))

theorem AVenhance.Infra.Section5.Contracts.sc_aemeasurable_gradNormSq {F : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hF : ∀ (i : Fin 2), ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => F p.1 p.2 i) (Set.Ioo 0 1 ×ˢ Set.univ)) : AEMeasurable (fun (t : ℝ) => ENNReal.ofReal (gradNormSq (F t))) (MeasureTheory.volume.restrict (Set.Ioo 0 1))

theorem AVenhance.Infra.Section5.Contracts.sc_d_continuousOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} (hκm : 0 < κm) {θ₀ : 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) (i : Fin 2) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => sourceErrorD I hΦ m κm (T (Nstar β)) p.1 p.2 i) tcU

(1) joint continuity of d_m on the open half space.

theorem AVenhance.Infra.Section5.Contracts.sc_e_continuousOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} (hκm : 0 < κm) {θ₀ : 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) (i : Fin 2) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => iterateError I hΦ m κm κprev T p.1 p.2 i) tcU

(2) joint continuity of e_{m-1} on the open half space.

theorem AVenhance.Infra.Section5.Contracts.sc_de_contDiff {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} (hκm : 0 < κm) {θ₀ : 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 ℝ ↑⊤ fun (x : Homogenization.Vec 2) => sourceErrorD I hΦ m κm (T (Nstar β)) t x + iterateError I hΦ m κm κprev T t x

(3) d + e is C^∞ on every positive-time slice.

theorem AVenhance.Infra.Section5.Contracts.sc_de_periodic {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {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 fun (x : Homogenization.Vec 2) => sourceErrorD I hΦ m κm (T (Nstar β)) t x + iterateError I hΦ m κm κprev T t x

The divergence-form field d_t + e_t is ℤ²-periodic for t > 0.

theorem AVenhance.Infra.Section5.Contracts.sc_tiny_slice_continuous {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} (hκm : 0 < κm) {θ₀ : 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) : Continuous (tiny I hΦ m κm (sourceErrorD I hΦ m κm (T (Nstar β))) (iterateError I hΦ m κm κprev T) t)

(5) tiny is continuous on every positive-time slice.

theorem AVenhance.Infra.Section5.Contracts.sc_vecDiv_de_continuous {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} (hκm : 0 < κm) {θ₀ : 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) : Continuous fun (x : Homogenization.Vec 2) => vecDiv (fun (y : Homogenization.Vec 2) => sourceErrorD I hΦ m κm (T (Nstar β)) t y + iterateError I hΦ m κm κprev T t y) x

The divergence of the smooth field d_t + e_t is continuous.

theorem AVenhance.Infra.Section5.Contracts.sc_nd_continuous {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} (hκm : 0 < κm) {θ₀ : 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) : Continuous (tinyNondivergencePart I hΦ m κm (iterateError I hΦ m κm κprev T) t)

(6) The nondivergence part of tiny is continuous on positive-time slices.

theorem AVenhance.Infra.Section5.Contracts.sc_nd_meanZero {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} (hκm : 0 < κm) {θ₀ : 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) (hmean : Homogenization.MeanZeroOn unitCube (tiny I hΦ m κm (sourceErrorD I hΦ m κm (T (Nstar β))) (iterateError I hΦ m κm κprev T) t)) : Homogenization.MeanZeroOn unitCube (tinyNondivergencePart I hΦ m κm (iterateError I hΦ m κm κprev T) t)

(7) mean of tiny zero gives mean of its nondivergence part zero.