The actual continuous time weights for the high and mean packet grades.

Exact time-profile bookkeeping for the high, mean, and previous-corrector terms.

def EulerPacketTimeProfile.meanScale (H : ℝ) (p : ℕ) : ℝ

Mean scale, given by H^(2*p-2).

Equations

• EulerPacketTimeProfile.meanScale H p = H ^ (2 * p - 2)

def EulerPacketTimeProfile.highScale (γ H : ℝ) (p : ℕ) : ℝ

High scale, given by γ*meanScale H p.

Equations

• EulerPacketTimeProfile.highScale γ H p = γ * EulerPacketTimeProfile.meanScale H p

theorem EulerPacketTimeProfile.meanScale_pos (H : ℝ) (hH : 0 < H) (p : ℕ) : 0 < meanScale H p

theorem EulerPacketTimeProfile.highScale_pos (γ H : ℝ) (hγ : 0 < γ) (hH : 0 < H) (p : ℕ) : 0 < highScale γ H p

theorem EulerPacketTimeProfile.meanScale_mono (H : ℝ) (hH : 1 ≤ H) {i j : ℕ} (hij : i ≤ j) : meanScale H i ≤ meanScale H j

theorem EulerPacketTimeProfile.highScale_mono (γ H : ℝ) (hγ : 0 ≤ γ) (hH : 1 ≤ H) {i j : ℕ} (hij : i ≤ j) : highScale γ H i ≤ highScale γ H j

theorem EulerPacketTimeProfile.meanScale_slow_identity (H : ℝ) (i j p : ℕ) (hi : 1 ≤ i) (hj : 1 ≤ j) (hp : i + j = p) : meanScale H i * meanScale H j * H ^ 2 = meanScale H p

theorem EulerPacketTimeProfile.slow_mean_mean (H : ℝ) (hH : 1 ≤ H) (i j p : ℕ) (hi : 1 ≤ i) (hj : 1 ≤ j) (hp : i + j = p) : meanScale H i * meanScale H j ≤ meanScale H p

theorem EulerPacketTimeProfile.slow_high_high_mean (γ H : ℝ) (hγ : 0 ≤ γ) (hγH : γ ≤ H) (hH : 1 ≤ H) (i j p : ℕ) (hi : 1 ≤ i) (hj : 1 ≤ j) (hp : i + j = p) : highScale γ H i * highScale γ H j ≤ meanScale H p

theorem EulerPacketTimeProfile.slow_high_high_high (γ H : ℝ) (hγ : 0 ≤ γ) (hγH : γ ≤ H) (hH : 1 ≤ H) (i j p : ℕ) (hi : 1 ≤ i) (hj : 1 ≤ j) (hp : i + j = p) : highScale γ H i * highScale γ H j ≤ highScale γ H p

theorem EulerPacketTimeProfile.slow_mean_high_high (γ H : ℝ) (hγ : 0 ≤ γ) (hH : 1 ≤ H) (i j p : ℕ) (hi : 1 ≤ i) (hj : 1 ≤ j) (hp : i + j = p) : meanScale H i * highScale γ H j ≤ highScale γ H p

theorem EulerPacketTimeProfile.slow_mean_high_mean (γ H : ℝ) (hγ : 0 ≤ γ) (hγH : γ ≤ H) (hH : 1 ≤ H) (i j p : ℕ) (hi : 1 ≤ i) (hj : 1 ≤ j) (hp : i + j = p) : meanScale H i * highScale γ H j ≤ meanScale H p

theorem EulerPacketTimeProfile.fast_mean_high (γ H : ℝ) (i j p : ℕ) (hi : 1 ≤ i) (hj : 1 ≤ j) (hp : i + j = p + 1) : meanScale H i * highScale γ H j = highScale γ H p

theorem EulerPacketTimeProfile.fast_corrector_high_mean (γ H : ℝ) (hγ : 0 ≤ γ) (hγH : γ ≤ H) (hH : 1 ≤ H) (i j p : ℕ) (hi : 2 ≤ i) (hj : 1 ≤ j) (hp : i + j = p + 1) : highScale γ H (i - 1) * highScale γ H j ≤ meanScale H p

