Exact TMaterialContract adapter retaining the small material rate.

theorem AVenhance.Infra.Section5.Contracts.TMaterialProfiles.terminal_materialGrad_aestronglyMeasurable {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} {κm κprev : ℝ} {θ₀ : 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) : MeasureTheory.AEStronglyMeasurable (fun (z : Section4.AmnrSpace) => LeftToShow.materialGrad (streamVel (Φ (m - 1))) (T (Nstar β)) z.1 z.2) (MeasureTheory.volume.restrict timeCube)

def AVenhance.Infra.Section5.Contracts.TMaterialRateProfile {β : ℝ} (I : Ingredients β) (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (m : ℕ) (κprev : ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (S C : ℝ) : Prop

The source-rate form of the first material estimate before the rate conversion.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Section5.Contracts.TMaterialProfiles.eLpNorm_vec2_le_of_component_bounds {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → Homogenization.Vec 2} {B : ℝ} (hB : 0 ≤ B) (hf : MeasureTheory.AEStronglyMeasurable f μ) (h0 : MeasureTheory.eLpNorm (fun (z : α) => f z 0) 2 μ ≤ ENNReal.ofReal B) (h1 : MeasureTheory.eLpNorm (fun (z : α) => f z 1) 2 μ ≤ ENNReal.ofReal B) : MeasureTheory.eLpNorm f 2 μ ≤ ENNReal.ofReal (2 * B)

theorem AVenhance.Infra.Section5.Contracts.tMaterial_rate_profile_of_spatial_profiles {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm ν : ℝ} (hκm : 0 < κm) (hν : 0 < ν) {g : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθ : IsClassicalSol (streamVel (Φ (m - 1))) ν (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θprev) (hT : I.IsTIterates hΦ m κm ν g θprev T) {L G CA Cb Cd Cg S : ℝ} (hL : 0 < L) (hG : 0 ≤ G) (hCA : 0 ≤ CA) (hCb : 0 ≤ Cb) (hCd : 0 ≤ Cd) (hGscale : G ≤ Cg * (√ν)⁻¹ * S) (hRate : ν * L ^ 2 ≤ Cd * a β I.Λ (m - 1)) (hCoefficient : ∀ (j p : Fin 2) (α : List (Fin 2)), α.length ≤ 2 → ∀ (z : Section4.AmnrSpace), |Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (List.map some α) (Section4.amnrTemperatureCoefficient I hΦ m κm ν j p) z| ≤ CA * ν * L ^ α.length) (hVelocity : ∀ (q p : Fin 2) (z : Section4.AmnrSpace), |Section4.amnrVelocityGradient (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) q p z| ≤ Cb * a β I.Λ (m - 1)) (hSpatial : ∀ i ≤ Nstar β, ∀ (p : Fin 2) (α : List (Fin 2)), α.length ≤ 2 → MeasureTheory.eLpNorm (Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (List.map some α) (Section4.amnrTGradient (T i) p)) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal (G * L ^ α.length)) : TMaterialRateProfile I Φ m ν T S (2 * √2 * tMaterialSpatialStepConstant Cb CA Cd * Cg)

The minimal source-rate estimate. Only spatial words of lengths zero, one and two are consumed; the material-rate coefficient premise is absent.

theorem AVenhance.Infra.Section5.Contracts.tMaterial_contract_of_material_rate {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {m : ℕ} {κprev : ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {S C : ℝ} (hm : 1 ≤ m) (hS : 0 ≤ S) (hC : 0 ≤ C) (hmaterial : TMaterialRateProfile I Φ m κprev T S C) : Integration.TMaterialContract I Φ m κprev T (C * 2 ^ (-27)) S

Convert a material-rate estimate into the exact hDt contract.

The hypothesis is the first-material-level estimate at the actual source rate a β Λ (m - 1). The proved rate lemma supplies a ≤ 2^(-27) ε^(3δ) / τP, so this conversion retains the required small factor.