Contracts already produced

Each theorem below proves an Integration.*Contract of Integration/OpenInputs.lean exactly, in the producer form ∃ C₁, OnA7Instances β C₀ C₁ (fun … => <Name>Contract …) (no constants needed).

theorem AVenhance.Infra.Section5.Contracts.onA7_basic {β : ℝ} (I : Ingredients β) {κ R : ℝ} {M m : ℕ} (hκ : κ ∈ permittedInterval β I.Λ M) (hR : 0 < R) (hm : mTheta0 β I.Λ R ≤ m) : 2 ≤ m ∧ 0 < I.kappaSeq κ M m

Positivity facts available on the big-bound premise block.

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

ResidualContract (big-bound estimate residual), from the frozenResidualBigBoundResidual.

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

R46FluxSmoothContract (big-bound estimate R46_flux_smooth), from the tIterate_r46Flux_regular.

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

R46FluxPeriodicContract (big-bound estimate R46_flux_periodic), from the tIterate_r46Flux_regular.