Stream-function and diffusivity bounds parameter instance

theorem AVenhance.Infra.Section5.RelativeError.TraceInstanceFrozen.e44_rpow_sqrt {e q : ℝ} (he : 0 < e) : √(e ^ q) = e ^ (q / 2)

theorem AVenhance.Infra.Section5.RelativeError.TraceInstanceFrozen.e44_inverse_sqrt_kappa_of_power_lower {e c q ν : ℝ} (he : 0 < e) (hc : 0 < c) (hν : c * e ^ q ≤ ν) : (√ν)⁻¹ ≤ (√c)⁻¹ * e ^ (-q / 2)

theorem AVenhance.Infra.Section5.RelativeError.TraceInstanceFrozen.e44_later_scale_comparisons {e p δ R : ℝ} (he : 0 < e) (he1 : e ≤ 1) (hδ : 0 < δ) (hlater : e ^ (p - δ) ≤ R) : e ^ p ≤ R ∧ e ^ (-δ) ≤ R / e ^ p

The later-scale hypothesis gives the two radius comparisons used by the parameter absorption and the cutoff recombination.

noncomputable def AVenhance.Infra.Section5.RelativeError.e44TraceTailOrder (β : ℝ) : ℕ

Derivative cutoff order used to control the E44 trace tail.

Equations

• AVenhance.Infra.Section5.RelativeError.e44TraceTailOrder β = ⌈(β + AVenhance.gamma β) / 2 / AVenhance.delta β⌉₊

noncomputable def AVenhance.Infra.Section5.RelativeError.e44TraceCutoffAmplitude (β c : ℝ) : ℝ

Amplitude required for the E44 trace frequency cutoff.

Equations

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

noncomputable def AVenhance.Infra.Section5.RelativeError.e44FrozenTraceConstant (β c : ℝ) : ℝ

Fixed positive-word trace constant generated from the diffusivity bounds lower constant. Once c is chosen from l_recurse β C₀, this constant is independent of the Ingredients instance.

Equations

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

theorem AVenhance.Infra.Section5.RelativeError.TraceInstanceFrozen.e44_trace_rpow_le_nat_power {ε p δ : ℝ} (hε : 0 < ε) (hε1 : ε ≤ 1) (n : ℕ) (hn : p ≤ δ * ↑n) : ε.rpow (-p) ≤ ε.rpow (-δ) ^ n

theorem AVenhance.Infra.Section5.RelativeError.e44_trace_numeric_absorption {β c ε : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hc : 0 < c) (hε : 0 < ε) (hε1 : ε ≤ 1) : 2 ^ 24 ≤ c * e44TraceCutoffAmplitude β c ^ 2 ∧ 32 ≤ e44TraceCutoffAmplitude β c ∧ (√c)⁻¹ * ε.rpow (-((β + gamma β) / 2)) * Real.exp (-e44TailExponent * e44TraceCutoffAmplitude β c * ε.rpow (-delta β)) ≤ 1

theorem AVenhance.Infra.Section5.RelativeError.TraceInstanceFrozen.e44_natural_cutoff_data {r R A : ℝ} (hr : 0 < r) (hrR : r ≤ R) (hr1 : r ≤ 1) (hA : 32 ≤ A) : ∃ (M : ℕ), 0 < M ∧ 2 * Real.pi * √2 * ↑M ≤ A / r ∧ A / (2 * r) ≤ 2 * Real.pi * √2 * ↑M ∧ A / r ≤ 2 * Real.pi * √2 * (↑M + 1) ∧ 1 ≤ R / 2 * (↑M + 1)

The floor cutoff realizes the two-sided Fourier radius estimates needed for the low-frequency trace and the analytic tail.

theorem AVenhance.Infra.Section5.RelativeError.e44_streamVelocity_spatialDerivative_bound_of_A3 {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) (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))) (t : ℝ) (x : Homogenization.Vec 2) : ‖Flow.jointSpatialFDeriv (streamVel fun (s : ℝ) (y : Homogenization.Vec 2) => Φ (m - 1) s y) t x‖ ≤ 2 ^ 22 * a β I.Λ (m - 1)

The stream-function estimates second-jet bound gives the actual drift gradient bound used by the low-mode trace estimate.