theorem EulerPacketTimeProfile.fast_corrector_high_high (γ H : ℝ) (hγ : 0 ≤ γ) (hγH : γ ≤ H) (hH : 1 ≤ H) (i j p : ℕ) (hi : 2 ≤ i) (hj : 1 ≤ j) (hp : i + j = p + 1) : highScale γ H (i - 1) * highScale γ H j ≤ highScale γ H p

theorem EulerPacketTimeProfile.fast_corrector_corrector_mean (γ H : ℝ) (hγ : 0 ≤ γ) (hγH : γ ≤ H) (hH : 1 ≤ H) (i j p : ℕ) (hi : 2 ≤ i) (hj : 2 ≤ j) (hp : i + j = p + 1) : highScale γ H (i - 1) * highScale γ H (j - 1) ≤ meanScale H p

theorem EulerPacketTimeProfile.fast_corrector_corrector_high (γ H : ℝ) (hγ : 0 ≤ γ) (hγH : γ ≤ H) (hH : 1 ≤ H) (i j p : ℕ) (hi : 2 ≤ i) (hj : 2 ≤ j) (hp : i + j = p + 1) : highScale γ H (i - 1) * highScale γ H (j - 1) ≤ highScale γ H p

theorem EulerPacketTimeProfile.previous_linear_mean (γ H : ℝ) (hγ : 0 ≤ γ) (hγH : γ ≤ H) (hH : 1 ≤ H) (p : ℕ) (hp : 2 ≤ p) : highScale γ H (p - 1) ≤ meanScale H p

structure EulerPacketTimeProfile.Scales (K : Type u_1) [TopologicalSpace K] : Type u_1

Scales data, collecting growth, growth_pos, H0, H0_one_le, growth_le.

• growth : C(K, ℝ)

  Growth of Scales, of type C(K,ℝ).

• growth_pos (t : K) : 0 < self.growth t
• H0 : ℝ

  H0 of Scales, of type ℝ.

• H0_one_le : 1 ≤ self.H0
• growth_le (t : K) : self.growth t ≤ self.H0

