The pressure and initial-gradient costs allow one common scale choice with any finite collection of the other source costs. Their finite partial sums control the actual low-bound increments.

noncomputable def EulerPacketPressureScale.goodCostSpec (CM : ℝ) (hCM : 0 ≤ CM) : EulerPacketSourceScaleChoice.CostSpec

Good 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 EulerPacketPressureScale.goodCost_le_spec (J : ℕ) (hJ : 3 ≤ J) (CM : ℝ) (hCM : 0 ≤ CM) (x : ℕ → ℝ) (n : ℕ) (hx : 0 ≤ x n) : 2 * CM * EulerPacketGeometryLowBounds.goodRatio * EulerPacketSourceScaleChoice.goodCost J x n ≤ (goodCostSpec CM hCM).cost J x n

theorem EulerPacketPressureScale.add_series {f g : ℕ → ℝ} {a b : ℝ} (hf : EulerPacketSourceScaleChoice.SmallSeries f a) (hg : EulerPacketSourceScaleChoice.SmallSeries g b) : EulerPacketSourceScaleChoice.SmallSeries (fun (n : ℕ) => f n + g n) (a + b)

theorem EulerPacketPressureScale.finite_sum_le {f : ℕ → ℝ} {a : ℝ} (hf : EulerPacketSourceScaleChoice.SmallSeries f a) (N : ℕ) : ∑ n ∈ Finset.range N, f n ≤ a

theorem EulerPacketPressureScale.upper_increment_series {J : ℕ} {Cθ CM CMn CHn c : ℝ} {x increment error : ℕ → ℝ} {a b e : ℝ} (hg : EulerPacketSourceScaleChoice.SmallSeries (fun (n : ℕ) => 2 * CM * EulerPacketGeometryLowBounds.goodRatio * EulerPacketSourceScaleChoice.goodCost J x n) a) (hb : EulerPacketSourceScaleChoice.SmallSeries (badCost J Cθ CM CMn CHn c x) b) (he : EulerPacketSourceScaleChoice.SmallSeries error e) (h0 : ∀ (n : ℕ), 0 ≤ increment n) (h : ∀ (n : ℕ), increment n ≤ 2 * CM * EulerPacketGeometryLowBounds.goodRatio * EulerPacketSourceScaleChoice.goodCost J x n + badCost J Cθ CM CMn CHn c x n + error n) : EulerPacketSourceScaleChoice.SmallSeries increment (a + b + e)

theorem EulerPacketPressureScale.initial_increment_series {J : ℕ} {Cθ CM CMn CHn c : ℝ} {x increment error : ℕ → ℝ} {b e : ℝ} (hb : EulerPacketSourceScaleChoice.SmallSeries (badCost J Cθ CM CMn CHn c x) b) (he : EulerPacketSourceScaleChoice.SmallSeries error e) (h0 : ∀ (n : ℕ), 0 ≤ increment n) (h : ∀ (n : ℕ), increment n ≤ badCost J Cθ CM CMn CHn c x n + error n) : EulerPacketSourceScaleChoice.SmallSeries increment (b + e)

theorem EulerPacketPressureScale.uniform_choice {ι : Type u_1} [Finite ι] (s : ι → EulerPacketSourceScaleChoice.CostSpec) (Cθ CM CMn CHn c : ℝ) (hθ : 0 ≤ Cθ) (hM : 0 ≤ CM) (hMn : 0 ≤ CMn) (hHn : 0 ≤ CHn) : ∃ (J : ℕ), 3 ≤ J ∧ ∀ (η : ℝ), 0 < η → ∃ (X₀ : ℝ), 8 ≤ X₀ ∧ ∀ (x : ℕ → ℝ), X₀ ≤ x 0 → (∀ (n : ℕ), x (n + 1) = ↑(J + n) ^ 2 * x n) → (∀ (i : ι), EulerPacketSourceScaleChoice.SmallSeries ((s i).cost J x) η) ∧ EulerPacketSourceScaleChoice.SmallSeries (badCost J Cθ CM CMn CHn c x) η ∧ EulerPacketSourceScaleChoice.SmallSeries (fun (n : ℕ) => 2 * CM * EulerPacketGeometryLowBounds.goodRatio * EulerPacketSourceScaleChoice.goodCost J x n) η

The added pressure costs share the stage index and base scale with any finite list of the existing source costs.

theorem EulerPacketPressureScale.literal_uniform_choice {ι : Type u_1} [Finite ι] (s : ι → EulerPacketSourceScaleChoice.CostSpec) (D : ℕ) (Cθ CM CMn CHn c : ℝ) (hθ : 0 ≤ Cθ) (hM : 0 ≤ CM) (hMn : 0 ≤ CMn) (hHn : 0 ≤ CHn) : ∃ (J : ℕ), 3 ≤ J ∧ ∀ (η : ℝ), 0 < η → ∃ (X₀ : ℝ), 8 ≤ X₀ ∧ ∀ (X : ℝ), X₀ ≤ X → X ^ 1000 ≤ Real.exp (X / ↑(J - 1) ^ 7) ∧ X ^ D ≤ Real.exp (X / ↑(J - 1) ^ 4) ∧ (∀ (i : ι), EulerPacketSourceScaleChoice.SmallSeries ((s i).cost J (EulerPacketSourceScaleChoice.scaleSequence J X)) η) ∧ EulerPacketSourceScaleChoice.SmallSeries (badCost J Cθ CM CMn CHn c (EulerPacketSourceScaleChoice.scaleSequence J X)) η ∧ EulerPacketSourceScaleChoice.SmallSeries (fun (n : ℕ) => 2 * CM * EulerPacketGeometryLowBounds.goodRatio * EulerPacketSourceScaleChoice.goodCost J (EulerPacketSourceScaleChoice.scaleSequence J X) n) η

The same choice covers the literal initial polynomial frequency and shear and every subsequent recursively constructed scale.