Source contracts of the divergence-form terms twistie3, normie1, normie2

Producers of Twistie3SourceContract, Normie1SourceContract and Normie2SourceContract in the abstract-amplitude form (B free), conditional on the input contracts at the same amplitude B:

• twistie3Source_contract from TGradientContract (source e.monster.est.7);
• normie1Source_contract from FirstOrderGradJetContract and TGradientContract (source e.monster.est.10);
• normie2Source_contract from HmGradientContract (source e.monster.est.11).

The proofs use the flux L² bound |flux|² ≤ ∑ c_j |V_j|² pointwise (TermSourcesFluxPointwise), the space-time transfer saTimeL2_le_of_pointwise and the scale package left_to_show_scales.

Continuity inputs

theorem AVenhance.Infra.Section5.Contracts.sa_gradT_cont {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) (i : Fin 2) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => spaceGrad (T p.1) p.2 i) (Set.Icc 0 1 ×ˢ Set.univ)

theorem AVenhance.Infra.Section5.Contracts.sa_hess_cont {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) (q i : Fin 2) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => spaceGrad (Section4.iterateSpatialWord [q] (T p.1)) p.2 i) (Set.Icc 0 1 ×ˢ Set.univ)

theorem AVenhance.Infra.Section5.Contracts.sa_Hm_grad_extends {β : ℝ} (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) : ∃ (Gh : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2), (∀ (i : Fin 2), ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => Gh p i) (Set.Ici 0 ×ˢ Set.univ)) ∧ ∀ p ∈ Set.Ioi 0 ×ˢ Set.univ, spaceGrad (I.Hm hΦ m κm (T (Nstar β)) p.1) p.2 = Gh p

∇HTilde_m extends continuously to [0,∞) × ℝ².

twistie3

theorem AVenhance.Infra.Section5.Contracts.twistie3Source_contract (β C₀ A : ℝ) (hA : 0 ≤ A) : ∃ (C : ℝ), 0 ≤ 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 → ℝ) => ∀ (B : ℝ), 0 ≤ B → Integration.TGradientContract β (I.kappaSeq κ M (m - 1)) T A B → Integration.Twistie3SourceContract I hΦ m (I.kappaSeq κ M m) T C B

normie1

theorem AVenhance.Infra.Section5.Contracts.normie1Source_contract (β C₀ A : ℝ) (hA : 0 ≤ A) : ∃ (C : ℝ), 0 ≤ 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 → ℝ) => ∀ (B : ℝ), 0 ≤ B → Integration.FirstOrderGradJetContract I m (I.kappaSeq κ M (m - 1)) T A B → Integration.TGradientContract β (I.kappaSeq κ M (m - 1)) T A B → Integration.Normie1SourceContract I hΦ m (I.kappaSeq κ M m) T C B

normie2

theorem AVenhance.Infra.Section5.Contracts.normie2Source_contract (β C₀ CH : ℝ) (hCH : 0 ≤ CH) : ∃ (C : ℝ), 0 ≤ 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 → ℝ) => ∀ (B : ℝ), 0 ≤ B → Integration.HmGradientContract I hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) T CH B → Integration.Normie2SourceContract I hΦ m (I.kappaSeq κ M m) T C B