Time assembly for the twistie1 source contract #
Abstract measure-theoretic step: if the slices of the negative norm are dominated by
72 (P₁ √G(t) + P₂) with G(t) ≤ ∑_w c_w ‖V_w(t)‖² (t ∈ (0,1)) for fields V_w continuous on
[0,1] × ℝ², then the time negative norm is at most
72 √2 (P₁ √(∑_w c_w ‖V_w‖²_{L²((0,1)×𝕋²)}) + P₂).
theorem
AVenhance.Infra.Section5.Contracts.se_time_assembly
{H : ℝ → ENNReal}
{G : ℝ → ℝ}
(V : List (Fin 2) → ℝ → Homogenization.Vec 2 → Homogenization.Vec 2)
(cw : List (Fin 2) → ℝ)
{P₁ P₂ : ℝ}
(hP₁ : 0 ≤ P₁)
(hP₂ : 0 ≤ P₂)
(hcw : ∀ w ∈ scWords2, 0 ≤ cw w)
(hV :
∀ w ∈ scWords2,
∀ (i : Fin 2), ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => V w p.1 p.2 i) (Set.Icc 0 1 ×ˢ Set.univ))
(hG0 : ∀ t ∈ Set.Ioo 0 1, 0 ≤ G t)
(hH : ∀ t ∈ Set.Ioo 0 1, H t ≤ ENNReal.ofReal (72 * (P₁ * √(G t) + P₂)))
(hGle : ∀ t ∈ Set.Ioo 0 1, G t ≤ ∑ w ∈ scWords2, cw w * gradNormSq (V w t))
: