The literal initial packet is the sum of its oscillating high part and its angle-independent mean part. Every field below is realized by the already constructed continuous cylinder L² paths.

Time evaluation and constant extension preserve every genuine spatial word bound. Restoring a time weight uses its value at that time, retaining the source's initial alpha factor.

def EulerContinuousTimeFreeze.freezePath {K : Type u_1} {E : Type u_2} [TopologicalSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (t : K) : C(K, E) →L[ℝ] C(K, E)

Freeze path, given by (ContinuousLinearMap.const ℝ K).comp (ContinuousMap.evalCLM ℝ t).

Equations

• EulerContinuousTimeFreeze.freezePath t = ContinuousLinearMap.const ℝ K ∘SL ContinuousMap.evalCLM ℝ t

@[simp]

theorem EulerContinuousTimeFreeze.freezePath_apply {K : Type u_1} {E : Type u_2} [TopologicalSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (t s : K) (p : C(K, E)) : ((freezePath t) p) s = p t

theorem EulerContinuousTimeFreeze.freezePath_norm {K : Type u_1} {E : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup E] [NormedSpace ℝ E] (t : K) : ‖freezePath t‖ ≤ 1

theorem EulerPacketCylinderField.Field.freezePath_translate {P T : ℝ} [Fact (0 < P)] (t : ↑(Set.Icc 0 T)) (p : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 P))) (a : EulerLiftedGradientSpace.LiftTangent) : (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeFreeze.freezePath t) p) = (EulerContinuousTimeFreeze.freezePath t) ((EulerLpCylinderTranslation.pathTranslate P a) p)

noncomputable def EulerPacketCylinderField.Field.freeze {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (t : ↑(Set.Icc 0 T)) : Field P T fun (z : EulerPacketPointJets.Domain) => raw (↑t, z.2)

Freeze, constructed using ofLifted.

Equations

• G.freeze t = EulerPacketCylinderField.Field.ofLifted ((EulerContinuousTimeFreeze.freezePath t) G.path) ⋯ (fun (x : ↑(Set.Icc 0 T)) => EulerCylinderSmoothOrbit.pointField P G.path ⋯ t) ⋯ ⋯ ⋯

@[simp]

theorem EulerPacketCylinderField.Field.freeze_path {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (t : ↑(Set.Icc 0 T)) : (G.freeze t).path = (EulerContinuousTimeFreeze.freezePath t) G.path

theorem EulerPacketCylinderField.Field.WordBound.freeze {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q d : ℕ} {R A : ℝ} (hG : G.WordBound q R A d) (t : ↑(Set.Icc 0 T)) : (G.freeze t).WordBound q R A d

theorem EulerPacketCylinderField.Field.freeze_normalized_restore {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) (t : ↑(Set.Icc 0 T)) : (G.freeze t).path = (((G.normalized hT g hg).freeze t).smul (g t)).path

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

theorem EulerPacketCylinderField.ProfileBudget.high_freeze {P T : ℝ} [Fact (0 < P)] {hT : 0 ≤ T} {support : Set EulerSmoothLimit.Space} {a : EulerPacketProfileRecursion.Profile} {G : ProfileRegularity P T hT support a} {S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)} {R : ℝ} {p : ℕ} (hG : ProfileBudget G S R p) (t : ↑(Set.Icc 0 T)) : (G.high.freeze t).WordBound 6 R ((S.high p) t) (EulerPacketShiftArithmetic.highShift p)

theorem EulerPacketCylinderField.ProfileBudget.corrector_freeze {P T : ℝ} [Fact (0 < P)] {hT : 0 ≤ T} {support : Set EulerSmoothLimit.Space} {a : EulerPacketProfileRecursion.Profile} {G : ProfileRegularity P T hT support a} {S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)} {R : ℝ} {p : ℕ} (hG : ProfileBudget G S R p) (t : ↑(Set.Icc 0 T)) : (G.corrector.freeze t).WordBound 6 R ((S.high p) t) (EulerPacketShiftArithmetic.highShift p)

