Grouped mean-zero assembly: the centered ten-term family

Only the sum twistie4 + twistie5 + normie3 of the ten §5.1 terms is mean zero (the grouped mean-zero decomposition (12)/(13)); the three are not individually so. The centered family section5CenteredTerm replaces the slots 3 (twistie4), 4 (twistie5) and 8 (normie3) of section5Term by their centerCell. On t ∈ (0,1) it has the same pointwise sum as the original family (sum_section5CenteredTerm_eq), and the triangle inequality in the exact HDot⁻¹ time norm holds for any finite family of jointly continuous terms (timeHMinusOneNorm_sum_range_le).

Triangle inequality for a finite jointly continuous family

theorem AVenhance.Infra.Section5.Integration.timeHMinusOneNorm_sum_range_le {u : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {n : ℕ} (hn : 1 ≤ n) (hu : ∀ i < n, ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => u i p.1 p.2) (Set.Ioo 0 1 ×ˢ Set.univ)) : (timeHMinusOneNorm fun (t : ℝ) (x : Homogenization.Vec 2) => ∑ i ∈ Finset.range n, u i t x) ≤ ∑ i ∈ Finset.range n, timeHMinusOneNorm (u i)

A finite sum of jointly continuous terms obeys the triangle inequality in the HDot⁻¹ time norm (L² regularity and time measurability of every partial sum come from joint continuity).

The centered family

noncomputable def AVenhance.Infra.Section5.Integration.section5CenteredTerm {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (d e : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (i : ℕ) : ℝ → Homogenization.Vec 2 → ℝ

The ten §5.1 terms with the three grouped slots 3 (twistie4), 4 (twistie5) and 8 (normie3) replaced by their unit-cube centering.

Equations

• One or more equations did not get rendered due to their size.
• AVenhance.Infra.Section5.Integration.section5CenteredTerm I hΦ m κm T d e i = AVenhance.Infra.Section5.section5Term I hΦ m κm T d e i

theorem AVenhance.Infra.Section5.Integration.sum_section5CenteredTerm_eq {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (d e : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (t : ℝ) (hL2 : ∀ i < 10, Homogenization.MemL2On unitCube (section5Term I hΦ m κm T d e i t)) (hgroup : Homogenization.MeanZeroOn unitCube fun (x : Homogenization.Vec 2) => twistie4 I hΦ m κm T t x + twistie5 I hΦ m κm T t x + normie3 I hΦ m κm T t x) (x : Homogenization.Vec 2) : ∑ i ∈ Finset.range 10, section5CenteredTerm I hΦ m κm T d e i t x = ∑ i ∈ Finset.range 10, section5Term I hΦ m κm T d e i t x

On a time where the slots are L² and the group twistie4 + twistie5 + normie3 has mean zero, the centered ten-term sum equals the original ten-term sum.