Step-down estimate theta profile contract with constants fixed before the instance

theorem AVenhance.Infra.Section5.Contracts.ThetaProfile.iterateSpatialWord_eq_classicalWordDerivative (w : List (Fin 2)) (f : Homogenization.Vec 2 → ℝ) : Section4.iterateSpatialWord w f = Section4.classicalWordDerivative w f

theorem AVenhance.Infra.Section5.Contracts.ThetaProfile.theta_profile_of_explicit_A3_A5 {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m M : ℕ} (hm : 2 ≤ m) (hmM : m ≤ M) {κ R : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} (hR : 0 < R) (hscale : epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) ≤ R) (hθ₀ : IsThetaAnalytic R θ₀) (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) (I.kappaSeq κ M (m - 1)) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) {c C Cs : ℝ} (hc : 0 < c) (hcC : c < C) (hRadius : 8 * max (Section4.thetaAnalyticRadiusBase c) 2 ≤ Cs) (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))) (hA5 : ∀ (j : ℕ), 1 ≤ j → j < M → c * (AVenhance.a β I.Λ j * epsilon β I.Λ j ^ (2 + gamma β)) ≤ I.kappaAt κ j (M - j) ∧ I.kappaAt κ j (M - j) ≤ C * (AVenhance.a β I.Λ j * epsilon β I.Λ j ^ (2 + gamma β))) : Section4.iterateCoordinateEnergyProfile θprev (I.kappaSeq κ M (m - 1)) (2 * √(l2NormSq θ₀)) (Cs * epsilon β I.Λ (m - 1) ^ (-1 - gamma β / 2)) 0

theorem AVenhance.Infra.Section5.Contracts.thetaProfile_S_of_explicit_A3_A5_T1h {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m M : ℕ} (hm : 2 ≤ m) (hmM : m ≤ M) {κ Ctr Cs : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} (hCtr : 1 ≤ Ctr) (hmean : Homogenization.MeanZeroOn unitCube θ₀) (hT1h : ∀ (w : List (Fin 2)), 1 ≤ w.length → √(∫ (x : Homogenization.Vec 2) in unitCube, Section4.classicalWordDerivative w θ₀ x ^ 2) ≤ √(I.kappaSeq κ M (m - 1)) * √(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (θprev t)) * (↑w.length.factorial / (epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) / Ctr ^ 2) ^ w.length)) {c C : ℝ} (hc : 0 < c) (hcC : c < C) (hRadius : 8 * max (Section4.thetaAnalyticRadiusBase c) (2 * Ctr ^ 2) ≤ Cs) (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))) (hA5 : ∀ (j : ℕ), 1 ≤ j → j < M → c * (AVenhance.a β I.Λ j * epsilon β I.Λ j ^ (2 + gamma β)) ≤ I.kappaAt κ j (M - j) ∧ I.kappaAt κ j (M - j) ≤ C * (AVenhance.a β I.Λ j * epsilon β I.Λ j ^ (2 + gamma β))) (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) (I.kappaSeq κ M (m - 1)) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) : Integration.ThetaProfileContract I m (I.kappaSeq κ M (m - 1)) θprev Cs (√(I.kappaSeq κ M (m - 1)) * √(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (θprev t)))

S-amplitude theta profile under the literal conditional stream-function and diffusivity bounds data and the named trace input. Cs is an explicit caller-selected profile constant, so the uniform radius can be passed without choosing any constant after the Ingredients instance.

The S-amplitude profile has the same explicit stream-function and diffusivity bounds dependence as the analytic-data profile. hT1h is the named AV-parameter trace instance input until the wrapper lands. Its trace radius is the cutoff scale divided by Ctr^2; this loss is paid by the profile radius constant, chosen before I.

def AVenhance.Infra.Section5.Contracts.T1hThetaInitialTraceInput (β : ℝ) (I : Ingredients β) (κ : ℝ) (M m : ℕ) (θ₀ : Homogenization.Vec 2 → ℝ) (θprev : ℝ → Homogenization.Vec 2 → ℝ) (Ctr : ℝ) : Prop

The named input consumed by the relative theta profile. It is the positive-order wordwise trace, with amplitude exactly the integrated-gradient quantity S and trace radius epsilon^(1+gamma/2) / Ctr^2.

Equations

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

theorem AVenhance.Infra.Section5.Contracts.ThetaProfile.hg_iterateAnalyticWeight_mono_radius {n i : ℕ} {L₁ L₂ : ℝ} (hL₁ : 0 ≤ L₁) (hL : L₁ ≤ L₂) : Section4.iterateAnalyticWeight n i L₁ ≤ Section4.iterateAnalyticWeight n i L₂

theorem AVenhance.Infra.Section5.Contracts.ThetaProfile.hg_iterateCoordinateEnergyProfile_mono_radius {u : ℝ → Homogenization.Vec 2 → ℝ} {κ N L₁ L₂ : ℝ} {i : ℕ} (hL₁ : 0 ≤ L₁) (hL : L₁ ≤ L₂) (hprofile : Section4.iterateCoordinateEnergyProfile u κ N L₁ i) : Section4.iterateCoordinateEnergyProfile u κ N L₂ i

theorem AVenhance.Infra.Section5.Contracts.thetaProfile_S_contract_of_T1h (β C₀ Ctr : ℝ) (hCtr : 1 ≤ Ctr) : ∃ (Cs_S : ℝ), 1 ≤ Cs_S ∧ ∀ (Cs : ℝ), Cs_S ≤ Cs → Integration.OnA8Instances β C₀ 0 fun (I : Ingredients β) (_Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (_hΦ : IsStreamSeq I _Φ) (κ : ℝ) (M : ℕ) (_R : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (m : ℕ) (_θm θprev : ℝ → Homogenization.Vec 2 → ℝ) (_T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) => T1hThetaInitialTraceInput β I κ M m θ₀ θprev Ctr → Integration.ThetaProfileContract I m (I.kappaSeq κ M (m - 1)) θprev Cs (√(I.kappaSeq κ M (m - 1)) * √(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (θprev t)))

Conditional exact ThetaProfileContract at the relative amplitude S. The only additional per-instance premise is the positive-order initial trace. All profile constants are fixed before the Ingredients instance.

theorem AVenhance.Infra.Section5.Contracts.thetaProfile_contract (β C₀ : ℝ) : ∃ (Cs : ℝ) (C₁ : ℝ), Integration.OnA8Instances β C₀ 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 → ℝ) => Integration.ThetaProfileContract I m (I.kappaSeq κ M (m - 1)) θprev Cs (2 * √(l2NormSq θ₀))

The exact step-down estimate theta-profile contract at the amplitude. The stream-function barNorm data and diffusivity bounds diffusivity constants are extracted with constants fixed before the Ingredients instance.