theorem EulerPacketCylinderField.ProfileBudget.mean_freeze {P T : ℝ} [Fact (0 < P)] {hT : 0 ≤ T} {support : Set EulerSmoothLimit.Space} {a : EulerPacketProfileRecursion.Profile} {G : ProfileRegularity P T hT support a} {S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T)} {R : ℝ} {p : ℕ} (hG : ProfileBudget G S R p) (t : ↑(Set.Icc 0 T)) : (G.mean.freeze t).WordBound 6 R ((S.mean p) t) (EulerPacketShiftArithmetic.meanShift p)

def EulerPacketInitial.timeSlice (t : ℝ) (f : EulerPacketProfileRecursion.VectorField) : EulerPacketProfileRecursion.VectorField

Time slice, defined pointwise by f (t,z.2).

Equations

• EulerPacketInitial.timeSlice t f z = f (t, z.2)

def EulerPacketInitial.highGrade (N : ℕ) (t : ℝ) (a : ℕ → EulerPacketProfileRecursion.Profile) : ℕ → EulerPacketProfileRecursion.VectorField

High grade, given by assemble N (fun i => timeSlice t (a i).high) (fun i => timeSlice t (a i).corrector).

Equations

• EulerPacketInitial.highGrade N t a = EulerFiniteGrades.assemble N (fun (i : ℕ) => EulerPacketInitial.timeSlice t (a i).high) fun (i : ℕ) => EulerPacketInitial.timeSlice t (a i).corrector

def EulerPacketInitial.meanGrade (N : ℕ) (t : ℝ) (a : ℕ → EulerPacketProfileRecursion.Profile) : ℕ → EulerPacketProfileRecursion.VectorField

Mean grade, given by truncate N (fun i => timeSlice t (a i).mean).

Equations

• EulerPacketInitial.meanGrade N t a = EulerFiniteGrades.truncate N fun (i : ℕ) => EulerPacketInitial.timeSlice t (a i).mean

noncomputable def EulerPacketInitial.high (N : ℕ) (κ t : ℝ) (a : ℕ → EulerPacketProfileRecursion.Profile) : EulerPacketProfileRecursion.VectorField

High, given by fieldSum (N+1) κ (highGrade N t a).

Equations

• EulerPacketInitial.high N κ t a = EulerPacketPointJets.fieldSum (N + 1) κ (EulerPacketInitial.highGrade N t a)

noncomputable def EulerPacketInitial.mean (N : ℕ) (κ t : ℝ) (a : ℕ → EulerPacketProfileRecursion.Profile) : EulerPacketProfileRecursion.VectorField

Mean, given by fieldSum (N+1) κ (meanGrade N t a).

Equations

• EulerPacketInitial.mean N κ t a = EulerPacketPointJets.fieldSum (N + 1) κ (EulerPacketInitial.meanGrade N t a)

theorem EulerPacketInitial.high_eq (N : ℕ) (κ t : ℝ) (a : ℕ → EulerPacketProfileRecursion.Profile) : high N κ t a = (EulerPacketPointJets.fieldSum N κ fun (i : ℕ) => timeSlice t (a i).high) + κ • EulerPacketPointJets.fieldSum N κ fun (i : ℕ) => timeSlice t (a i).corrector

theorem EulerPacketInitial.mean_eq (N : ℕ) (κ t : ℝ) (a : ℕ → EulerPacketProfileRecursion.Profile) : mean N κ t a = EulerPacketPointJets.fieldSum N κ fun (i : ℕ) => timeSlice t (a i).mean

theorem EulerPacketInitial.packet_split (N : ℕ) (κ t : ℝ) (a : ℕ → EulerPacketProfileRecursion.Profile) : timeSlice t (EulerPacketPointJets.fieldSum (N + 1) κ (EulerPacketProfileRecursion.assembledVelocity N a)) = high N κ t a + mean N κ t a

noncomputable def EulerPacketInitial.highGradeField {P T : ℝ} [Fact (0 < P)] {hT : 0 ≤ T} {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} {support : Set EulerSmoothLimit.Space} (G : (i : ℕ) → i ≤ N → EulerPacketCylinderField.ProfileRegularity P T hT support (a i)) (t : ↑(Set.Icc 0 T)) (n : ℕ) : EulerPacketCylinderField.Field P T (highGrade N (↑t) a n)

