Uniform frequency separation for polynomial source sizes. These costs can be placed in the same finite list as the geometric and pressure costs, so the starting stage is chosen only once.

noncomputable def EulerPacketUniformFrequencyScales.parameterEnvelope (J : ℕ) (C c : ℝ) (p q : ℕ) (X : ℝ) (n : ℕ) : ℝ

Parameter envelope, given by C*((J+n : ℕ) : ℝ)^p*(scaleSequence J X n)^q * exp (c*(scaleSequence J X n/((J-1+n : ℕ) : ℝ)^3)).

Equations

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

def EulerPacketUniformFrequencyScales.frequencyCostSpec (A C c : ℝ) (hA : 0 < A) (hC : 0 < C) (p q N : ℕ) (θ : ℝ) (hθ : 0 < θ) : EulerPacketSourceScaleChoice.CostSpec

Frequency cost spec, bundling d, B, N, a and the required compatibility proofs.

Equations

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

theorem EulerPacketUniformFrequencyScales.frequencyCost_eq (J : ℕ) (A C c : ℝ) (hA : 0 < A) (hC : 0 < C) (p q N : ℕ) (θ : ℝ) (hθ : 0 < θ) (X : ℝ) (n : ℕ) : (frequencyCostSpec A C c hA hC p q N θ hθ).cost J (EulerPacketSourceScaleChoice.scaleSequence J X) n = A * parameterEnvelope J C c p q X n ^ N / EulerPacketSourceScaleSequence.frequency J X n ^ θ

theorem EulerPacketUniformFrequencyScales.guard_of_cost_le (J : ℕ) (A C c : ℝ) (hA : 0 < A) (hC : 0 < C) (p q N : ℕ) (θ : ℝ) (hθ : 0 < θ) (X : ℝ) (n : ℕ) (hcost : (frequencyCostSpec A C c hA hC p q N θ hθ).cost J (EulerPacketSourceScaleChoice.scaleSequence J X) n ≤ 1) : A * parameterEnvelope J C c p q X n ^ N ≤ EulerPacketSourceScaleSequence.frequency J X n ^ θ

theorem EulerPacketUniformFrequencyScales.frequency_monotone (J : ℕ) (hJ : 2 ≤ J) (X : ℝ) (hX : 0 ≤ X) : Monotone (EulerPacketSourceScaleSequence.frequency J X)

theorem EulerPacketUniformFrequencyScales.frequency_zero_tendsto_atTop (J : ℕ) (hJ : 1 ≤ J) : Filter.Tendsto (fun (X : ℝ) => EulerPacketSourceScaleSequence.frequency J X 0) Filter.atTop Filter.atTop

theorem EulerPacketUniformFrequencyScales.eventually_all_frequency (J : ℕ) (hJ : 2 ≤ J) (P : ℝ → Prop) (hP : ∀ᶠ (k : ℝ) in Filter.atTop, P k) : ∀ᶠ (X : ℝ) in Filter.atTop, ∀ (n : ℕ), P (EulerPacketSourceScaleSequence.frequency J X n)