Finite algebra on actual cylinder-path witnesses of raw packet fields.

def EulerPacketCylinderField.Field.ofLifted {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (p : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (f : ↑(Set.Icc 0 T) → EulerLiftedGradientSpace.LiftDomain P → EulerSmoothLimit.Space) (hc : ∀ (t : ↑(Set.Icc 0 T)), Continuous (f t)) (hrep : ∀ (t : ↑(Set.Icc 0 T)), ↑↑(p t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f t) (he : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, x, θ) = f t (x, ↑θ)) : Field P T raw

Recover a raw witness from an actual continuous representative of its L² path.

Equations

• EulerPacketCylinderField.Field.ofLifted p hp f hc hrep he = { path := p, orbit := hp, raw_eq := ⋯ }

def EulerPacketCylinderField.Field.congr {P T : ℝ} [Fact (0 < P)] {raw raw' : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (he : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw' (↑t, x, θ) = raw (↑t, x, θ)) : Field P T raw'

Equality is needed only on the actual closed time interval.

Equations

• G.congr he = { path := G.path, orbit := ⋯, raw_eq := ⋯ }

noncomputable def EulerPacketCylinderField.Field.zero (P T : ℝ) [Fact (0 < P)] : Field P T 0

Zero, constructed using ofLifted.

Equations

• EulerPacketCylinderField.Field.zero P T = EulerPacketCylinderField.Field.ofLifted 0 ⋯ (fun (x : ↑(Set.Icc 0 T)) (x_1 : EulerLiftedGradientSpace.LiftDomain P) => 0) ⋯ ⋯ ⋯

noncomputable def EulerPacketCylinderField.Field.add {P T : ℝ} [Fact (0 < P)] {raw raw' : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (H : Field P T raw') : Field P T (raw + raw')

Add, constructed using ofLifted.

Equations

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

noncomputable def EulerPacketCylinderField.Field.neg {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) : Field P T (-raw)

Neg, constructed using ofLifted.

Equations

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

noncomputable def EulerPacketCylinderField.Field.sub {P T : ℝ} [Fact (0 < P)] {raw raw' : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (H : Field P T raw') : Field P T (raw - raw')

Sub, given by (G.add H.neg).congr (fun t x θ => by simp only [sub_eq_add_neg]).

Equations

• G.sub H = (G.add H.neg).congr ⋯

noncomputable def EulerPacketCylinderField.Field.smul {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (c : ℝ) : Field P T (c • raw)

Smul, constructed using ofLifted.

Equations

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

noncomputable def EulerPacketCylinderField.Field.finsetSum {P T : ℝ} [Fact (0 < P)] {ι : Type u_1} (s : Finset ι) (f : ι → EulerPacketProfileRecursion.VectorField) (G : (i : ι) → Field P T (f i)) : Field P T (∑ i ∈ s, f i)

Literal finite raw sums have a single actual continuous L² witness.

Equations

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

@[simp]

theorem EulerPacketCylinderField.Field.add_path {P T : ℝ} [Fact (0 < P)] {raw raw' : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (H : Field P T raw') : (G.add H).path = G.path + H.path

@[simp]

theorem EulerPacketCylinderField.Field.neg_path {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) : G.neg.path = -G.path

@[simp]

theorem EulerPacketCylinderField.Field.smul_path {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (c : ℝ) : (G.smul c).path = c • G.path