High grade field, given by Field.assembleFamily N _ _ (fun i hi => (G i hi).high.freeze t) (fun i hi => (G i hi).corrector.freeze t) n.

Equations

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

noncomputable def EulerPacketInitial.meanGradeField {P T : ℝ} [Fact (0 < P)] {hT : 0 ≤ T} {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} {support : Set EulerSmoothLimit.Space} (G : (i : ℕ) → i ≤ N → EulerPacketCylinderField.ProfileRegularity P T hT support (a i)) (t : ↑(Set.Icc 0 T)) (n : ℕ) : EulerPacketCylinderField.Field P T (meanGrade N (↑t) a n)

Mean grade field, given by Field.truncateFamily N _ (fun i hi => (G i hi).mean.freeze t) n.

Equations

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

noncomputable def EulerPacketInitial.highField {P T : ℝ} [Fact (0 < P)] {hT : 0 ≤ T} {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} {support : Set EulerSmoothLimit.Space} (G : (i : ℕ) → i ≤ N → EulerPacketCylinderField.ProfileRegularity P T hT support (a i)) (t : ↑(Set.Icc 0 T)) (κ : ℝ) : EulerPacketCylinderField.Field P T (high N κ (↑t) a)

High field, given by Field.evaluateFamily (N+1) κ _ (highGradeField G t).

Equations

• EulerPacketInitial.highField G t κ = EulerPacketCylinderField.Field.evaluateFamily (N + 1) κ (EulerPacketInitial.highGrade N (↑t) a) (EulerPacketInitial.highGradeField G t)

noncomputable def EulerPacketInitial.meanField {P T : ℝ} [Fact (0 < P)] {hT : 0 ≤ T} {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} {support : Set EulerSmoothLimit.Space} (G : (i : ℕ) → i ≤ N → EulerPacketCylinderField.ProfileRegularity P T hT support (a i)) (t : ↑(Set.Icc 0 T)) (κ : ℝ) : EulerPacketCylinderField.Field P T (mean N κ (↑t) a)

Mean field, given by Field.evaluateFamily (N+1) κ _ (meanGradeField G t).

Equations

• EulerPacketInitial.meanField G t κ = EulerPacketCylinderField.Field.evaluateFamily (N + 1) κ (EulerPacketInitial.meanGrade N (↑t) a) (EulerPacketInitial.meanGradeField G t)

theorem EulerPacketInitial.high_zero_outside {P T : ℝ} [Fact (0 < P)] {hT : 0 ≤ T} {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} {support : Set EulerSmoothLimit.Space} (G : (i : ℕ) → i ≤ N → EulerPacketCylinderField.ProfileRegularity P T hT support (a i)) (t : ↑(Set.Icc 0 T)) (κ s : ℝ) (x : EulerSmoothLimit.Space) (hx : x ∉ support) (θ : ℝ) : high N κ (↑t) a (s, x, θ) = 0

theorem EulerPacketInitial.mean_angle {P T : ℝ} [Fact (0 < P)] {hT : 0 ≤ T} {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} {support : Set EulerSmoothLimit.Space} (G : (i : ℕ) → i ≤ N → EulerPacketCylinderField.ProfileRegularity P T hT support (a i)) (t : ↑(Set.Icc 0 T)) (κ s : ℝ) (x : EulerSmoothLimit.Space) (θ : ℝ) : mean N κ (↑t) a (s, x, θ) = mean N κ (↑t) a (s, x, 0)

theorem EulerPacketInitial.mean_zero_outside {N : ℕ} (t κ s : ℝ) (a : ℕ → EulerPacketProfileRecursion.Profile) (K : Set EulerSmoothLimit.Space) (hmean : ∀ i ≤ N, ∀ x ∉ K, ∀ (θ : ℝ), (a i).mean (t, x, θ) = 0) (x : EulerSmoothLimit.Space) (hx : x ∉ K) (θ : ℝ) : mean N κ t a (s, x, θ) = 0