Genuine regularity and locality data carried by each recursively constructed profile.

theorem EulerPacketCylinderField.Field.zero_time {P T : ℝ} [Fact (0 < P)] (hT : 0 ≤ T) : TimeDerivative hT (zero P T) (zero P T)

theorem EulerPacketCylinderField.raw_zero_changeTime {T : ℝ} {raw : EulerPacketProfileRecursion.VectorField} {T' : ℝ} (h : T = T') (S : Set EulerSmoothLimit.Space) (hs : ∀ (t : ↑(Set.Icc 0 T)), ∀ x ∉ S, ∀ (θ : ℝ), raw (↑t, x, θ) = 0) (t : ↑(Set.Icc 0 T')) (x : EulerSmoothLimit.Space) : x ∉ S → ∀ (θ : ℝ), raw (↑t, x, θ) = 0

structure EulerPacketCylinderField.ProfileRegularity (P T : ℝ) [Fact (0 < P)] (hT : 0 ≤ T) (S : Set EulerSmoothLimit.Space) (a : EulerPacketProfileRecursion.Profile) : Type

Profile regularity data, collecting high, mean, corrector, pressure, highT, meanT and their compatibility conditions.

• high : Field P T a.high

  High-frequency field of ProfileRegularity, of type Field P T a.high.

• mean : Field P T a.mean

  Mean field of ProfileRegularity, of type Field P T a.mean.

• corrector : Field P T a.corrector

  Correction field of ProfileRegularity, of type Field P T a.corrector.

• pressure : Field P T (pressureGradient a.highPressure)

  Pressure field of ProfileRegularity, of type Field P T (pressureGradient a.highPressure).

• highT : EulerPacketProfileRecursion.VectorField

  High T of ProfileRegularity, of type VectorField.

• meanT : EulerPacketProfileRecursion.VectorField

  Mean T of ProfileRegularity, of type VectorField.

• correctorT : EulerPacketProfileRecursion.VectorField

  Corrector T of ProfileRegularity, of type VectorField.

• highDerivative : Field P T self.highT

  High derivative of ProfileRegularity, of type Field P T highT.

• meanDerivative : Field P T self.meanT

  Mean derivative of ProfileRegularity, of type Field P T meanT.

• correctorDerivative : Field P T self.correctorT

  Corrector derivative of ProfileRegularity, of type Field P T correctorT.

• high_time : TimeDerivative hT self.high self.highDerivative
• mean_time : TimeDerivative hT self.mean self.meanDerivative
• corrector_time : TimeDerivative hT self.corrector self.correctorDerivative
• high_zero (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : x ∉ S → ∀ (θ : ℝ), a.high (↑t, x, θ) = 0
• corrector_zero (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : x ∉ S → ∀ (θ : ℝ), a.corrector (↑t, x, θ) = 0
• pressure_zero (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : x ∉ S → ∀ (θ : ℝ), pressureGradient a.highPressure (↑t, x, θ) = 0
• mean_angle (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : a.mean (↑t, x, θ) = a.mean (↑t, x, 0)

def EulerPacketCylinderField.ProfileRegularity.congr {P T : ℝ} [Fact (0 < P)] {hT : 0 ≤ T} {S : Set EulerSmoothLimit.Space} {a b : EulerPacketProfileRecursion.Profile} (G : ProfileRegularity P T hT S a) (h : a = b) : ProfileRegularity P T hT S b

Congr, given by h ▸ G.

Equations

• G.congr h = h ▸ G

noncomputable def EulerPacketCylinderField.ProfileRegularity.zero (P T : ℝ) [Fact (0 < P)] (hT : 0 ≤ T) (S : Set EulerSmoothLimit.Space) : ProfileRegularity P T hT S 0

Zero, bundling high, mean, corrector, pressure and the required compatibility proofs.

Equations

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

def EulerPacketCylinderField.ProfileRegularity.prefixFields {P T : ℝ} [Fact (0 < P)] {hT : 0 ≤ T} {S : Set EulerSmoothLimit.Space} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (G : (i : ℕ) → i < p → ProfileRegularity P T hT S (a i)) : PrefixFields P T p a

Prefix fields, bundling high, mean, corrector.

Equations

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

theorem EulerPacketCylinderField.ProfileRegularity.prefixLocality {P T : ℝ} [Fact (0 < P)] {hT : 0 ≤ T} {S : Set EulerSmoothLimit.Space} {p : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} (G : (i : ℕ) → i < p → ProfileRegularity P T hT S (a i)) : PrefixLocality T p a S