Uniform primitive coefficient constants for the S-amplitude AMNR Hessian

I-uniform versions (constants depending only on β and the common bound C₀) of the mixed velocity-gradient, flow-gradient, flow-average, seed-multiplier and temperature-coefficient bounds proved upstream with constants chosen after I. The proofs follow the upstream ones verbatim, substituting the uniform source jet levels of ATensorBoundLevels.

noncomputable def AVenhance.Infra.Section5.RelativeError.uniCb (β C₀ : ℝ) : ℝ

Uniform velocity-gradient constant.

Equations

• AVenhance.Infra.Section5.RelativeError.uniCb β C₀ = AVenhance.Infra.Section5.RelativeError.uniLevelConst β C₀ (AVenhance.Nstar β)

theorem AVenhance.Infra.Section5.RelativeError.one_le_uniCb (β C₀ : ℝ) : 1 ≤ uniCb β C₀

noncomputable def AVenhance.Infra.Section5.RelativeError.uniFlowGrad (β C₀ : ℝ) : ℝ

Uniform flow-gradient constant.

Equations

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

noncomputable def AVenhance.Infra.Section5.RelativeError.uniFlowAvg (β C₀ : ℝ) : ℝ

Uniform flow-average constant.

Equations

• AVenhance.Infra.Section5.RelativeError.uniFlowAvg β C₀ = 3 * 2 ^ AVenhance.Nstar β * C₀ * AVenhance.Infra.Section5.RelativeError.uniFlowGrad β C₀

noncomputable def AVenhance.Infra.Section5.RelativeError.uniFlowAvgA0Plus (β C₀ : ℝ) : ℝ

Uniform corrected-form flow-average constant, with the extra cutoff-flow factor estimated by the mixed product rule.

Equations

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

noncomputable def AVenhance.Infra.Section5.RelativeError.uniSeedA0Plus (β C₀ : ℝ) : ℝ

Uniform corrected-form seed constant: the old memory factor multiplies the two-flow cutoff average.

Equations

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

noncomputable def AVenhance.Infra.Section5.RelativeError.uniCoeff (β C₀ : ℝ) : ℝ

Uniform temperature-coefficient constant.

Equations

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

theorem AVenhance.Infra.Section5.RelativeError.uniFlowGrad_nonneg (β C₀ : ℝ) : 0 ≤ uniFlowGrad β C₀

theorem AVenhance.Infra.Section5.RelativeError.uni_velocityGradient_mixed_bounds {β C C₀ : ℝ} (I : Ingredients β) (hz : I.Czeta ≤ C₀) (hh : I.Chat ≤ C₀) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) (m : ℕ) : 1 ≤ m → ∀ (i p : Fin 2) (w : List (Option (Fin 2))), Section4.IsAmnrMixedWord w → Section4.amnrBudget w + 2 ≤ Nstar β → ∀ (z : Section4.AmnrSpace), |Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) w (Section4.amnrVelocityGradient (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) i p) z| ≤ uniCb β C₀ * (tauP β I.Λ m)⁻¹ * Section4.amnrWeight (epsilon β I.Λ (m - 1) ^ (-(1 + gamma β / 2))) (tauP β I.Λ m)⁻¹ w

Uniform mixed velocity-gradient bounds.

theorem AVenhance.Infra.Section5.RelativeError.uni_flowGrad_mixed_bounds {β C C₀ : ℝ} (I : Ingredients β) (hz : I.Czeta ≤ C₀) (hh : I.Chat ≤ C₀) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) (m : ℕ) : 1 ≤ m → ∀ (l : ℤ) (α : List (Fin 2)) (n : ℕ), α.length + 2 * n ≤ Nstar β → ∀ (z : Section4.AmnrSpace), |z.1 - ↑l * tauPP β I.Λ m| ≤ tauPP β I.Λ m / 2 + tauP β I.Λ m → ∀ (i p : Fin 2), |Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) (Section4.amnrMixedWord α n) (fun (y : Section4.AmnrSpace) => I.flowGrad hΦ m l y.1 y.2 i p) z| ≤ uniFlowGrad β C₀ * (epsilon β I.Λ (m - 1) ^ (-(1 + gamma β / 2))) ^ α.length * (tauP β I.Λ m)⁻¹ ^ n

Uniform mixed flow-gradient bounds.

theorem AVenhance.Infra.Section5.RelativeError.uni_flowAverage_mixed_bounds {β C C₀ : ℝ} (I : Ingredients β) (hz : I.Czeta ≤ C₀) (hh : I.Chat ≤ C₀) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) (m : ℕ) : 1 ≤ m → ∀ (k p : Fin 2) (w : List (Option (Fin 2))), Section4.IsAmnrMixedWord w → Section4.amnrBudget w ≤ Nstar β → ∀ (z : Section4.AmnrSpace), |Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) w (Section4.amnrFlowAverage I hΦ m k p) z| ≤ uniFlowAvg β C₀ * Section4.amnrWeight (epsilon β I.Λ (m - 1) ^ (-(1 + gamma β / 2))) (tauP β I.Λ m)⁻¹ w

