TermContinuousContract

Each of the ten §5.1 terms of the actual ansatz is jointly continuous on the open half space (TermContinuityDiv: the divergence-form terms; TermContinuityPointwise: the others), hence on (0,1) × ℝ².

theorem AVenhance.Infra.Section5.Contracts.termContinuous_contract (β C₀ : ℝ) : ∃ (C₁ : ℝ), Integration.OnA7Instances β C₀ C₁ fun (I : Ingredients β) (_Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I _Φ) (κ : ℝ) (M : ℕ) (_R : ℝ) (_θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (_θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) => Integration.TermContinuousContract I hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) T

TermContinuousContract (big-bound estimate term_continuous, also consumed by step-down part (ii)).