theorem AVenhance.Infra.Section5.RelativeError.e44_initialTrace_of_A3_A5_data {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {N m : ℕ} (hm : 2 ≤ m) (hmN : m ≤ N) {κ : ℝ} (c C : ℝ) (hc : 0 < c) (_hcC : c < C) (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 < N → c * (AVenhance.a β I.Λ j * epsilon β I.Λ j ^ (2 + gamma β)) ≤ I.kappaAt κ j (N - j) ∧ I.kappaAt κ j (N - j) ≤ C * (AVenhance.a β I.Λ j * epsilon β I.Λ j ^ (2 + gamma β))) {g : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {R : ℝ} (hsol : IsClassicalSol (streamVel fun (t : ℝ) (y : Homogenization.Vec 2) => Φ (m - 1) t y) (I.kappaSeq κ N (m - 1)) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g u) (hθ : IsThetaAnalytic R g) (hmean : ∫ (x : Homogenization.Vec 2) in unitCube, g x = 0) (hκ1 : I.kappaSeq κ N (m - 1) ≤ 1) (hLater : epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2 - delta β) ≤ R) (A : ℝ) (hA1 : 1 ≤ A) (hA5scale : 2 ^ 24 ≤ c * A ^ 2) (Mcut : ℕ) (hMcut : 0 < Mcut) (hKup : 2 * Real.pi * √2 * ↑Mcut ≤ A / epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2)) (hKlower : A / (2 * epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2)) ≤ 2 * Real.pi * √2 * ↑Mcut) (hKupperTail : A / epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) ≤ 2 * Real.pi * √2 * (↑Mcut + 1)) (hTailScale : 1 ≤ R / 2 * (↑Mcut + 1)) (hNumeric : (√c)⁻¹ * (epsilon β I.Λ (m - 1)).rpow (-(β + gamma β) / 2) * Real.exp (-e44TailExponent * A * (epsilon β I.Λ (m - 1)).rpow (-delta β)) ≤ 1) : 1 ≤ e44TraceCombinationConstant A (√3) e44TailConstant ∧ ∀ (w : List (Fin 2)), 1 ≤ w.length → √(∫ (x : Homogenization.Vec 2) in unitCube, Section4.classicalWordDerivative w g x ^ 2) ≤ √(I.kappaSeq κ N (m - 1)) * √(∫ (t : ℝ) in 0..1, classicalCellGradientEnergy u t) * (↑w.length.factorial / (epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) / e44TraceCombinationConstant A (√3) e44TailConstant ^ 2) ^ w.length)

Concrete stream-function and diffusivity bounds trace instance. hNumeric is the explicit large-Λ absorption threshold; the constants and cutoff radius stay visible in the statement so the later-scale and profile-radius checks cannot be hidden.

theorem AVenhance.Infra.Section5.RelativeError.e44_classical_energy_eq_spaceTimeGradNormSq {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {g : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol b κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g u) : ∫ (t : ℝ) in 0..1, classicalCellGradientEnergy u t = spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (u t)

Identify the classical slice-energy integral with the space-time gradient norm used by the initial-trace premise.

theorem AVenhance.Infra.Section5.RelativeError.e44_initialTrace_of_explicit_A3_A5 {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {N m : ℕ} (hm : 2 ≤ m) (hmN : m ≤ N) {κ : ℝ} (c C : ℝ) (hc : 0 < c) (hcC : c < C) (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 < N → c * (AVenhance.a β I.Λ j * epsilon β I.Λ j ^ (2 + gamma β)) ≤ I.kappaAt κ j (N - j) ∧ I.kappaAt κ j (N - j) ≤ C * (AVenhance.a β I.Λ j * epsilon β I.Λ j ^ (2 + gamma β))) {g : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {R : ℝ} (hsol : IsClassicalSol (streamVel fun (t : ℝ) (y : Homogenization.Vec 2) => Φ (m - 1) t y) (I.kappaSeq κ N (m - 1)) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g u) (hθ : IsThetaAnalytic R g) (hmean : ∫ (x : Homogenization.Vec 2) in unitCube, g x = 0) (hκ1 : I.kappaSeq κ N (m - 1) ≤ 1) (hLater : epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2 - delta β) ≤ R) : 1 ≤ e44FrozenTraceConstant β c ∧ ∀ (w : List (Fin 2)), 1 ≤ w.length → √(∫ (x : Homogenization.Vec 2) in unitCube, Section4.classicalWordDerivative w g x ^ 2) ≤ √(I.kappaSeq κ N (m - 1)) * √(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (u t)) * (↑w.length.factorial / (epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) / e44FrozenTraceConstant β c ^ 2) ^ w.length)

The same trace construction with the diffusivity bounds constants supplied explicitly. This is the family-level form: callers may choose c,C before the Ingredients instance and provide the corresponding stream-function and diffusivity bounds.