Transfer quantitative bounds between genuine witnesses of the same raw field on the interval.

theorem EulerPacketCylinderField.Field.WordBound.ofRawEq {P T : ℝ} [Fact (0 < P)] {raw raw' : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} (H : Field P T raw') {q d : ℕ} {R A : ℝ} (hG : G.WordBound q R A d) (he : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw' (↑t, x, θ) = raw (↑t, x, θ)) : H.WordBound q R A d

theorem EulerPacketCylinderField.Field.WordBound.normalized_of_raw_eq {P T : ℝ} [Fact (0 < P)] {raw raw' : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} (H : Field P T raw') (hT : 0 ≤ T) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) {q d : ℕ} {R A : ℝ} (hG : (G.normalized hT g hg).WordBound q R A d) (he : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw' (↑t, x, θ) = raw (↑t, x, θ)) : (H.normalized hT g hg).WordBound q R A d