noncomputable def EulerPacketTimeProfile.Scales.ofGrowth {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (g : C(K, ℝ)) (hg : ∀ (t : K), 0 < g t) : Scales K

Compactness supplies the single grade-independent upper scale.

Equations

• EulerPacketTimeProfile.Scales.ofGrowth g hg = { growth := g, growth_pos := hg, H0 := max 1 ‖g‖, H0_one_le := ⋯, growth_le := ⋯ }

def EulerPacketTimeProfile.Scales.mean {K : Type u_1} [TopologicalSpace K] (S : Scales K) (p : ℕ) : C(K, ℝ)

Mean, given by ContinuousMap.const K (meanScale S.H0 p).

Equations

• S.mean p = ContinuousMap.const K (EulerPacketTimeProfile.meanScale S.H0 p)

def EulerPacketTimeProfile.Scales.high {K : Type u_1} [TopologicalSpace K] (S : Scales K) (p : ℕ) : C(K, ℝ)

High, given by S.growth*S.mean p.

Equations

• S.high p = S.growth * S.mean p

@[simp]

theorem EulerPacketTimeProfile.Scales.mean_apply {K : Type u_1} [TopologicalSpace K] (S : Scales K) (p : ℕ) (t : K) : (S.mean p) t = meanScale S.H0 p

@[simp]

theorem EulerPacketTimeProfile.Scales.high_apply {K : Type u_1} [TopologicalSpace K] (S : Scales K) (p : ℕ) (t : K) : (S.high p) t = highScale (S.growth t) S.H0 p

theorem EulerPacketTimeProfile.Scales.H0_pos {K : Type u_1} [TopologicalSpace K] (S : Scales K) : 0 < S.H0

theorem EulerPacketTimeProfile.Scales.mean_pos {K : Type u_1} [TopologicalSpace K] (S : Scales K) (p : ℕ) (t : K) : 0 < (S.mean p) t

theorem EulerPacketTimeProfile.Scales.high_pos {K : Type u_1} [TopologicalSpace K] (S : Scales K) (p : ℕ) (t : K) : 0 < (S.high p) t

theorem EulerPacketTimeProfile.Scales.mean_mono {K : Type u_1} [TopologicalSpace K] (S : Scales K) {i j : ℕ} (hij : i ≤ j) (t : K) : (S.mean i) t ≤ (S.mean j) t

theorem EulerPacketTimeProfile.Scales.high_mono {K : Type u_1} [TopologicalSpace K] (S : Scales K) {i j : ℕ} (hij : i ≤ j) (t : K) : (S.high i) t ≤ (S.high j) t

theorem EulerPacketTimeProfile.Scales.high_one {K : Type u_1} [TopologicalSpace K] (S : Scales K) (t : K) : (S.high 1) t = S.growth t

theorem EulerPacketTimeProfile.Scales.slow_mean_mean_bound {K : Type u_1} [TopologicalSpace K] (S : Scales K) (i j p : ℕ) (hi : 1 ≤ i) (hj : 1 ≤ j) (hp : i + j = p) (t : K) : (S.mean i) t * (S.mean j) t ≤ (S.mean p) t

theorem EulerPacketTimeProfile.Scales.slow_high_high_mean_bound {K : Type u_1} [TopologicalSpace K] (S : Scales K) (i j p : ℕ) (hi : 1 ≤ i) (hj : 1 ≤ j) (hp : i + j = p) (t : K) : (S.high i) t * (S.high j) t ≤ (S.mean p) t

theorem EulerPacketTimeProfile.Scales.slow_high_high_high_bound {K : Type u_1} [TopologicalSpace K] (S : Scales K) (i j p : ℕ) (hi : 1 ≤ i) (hj : 1 ≤ j) (hp : i + j = p) (t : K) : (S.high i) t * (S.high j) t ≤ (S.high p) t

theorem EulerPacketTimeProfile.Scales.slow_mean_high_mean_bound {K : Type u_1} [TopologicalSpace K] (S : Scales K) (i j p : ℕ) (hi : 1 ≤ i) (hj : 1 ≤ j) (hp : i + j = p) (t : K) : (S.mean i) t * (S.high j) t ≤ (S.mean p) t

theorem EulerPacketTimeProfile.Scales.slow_mean_high_high_bound {K : Type u_1} [TopologicalSpace K] (S : Scales K) (i j p : ℕ) (hi : 1 ≤ i) (hj : 1 ≤ j) (hp : i + j = p) (t : K) : (S.mean i) t * (S.high j) t ≤ (S.high p) t

theorem EulerPacketTimeProfile.Scales.fast_mean_high_bound {K : Type u_1} [TopologicalSpace K] (S : Scales K) (i j p : ℕ) (hi : 1 ≤ i) (hj : 1 ≤ j) (hp : i + j = p + 1) (t : K) : (S.mean i) t * (S.high j) t = (S.high p) t

theorem EulerPacketTimeProfile.Scales.fast_corrector_high_mean_bound {K : Type u_1} [TopologicalSpace K] (S : Scales K) (i j p : ℕ) (hi : 2 ≤ i) (hj : 1 ≤ j) (hp : i + j = p + 1) (t : K) : (S.high (i - 1)) t * (S.high j) t ≤ (S.mean p) t

theorem EulerPacketTimeProfile.Scales.fast_corrector_high_high_bound {K : Type u_1} [TopologicalSpace K] (S : Scales K) (i j p : ℕ) (hi : 2 ≤ i) (hj : 1 ≤ j) (hp : i + j = p + 1) (t : K) : (S.high (i - 1)) t * (S.high j) t ≤ (S.high p) t

theorem EulerPacketTimeProfile.Scales.fast_corrector_corrector_mean_bound {K : Type u_1} [TopologicalSpace K] (S : Scales K) (i j p : ℕ) (hi : 2 ≤ i) (hj : 2 ≤ j) (hp : i + j = p + 1) (t : K) : (S.high (i - 1)) t * (S.high (j - 1)) t ≤ (S.mean p) t

theorem EulerPacketTimeProfile.Scales.fast_corrector_corrector_high_bound {K : Type u_1} [TopologicalSpace K] (S : Scales K) (i j p : ℕ) (hi : 2 ≤ i) (hj : 2 ≤ j) (hp : i + j = p + 1) (t : K) : (S.high (i - 1)) t * (S.high (j - 1)) t ≤ (S.high p) t

theorem EulerPacketTimeProfile.Scales.previous_linear_mean_bound {K : Type u_1} [TopologicalSpace K] (S : Scales K) (p : ℕ) (hp : 2 ≤ p) (t : K) : (S.high (p - 1)) t ≤ (S.mean p) t