Actual time-profile multiplication of raw cylinder witnesses and their same-radius bounds.

theorem EulerContinuousTimeWeight.weight_norm_of_pointwise {K : Type u_1} {E : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (g : C(K, ℝ)) (C : ℝ) (hC : 0 ≤ C) (hg : ∀ (t : K), |g t| ≤ C) : ‖weight g‖ ≤ C

noncomputable def EulerPacketCylinderField.Field.weighted {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (hT : 0 ≤ T) (g : C(↑(Set.Icc 0 T), ℝ)) : Field P T fun (z : EulerPacketPointJets.Domain) => g (Set.projIcc 0 T hT z.1) • raw z

Weighted, constructed using ofLifted.

Equations

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

noncomputable def EulerPacketCylinderField.Field.normalized {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (hT : 0 ≤ T) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) : Field P T fun (z : EulerPacketPointJets.Domain) => (g (Set.projIcc 0 T hT z.1))⁻¹ • raw z

Normalized, given by G.weighted hT (reciprocal g hg).

Equations

• G.normalized hT g hg = G.weighted hT (EulerContinuousTimeWeight.reciprocal g hg)

@[simp]

theorem EulerPacketCylinderField.Field.weighted_path {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (hT : 0 ≤ T) (g : C(↑(Set.Icc 0 T), ℝ)) : (G.weighted hT g).path = (EulerContinuousTimeWeight.weight g) G.path

@[simp]

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

theorem EulerPacketCylinderField.Field.derivative_weighted_path {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (hT : 0 ≤ T) (g : C(↑(Set.Icc 0 T), ℝ)) (i : Fin 4) : ((G.weighted hT g).derivative i).path = ((G.derivative i).weighted hT g).path

theorem EulerPacketCylinderField.Field.derivative_normalized_path {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (hT : 0 ≤ T) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (i : Fin 4) : ((G.normalized hT g hg).derivative i).path = ((G.derivative i).normalized hT g hg).path

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