Flux contracts of the divergence-form terms

Producers, in the exact form ∃ C₁, OnA7Instances β C₀ C₁ (… <Name>Contract …), of the smoothness and ℤ²-periodicity contracts of the twistie3, normie1 and normie2 fluxes. At a fixed time t ∈ (0,1) the ξ-sums are finite, the diffusion matrix, ∇T - G_l, ΧTilde ∇G_l are smooth and periodic, and ∇HTilde_m(t) is smooth and periodic for t > 0.

theorem AVenhance.Infra.Section5.Contracts.twistie3FluxSmooth_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.Twistie3FluxSmoothContract I hΦ m (I.kappaSeq κ M m) T

Twistie3FluxSmoothContract (big-bound estimate twistie3_flux_smooth).

theorem AVenhance.Infra.Section5.Contracts.twistie3FluxPeriodic_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.Twistie3FluxPeriodicContract I hΦ m (I.kappaSeq κ M m) T

Twistie3FluxPeriodicContract (big-bound estimate twistie3_flux_periodic).

theorem AVenhance.Infra.Section5.Contracts.normie1FluxSmooth_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.Normie1FluxSmoothContract I hΦ m (I.kappaSeq κ M m) T

Normie1FluxSmoothContract (big-bound estimate normie1_flux_smooth).

theorem AVenhance.Infra.Section5.Contracts.normie1FluxPeriodic_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.Normie1FluxPeriodicContract I hΦ m (I.kappaSeq κ M m) T

Normie1FluxPeriodicContract (big-bound estimate normie1_flux_periodic).

theorem AVenhance.Infra.Section5.Contracts.normie2FluxSmooth_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.Normie2FluxSmoothContract I hΦ m (I.kappaSeq κ M m) T

Normie2FluxSmoothContract (big-bound estimate normie2_flux_smooth).

theorem AVenhance.Infra.Section5.Contracts.normie2FluxPeriodic_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.Normie2FluxPeriodicContract I hΦ m (I.kappaSeq κ M m) T

Normie2FluxPeriodicContract (big-bound estimate normie2_flux_periodic).