The three actual, strictly known pieces of a recursive velocity jet.

inductive EulerPacketCylinderField.KnownPiece : Type

The previous corrector carries velocity grade i and profile grade i-1.

• high : KnownPiece
• mean : KnownPiece
• corrector : KnownPiece

@[instance_reducible]

instance EulerPacketCylinderField.instDecidableEqKnownPiece : DecidableEq KnownPiece

Equations

• EulerPacketCylinderField.instDecidableEqKnownPiece x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance EulerPacketCylinderField.instFintypeKnownPiece : Fintype KnownPiece

Equations

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

def EulerPacketCylinderField.KnownPiece.active (k : KnownPiece) (p i : ℕ) : Prop

Active as an element of Prop.

Equations

• EulerPacketCylinderField.KnownPiece.high.active p i = (1 ≤ i ∧ i < p)
• EulerPacketCylinderField.KnownPiece.mean.active p i = (2 ≤ i ∧ i < p)
• EulerPacketCylinderField.KnownPiece.corrector.active p i = (2 ≤ i ∧ i ≤ p)

@[instance_reducible]

instance EulerPacketCylinderField.KnownPiece.instDecidableActive (k : KnownPiece) (p i : ℕ) : Decidable (k.active p i)

Equations

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

def EulerPacketCylinderField.KnownPiece.profileIndex (k : KnownPiece) (i : ℕ) : ℕ

Profile index as an element of ℕ.

Equations

• EulerPacketCylinderField.KnownPiece.high.profileIndex i = i
• EulerPacketCylinderField.KnownPiece.mean.profileIndex i = i
• EulerPacketCylinderField.KnownPiece.corrector.profileIndex i = i - 1

def EulerPacketCylinderField.KnownPiece.raw (k : KnownPiece) (p : ℕ) (a : ℕ → EulerPacketProfileRecursion.Profile) (i : ℕ) : EulerPacketProfileRecursion.VectorField

Raw, with branches according to k.active p i.

Equations

• EulerPacketCylinderField.KnownPiece.high.raw p a i = if EulerPacketCylinderField.KnownPiece.high.active p i then (a i).high else 0
• EulerPacketCylinderField.KnownPiece.mean.raw p a i = if EulerPacketCylinderField.KnownPiece.mean.active p i then (a i).mean else 0
• EulerPacketCylinderField.KnownPiece.corrector.raw p a i = if EulerPacketCylinderField.KnownPiece.corrector.active p i then (a (i - 1)).corrector else 0

noncomputable def EulerPacketCylinderField.KnownPiece.jet (k : KnownPiece) (O : EulerPacketProfileRecursion.Operators) (p : ℕ) (a : ℕ → EulerPacketProfileRecursion.Profile) (z : EulerPacketPointJets.Domain) (i : ℕ) : EulerPacketPointJets.VectorJet

Jet, given by slicedJet O.interval (k.raw p a i) z.

Equations

• k.jet O p a z i = EulerPacketPointJets.slicedJet O.interval (k.raw p a i) z

theorem EulerPacketCylinderField.KnownPiece.jet_zero_of_inactive (k : KnownPiece) (O : EulerPacketProfileRecursion.Operators) (p : ℕ) (a : ℕ → EulerPacketProfileRecursion.Profile) (z : EulerPacketPointJets.Domain) (i : ℕ) (hi : ¬k.active p i) : k.jet O p a z i = 0

theorem EulerPacketCylinderField.KnownPiece.active_profile_lt (k : KnownPiece) (p i : ℕ) (hi : k.active p i) : k.profileIndex i < p

theorem EulerPacketCylinderField.knownJets_eq_pieces (O : EulerPacketProfileRecursion.Operators) (p : ℕ) (hp : 2 ≤ p) (a : ℕ → EulerPacketProfileRecursion.Profile) (hc : (a 0).corrector = 0) (hb : (a 1).mean = 0) (z : EulerPacketPointJets.Domain) (i : ℕ) : EulerPacketProfileRecursion.knownJets O p a z i = KnownPiece.high.jet O p a z i + KnownPiece.mean.jet O p a z i + KnownPiece.corrector.jet O p a z i

noncomputable def EulerPacketCylinderField.PrefixFields.piece {P T : ℝ} [Fact (0 < P)] {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T p a) (k : KnownPiece) (i : ℕ) : Field P T (k.raw p a i)

Each masked component remains an actual field from the strict prefix.

Equations

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

noncomputable def EulerPacketCylinderField.PrefixFields.pieceJet {P T : ℝ} [Fact (0 < P)] {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T p a) (O : EulerPacketProfileRecursion.Operators) (k : KnownPiece) (i : ℕ) : SpatialJetField P T fun (z : EulerPacketPointJets.Domain) => k.jet O p a z i

Piece jet, given by SpatialJetField.ofField O.interval (F.piece k i).

Equations

• F.pieceJet O k i = EulerPacketCylinderField.SpatialJetField.ofField O.interval (F.piece k i)

theorem EulerPacketCylinderField.KnownPiece.high_tangent {T : ℝ} {O : EulerPacketProfileRecursion.Operators} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (h : ∀ i < p, ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), inner ℝ (O.normal (↑t, x, θ)) ((a i).high (↑t, x, θ)) = 0) (i : ℕ) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : inner ℝ (O.normal (↑t, x, θ)) (high.jet O p a (↑t, x, θ) i).1 = 0

theorem EulerPacketCylinderField.KnownPiece.mean_angle {T : ℝ} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (h : ∀ i < p, ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), (a i).mean (↑t, x, θ) = (a i).mean (↑t, x, 0)) (i : ℕ) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : mean.raw p a i (↑t, x, θ) = mean.raw p a i (↑t, x, 0)

theorem EulerPacketCylinderField.PrefixFields.meanPiece_angleIndependent {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (F : PrefixFields P T p a) (h : ∀ i < p, ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), (a i).mean (↑t, x, θ) = (a i).mean (↑t, x, 0)) (i : ℕ) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : AngleIndependentJet fun (θ : ℝ) => KnownPiece.mean.jet O p a (↑t, x, θ) i