Uniform mixed flow-average bounds.

theorem AVenhance.Infra.Section5.RelativeError.uni_seedMultiplierA0Plus_mixed_bounds {β C C₀ : ℝ} (I : Ingredients β) (hz : I.Czeta ≤ C₀) (hh : I.Chat ≤ C₀) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) (m : ℕ) : 1 ≤ m → ∀ (κ : ℝ), 0 < κ → ∀ n ≤ Nstar β, ∀ (j k i p : Fin 2) (w : List (Option (Fin 2))), Section4.IsAmnrMixedWord w → Section4.amnrBudget w ≤ Nstar β → ∀ (z : Section4.AmnrSpace), |Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) w (Section4.amnrSeedMultiplierA0Plus I hΦ m κ n j k i p) z| ≤ uniSeedA0Plus β C₀ * (epsilon β I.Λ m ^ 2 / κ) * Section4.amnrWeight (epsilon β I.Λ (m - 1) ^ (-(1 + gamma β / 2))) (tauP β I.Λ m)⁻¹ w

Uniform mixed bounds for the corrected-form candidate seed multiplier. The constants depend only on (β,C₀) and precede the instance I.

theorem AVenhance.Infra.Section5.RelativeError.uni_temperatureCoefficient_mixed_of_step_size {β C C₀ : ℝ} (I : Ingredients β) (hz : I.Czeta ≤ C₀) (hh : I.Chat ≤ C₀) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) (m : ℕ) : 1 ≤ m → ∀ (κm κprev : ℝ), 0 < κm → 0 < κprev → epsilon β I.Λ m ^ 2 ≤ κm * tau β I.Λ m → κm + AVenhance.a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κm ≤ 160 / 9 * κprev → ∀ (i j : Fin 2) (w : List (Option (Fin 2))), Section4.IsAmnrMixedWord w → Section4.amnrBudget w ≤ Nstar β → ∀ (z : Section4.AmnrSpace), |Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) w (Section4.amnrTemperatureCoefficient I hΦ m κm κprev i j) z| ≤ uniCoeff β C₀ * κprev * Section4.amnrWeight (epsilon β I.Λ (m - 1) ^ (-(1 + gamma β / 2))) (tauP β I.Λ m)⁻¹ w

Uniform primitive temperature coefficient jets without an interior-scale restriction.

theorem AVenhance.Infra.Section5.RelativeError.uni_temperatureCoefficient_mixed_bounds_through_top {β Creg C₀ c C : ℝ} (I : Ingredients β) (hz : I.Czeta ≤ C₀) (hh : I.Chat ≤ C₀) (hc : 0 < c) (hcC : c < C) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds Creg I Φ) (κ : ℝ) (M : ℕ) : 0 < κ → κ ∈ permittedInterval β I.Λ M → ((∀ (m : ℕ), 1 ≤ m → m < M → c * (AVenhance.a β I.Λ m * epsilon β I.Λ m ^ (2 + gamma β)) ≤ I.kappaAt κ m (M - m) ∧ I.kappaAt κ m (M - m) ≤ C * (AVenhance.a β I.Λ m * epsilon β I.Λ m ^ (2 + gamma β))) ∧ ∀ (m : ℕ), 2 ≤ m → m < M → c * epsilon β I.Λ (m - 1) ^ (4 * delta β) ≤ epsilon β I.Λ m ^ 2 / (I.kappaAt κ m (M - m) * tau β I.Λ m) ∧ epsilon β I.Λ m ^ 2 / (I.kappaAt κ m (M - m) * tau β I.Λ m) ≤ C * epsilon β I.Λ (m - 1) ^ (4 * delta β)) → ∀ (m : ℕ), 2 ≤ m → m ≤ M → Section4.amnrSourceRatioConstant β C * epsilon β I.Λ (m - 1) ^ (2 * delta β) ≤ 1 / 2 → Section3.lAmtOneStepConstant β C₀ * (Section4.amnrSourceRatioConstant β C * epsilon β I.Λ (m - 1) ^ (2 * delta β) + epsilon β I.Λ (m - 1) ^ delta β) ≤ 9 / 160 → ∀ (i j : Fin 2) (w : List (Option (Fin 2))), Section4.IsAmnrMixedWord w → Section4.amnrBudget w ≤ Nstar β → ∀ (z : Section4.AmnrSpace), |Section4.amnrWord (fun (y : Section4.AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) w (Section4.amnrTemperatureCoefficient I hΦ m (I.kappaAt κ m (M - m)) (I.kappaAt κ (m - 1) (M - (m - 1))) i j) z| ≤ uniCoeff β C₀ * I.kappaAt κ (m - 1) (M - (m - 1)) * Section4.amnrWeight (epsilon β I.Λ (m - 1) ^ (-(1 + gamma β / 2))) (tauP β I.Λ m)⁻¹ w

Uniform literal-source coefficient bounds through the terminal permitted scale.