Uniform source jet levels for the S-amplitude AMNR Hessian

The upstream source-jet induction (amnr_source_jet_levels_exist) produces its constant after the ingredients I. The constants are however explicit functions of β, I.Chat and I.Czeta, and are monotone in the latter two. This module re-runs the induction with a constant that depends only on β and a common bound C₀ ≥ I.Czeta, I.Chat, so that it may be chosen before I.

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

I-free majorant of amnrStreamMixedCurrentConstant I.

Equations

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

theorem AVenhance.Infra.Section5.RelativeError.amnrStreamMixedCurrentConstant_le_uni {β C₀ : ℝ} (I : Ingredients β) (hz : I.Czeta ≤ C₀) (hh : I.Chat ≤ C₀) : Section4.amnrStreamMixedCurrentConstant I ≤ uniStreamCurrent β C₀

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

I-free majorant of amnrHigherFastConstant I K.

Equations

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

noncomputable def AVenhance.Infra.Section5.RelativeError.uniHigherStep (β C₀ K : ℝ) (n k : ℕ) : ℝ

I-free majorant of amnrHigherVelocityStepConstant I K n k.

Equations

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

theorem AVenhance.Infra.Section5.RelativeError.amnrHigherVelocityStepConstant_le_uni {β C₀ K : ℝ} (I : Ingredients β) (hz : I.Czeta ≤ C₀) (hh : I.Chat ≤ C₀) (hK : 0 ≤ K) (n k : ℕ) : Section4.amnrHigherVelocityStepConstant I K n k ≤ uniHigherStep β C₀ K n k

noncomputable def AVenhance.Infra.Section5.RelativeError.uniAdvance (β C₀ K : ℝ) (cut : ℕ) : ℝ

The advance constant of one source induction level, I-free.

Equations

• AVenhance.Infra.Section5.RelativeError.uniAdvance β C₀ K cut = K + 2 * AVenhance.Infra.Section5.RelativeError.uniHigherStep β C₀ K (cut + 1) (AVenhance.Nstar β)

theorem AVenhance.Infra.Section5.RelativeError.amnrSourceVelocityAdvanceConstant_le_uni {β C₀ K : ℝ} (I : Ingredients β) (hz : I.Czeta ≤ C₀) (hh : I.Chat ≤ C₀) (hK : 0 ≤ K) (cut : ℕ) : Section4.amnrSourceVelocityAdvanceConstant I K cut ≤ uniAdvance β C₀ K cut

noncomputable def AVenhance.Infra.Section5.RelativeError.uniNew (β C₀ K : ℝ) (cut : ℕ) : ℝ

The I-free constant of the next source level.

Equations

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

def AVenhance.Infra.Section5.RelativeError.uniLevelConst (β C₀ : ℝ) : ℕ → ℝ

The I-free constants of the source jet levels.

Equations

• AVenhance.Infra.Section5.RelativeError.uniLevelConst β C₀ 0 = max 1 (AVenhance.Infra.Section4.amnrSpatialVelocityConstant (AVenhance.Nstar β))
• AVenhance.Infra.Section5.RelativeError.uniLevelConst β C₀ cut.succ = AVenhance.Infra.Section5.RelativeError.uniNew β C₀ (AVenhance.Infra.Section5.RelativeError.uniLevelConst β C₀ cut) cut

theorem AVenhance.Infra.Section5.RelativeError.uniHigherStep_nonneg (β C₀ : ℝ) {K : ℝ} (hK : 0 ≤ K) (n k : ℕ) : 0 ≤ uniHigherStep β C₀ K n k

theorem AVenhance.Infra.Section5.RelativeError.one_le_uniNew (β C₀ : ℝ) {K : ℝ} (hK : 1 ≤ K) (cut : ℕ) : 1 ≤ uniNew β C₀ K cut

theorem AVenhance.Infra.Section5.RelativeError.uniLevelConst_one_le (β C₀ : ℝ) (cut : ℕ) : 1 ≤ uniLevelConst β C₀ cut

theorem AVenhance.Infra.Section5.RelativeError.amnrSourceJetLevels_advance_uni {β C C₀ K : ℝ} (I : Ingredients β) (hz : I.Czeta ≤ C₀) (hh : I.Chat ≤ C₀) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {cut : ℕ} (hlevels : Section4.AmnrSourceJetLevels I Φ K cut) (hK : 1 ≤ K) : Section4.AmnrSourceJetLevels I Φ (uniNew β C₀ K cut) (cut + 1)

One complete source induction level with the I-free constant uniNew.

theorem AVenhance.Infra.Section5.RelativeError.uniLevelConst_spec {β C C₀ : ℝ} (I : Ingredients β) (hz : I.Czeta ≤ C₀) (hh : I.Chat ≤ C₀) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) (cut : ℕ) : Section4.AmnrSourceJetLevels I Φ (uniLevelConst β C₀ cut) cut

All source jet levels hold with the I-free constants uniLevelConst.