Exact contract adapter for the abstract-amplitude temperature error leaf.
@[instance_reducible]
def
AVenhance.Infra.Section5.Contracts.avInfraSection5ContractsTemperatureErrorNormedAddCommGroup1 :
NormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ)
Equip the spatial matrix space with its coordinate supremum norm.
Equations
Instances For
@[instance_reducible]
noncomputable def
AVenhance.Infra.Section5.Contracts.avInfraSection5ContractsTemperatureErrorNormedSpace2 :
Real normed-space structure for spatial matrices with the coordinate supremum norm.
Equations
Instances For
theorem
AVenhance.Infra.Section5.Contracts.temperatureError_contract
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{κ : ℝ}
{M m : ℕ}
(hκ : κ ∈ permittedInterval β I.Λ M)
(hm : 2 ≤ m)
(hmM : m ≤ M)
{θ₀ : Homogenization.Vec 2 → ℝ}
{θprev : ℝ → Homogenization.Vec 2 → ℝ}
{T : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hT : I.IsTIterates hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) θ₀ θprev T)
(hθ :
IsClassicalSol (streamVel (Φ (m - 1))) (I.kappaSeq κ M (m - 1)) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀
θprev)
(hflow : ∀ (l : ℤ), ContDiff ℝ ↑⊤ fun (z : Section4.AmnrSpace) => I.flowGrad hΦ m l z.1 z.2)
(hflowp : ∀ (t : ℝ), 0 < t → ∀ (l : ℤ), IsZ2Periodic (I.flowGrad hΦ m l t))
(hA3 :
∀ (j : ℕ),
1 ≤ j →
∀ (t : ℝ) (n : ℕ),
2 ≤ n →
barNorm n (2 ^ 8 * (epsilon β I.Λ j)⁻¹) (Φ j t) ≤ ENNReal.ofReal (2 ^ 5 * AVenhance.a β I.Λ j * epsilon β I.Λ j ^ 2 * ((↑n + 2) ^ 2 / (↑n + 1) ^ 3)))
{c Ck K Cflow Cmean Rflow Cθ Rθ C₀ Ct : ℝ}
(hc : 0 < c)
(hCk : 0 ≤ Ck)
(hK : 0 ≤ K)
(hCf : 0 ≤ Cflow)
(hCm : 0 ≤ Cmean)
(hRf : 256 ≤ Rflow)
(hRθ : 0 < Rθ)
(hlower : c * (a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ (2 + gamma β)) ≤ I.kappaSeq κ M (m - 1))
(hupper : I.kappaSeq κ M (m - 1) ≤ Ck * (a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ (2 + gamma β)))
(hC₀ :
Section4.iterateSourceConstant (Section4.iterateBudgetUniversalConstant K Ck c (2 ^ (-25)) Cflow Cmean) Rflow Cθ ≤ C₀)
(hsmall :
C₀ ^ 3 * epsilon β I.Λ (m - 1) ^ (2 * delta β) * max 1 (epsilon β I.Λ (m - 1) ^ (2 + gamma β) * Rθ ^ (-2)) ≤ 1)
(hKm : ∀ (t : ℝ) (j k : Fin 2), |I.Kmat (I.kappaSeq κ M m) m t j k| ≤ K * I.kappaSeq κ M (m - 1))
(hmean :
∀ (j k : Fin 2),
|(timeAvgMat (I.Kmat (I.kappaSeq κ M m) m) - I.kappaSeq κ M (m - 1) • 1) j k| ≤ I.kappaSeq κ M (m - 1) * Cmean * epsilon β I.Λ (m - 1) ^ (2 * delta β))
(hzero :
∀ (t : ℝ) (x : Homogenization.Vec 2) (l : ℤ),
I.hatXiML m l t ≠ 0 →
∀ (j k : Fin 2), |(I.flowGrad hΦ m l t x - 1) j k| ≤ Cflow * epsilon β I.Λ (m - 1) ^ (2 * delta β))
(hpositive :
∀ (t : ℝ) (x : Homogenization.Vec 2) (l : ℤ),
I.hatXiML m l t ≠ 0 →
∀ (p : List (Fin 2)),
1 ≤ p.length →
∀ (j k : Fin 2),
|Section4.iterateSpatialWord p (fun (y : Homogenization.Vec 2) => (I.flowGrad hΦ m l t y - 1) j k) x| ≤ Cflow * ↑p.length.factorial * (Rflow / epsilon β I.Λ (m - 1)) ^ p.length)
(hLater : epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2 - delta β) ≤ Rθ)
(hbase :
Section4.iterateCoordinateEnergyProfile θprev (I.kappaSeq κ M (m - 1))
(√(I.kappaSeq κ M (m - 1)) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev s) x))
(max (C₀ * epsilon β I.Λ (m - 1) ^ (-1 - gamma β / 2)) (C₀ / Rθ)) 0)
(hCt : ↑(Nstar β) * ↑(2 * Nstar β).factorial * C₀ ^ 3 ≤ Ct)
:
Integration.TemperatureErrorContract I m (I.kappaSeq κ M (m - 1)) θprev T Ct
(√(I.kappaSeq κ M (m - 1)) * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θprev s) x))
The abstract-V estimate, with its TemperatureErrorContract conclusion.
The base profile is the ThetaProfileContract at amplitude
S = √κprev · √spaceTimeGradNormSq(∇θprev); the flow and coefficient inputs retain the
precise hypotheses of the underlying open-time estimate.
theorem
AVenhance.Infra.Section5.Contracts.TemperatureError.temperatureError_of_VIncrement
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
{m : ℕ}
{κm κprev : ℝ}
{θ₀ : Homogenization.Vec 2 → ℝ}
{θprev : ℝ → Homogenization.Vec 2 → ℝ}
{T : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
{Cs R S : ℝ}
(hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T)
(hθ : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev)
(hCs : 1 ≤ Cs)
(hS : 0 ≤ S)
(hR : 0 < R)
(hradius : epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) ≤ R)
(hsmall : epsilon β I.Λ (m - 1) ^ (2 * delta β) ≤ (4 * Cs ^ 3)⁻¹)
(hV : Integration.VIncrementContract I m κprev T Cs R S)
:
The zeroth-word slice of the V-increment estimate telescopes to the exact
temperature-error contract. The scale bounds make the source and analytic
maxima equal to one and bound the error amplitude by the requested S.
theorem
AVenhance.Infra.Section5.Contracts.temperatureError_of_thetaProfile_contract
(β Ccut CsReq : ℝ)
(hReq : 1 ≤ CsReq)
:
∃ (Cs : ℝ) (Ct : ℝ) (C₁ : ℝ),
CsReq ≤ Cs ∧ 0 ≤ Ct ∧ Integration.OnA8Instances β Ccut C₁
fun (I : Ingredients β) (_Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (_hΦ : IsStreamSeq I _Φ) (κ : ℝ) (M : ℕ) (R : ℝ)
(_θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (_θm θprev : ℝ → Homogenization.Vec 2 → ℝ)
(T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) =>
∀ (S : ℝ),
0 ≤ S →
Integration.ThetaProfileContract I m (I.kappaSeq κ M (m - 1)) θprev Cs S →
Integration.VIncrementContract I m (I.kappaSeq κ M (m - 1)) T Cs R S →
Integration.TemperatureErrorContract I m (I.kappaSeq κ M (m - 1)) θprev T Ct S
Uniform temperature-error producer from the S-amplitude theta profile and
V-increment contracts. CsReq, the returned error coefficient, and the scale
threshold are all fixed before the ingredient instance. The profile is retained
as the common input shape for the theta-profile producers; the telescoping
estimate itself uses its companion V-increment bound.