Comparison of the actual time profiles and absorption of a finite family at a fixed radius.

noncomputable def EulerPacketCylinderField.profileRatio {K : Type u_1} [TopologicalSpace K] (g b : C(K, ℝ)) (hb : ∀ (t : K), 0 < b t) : C(K, ℝ)

Profile ratio, given by ⟨fun t => g t/b t,g.continuous.div b.continuous (fun t => (hb t).ne')⟩.

Equations

• EulerPacketCylinderField.profileRatio g b hb = { toFun := fun (t : K) => g t / b t, continuous_toFun := ⋯ }

@[simp]

theorem EulerPacketCylinderField.profileRatio_apply {K : Type u_1} [TopologicalSpace K] (g b : C(K, ℝ)) (hb : ∀ (t : K), 0 < b t) (t : K) : (profileRatio g b hb) t = g t / b t

theorem EulerPacketCylinderField.profileRatio_abs_le {K : Type u_1} [TopologicalSpace K] (g b : C(K, ℝ)) (hg : ∀ (t : K), 0 ≤ g t) (hb : ∀ (t : K), 0 < b t) (C : ℝ) (hC : ∀ (t : K), g t ≤ C * b t) (t : K) : |(profileRatio g b hb) t| ≤ C

theorem EulerPacketCylinderField.Field.normalized_changeProfile_path {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (hT : 0 ≤ T) (g b : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (hb : ∀ (t : ↑(Set.Icc 0 T)), 0 < b t) : (G.normalized hT b hb).path = ((G.normalized hT g hg).weighted hT (profileRatio g b hb)).path

theorem EulerPacketCylinderField.Field.WordBound.changeProfile {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} (hT : 0 ≤ T) {g : C(↑(Set.Icc 0 T), ℝ)} (b : C(↑(Set.Icc 0 T), ℝ)) {hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t} (hb : ∀ (t : ↑(Set.Icc 0 T)), 0 < b t) {q d : ℕ} {R A : ℝ} (hG : (G.normalized hT g hg).WordBound q R A d) (C : ℝ) (hC : 0 ≤ C) (hgb : ∀ (t : ↑(Set.Icc 0 T)), g t ≤ C * b t) : (G.normalized hT b hb).WordBound q R (C * A) d

theorem EulerPacketCylinderField.Field.WordBound.enlargeProfile {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} (hT : 0 ≤ T) {g : C(↑(Set.Icc 0 T), ℝ)} (b : C(↑(Set.Icc 0 T), ℝ)) {hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t} (hb : ∀ (t : ↑(Set.Icc 0 T)), 0 < b t) {q d : ℕ} {R A : ℝ} (hG : (G.normalized hT g hg).WordBound q R A d) (hgb : ∀ (t : ↑(Set.Icc 0 T)), g t ≤ b t) : (G.normalized hT b hb).WordBound q R A d

theorem EulerPacketCylinderField.Field.wordBound_normalized_finset_absorb {P T : ℝ} [Fact (0 < P)] (hT : 0 ≤ T) (b : C(↑(Set.Icc 0 T), ℝ)) (hb : ∀ (t : ↑(Set.Icc 0 T)), 0 < b t) {ι : Type u_1} (s : Finset ι) (f : ι → EulerPacketProfileRecursion.VectorField) (W : (i : ι) → Field P T (f i)) (q : ℕ) (R C : ℝ) (d : ℕ) (shift : ι → ℕ) (hR : 1 ≤ R) (hC : 0 ≤ C) (hCR : C ≤ R) (hd : 0 < d) (hcount : s.card ≤ d ^ 2) (hshift : ∀ i ∈ s, shift i < d) (hW : ∀ i ∈ s, ((W i).normalized hT b hb).WordBound q R C (shift i)) : ((finsetSum s f W).normalized hT b hb).WordBound q R 1 d