Related estimates used together by the same construction modules.

The genuine Piola constraint for every generated source high/corrector pair.

Exact angular mean and raw corrector identities for the constructed source profiles.

theorem EulerPacketCylinderField.source_high_mean_zero (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) (I Iprimary : EulerTransversePacketProvider.InitialData P D) (p : ℕ) (t : ℝ) (x : EulerSmoothLimit.Space) : ∫ (θ : ℝ) in 0..P, (sourceProfiles P M D I Iprimary p).high (t, x, θ) = 0

theorem EulerPacketCylinderField.source_corrector_eq (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (I Iprimary : EulerTransversePacketProvider.InitialData P D) (p : ℕ) (hp : 1 ≤ p) : (sourceProfiles P M D I Iprimary p).corrector = D.curlCorrector P (sourceProfiles P M D I Iprimary p).high

theorem EulerPacketCylinderField.Field.changeTime_apply {P T T' : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (h : T = T') (t : ↑(Set.Icc 0 T)) : (G.changeTime h).path ⟨↑t, ⋯⟩ = G.path t

def EulerPacketCylinderField.sourceTime (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) (t : ↑(Set.Icc 0 M.T)) : ↑(Set.Icc 0 D.T)

Source time, given by ⟨t,by rw [← hT]; exact t.property⟩.

Equations

• EulerPacketCylinderField.sourceTime M D hT t = ⟨↑t, ⋯⟩

noncomputable def EulerPacketCylinderField.sourcePairField (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) (I Iprimary : EulerTransversePacketProvider.InitialData P D) (κ : ℝ) (p : ℕ) : Field P M.T fun (z : EulerPacketPointJets.Domain) => ((sourceOperators P M D I).inverseFrame z) (κ ^ p • (sourceProfiles P M D I Iprimary p).high z + κ ^ (p + 1) • (sourceProfiles P M D I Iprimary p).corrector z)

Source pair field used in packet source piola.

Equations

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

theorem EulerPacketCylinderField.sourcePairField_mem (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (hT : M.T = D.T) (I Iprimary : EulerTransversePacketProvider.InitialData P D) (κ : ℝ) (p : ℕ) (hp : 1 ≤ p) (t : ↑(Set.Icc 0 M.T)) (Ξ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hΞ : ContDiff ℝ (↑⊤) Ξ) (hF : ∀ (x : EulerSmoothLimit.Space), fderiv ℝ Ξ x = (D.F.field (sourceTime M D hT t)) x) (hdet : ∀ (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field (sourceTime M D hT t)) x)) = 1) : (sourcePairField P M D hT I Iprimary κ p).path t ∈ EulerLiftedGradientSpace.divergenceFreeSpace P κ D.m₀

The literal packet sums and their genuine first derivatives match the graded assembly.

theorem EulerPacketPointJets.jet_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (z : Domain) : jet (fun (x : Domain) => 0) z = 0

theorem EulerPacketPointJets.jet_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f g : Domain → E) (z : Domain) (hf : DifferentiableAt ℝ f z) (hg : DifferentiableAt ℝ g z) : jet (f + g) z = jet f z + jet g z

theorem EulerPacketPointJets.jet_truncate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (N n : ℕ) (u : ℕ → Domain → E) (z : Domain) : jet (EulerFiniteGrades.truncate N u n) z = EulerFiniteGrades.truncate N (fun (i : ℕ) => jet (u i) z) n

theorem EulerPacketPointJets.jet_shiftUp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (N n : ℕ) (u : ℕ → Domain → E) (z : Domain) : jet (EulerFiniteGrades.shiftUp N u n) z = EulerFiniteGrades.shiftUp N (fun (i : ℕ) => jet (u i) z) n

theorem EulerPacketPointJets.differentiableAt_truncate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (N n : ℕ) (u : ℕ → Domain → E) (z : Domain) (hu : ∀ i ≤ N, DifferentiableAt ℝ (u i) z) : DifferentiableAt ℝ (EulerFiniteGrades.truncate N u n) z

theorem EulerPacketPointJets.differentiableAt_shiftUp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (N n : ℕ) (u : ℕ → Domain → E) (z : Domain) (hu : ∀ i ≤ N, DifferentiableAt ℝ (u i) z) : DifferentiableAt ℝ (EulerFiniteGrades.shiftUp N u n) z

theorem EulerPacketPointJets.jet_assemble {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (N n : ℕ) (u c : ℕ → Domain → E) (z : Domain) (hu : ∀ i ≤ N, DifferentiableAt ℝ (u i) z) (hc : ∀ i ≤ N, DifferentiableAt ℝ (c i) z) : jet (EulerFiniteGrades.assemble N u c n) z = EulerFiniteGrades.assemble N (fun (i : ℕ) => jet (u i) z) (fun (i : ℕ) => jet (c i) z) n

theorem EulerPacketPointJets.differentiableAt_assemble {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (N n : ℕ) (u c : ℕ → Domain → E) (z : Domain) (hu : ∀ i ≤ N, DifferentiableAt ℝ (u i) z) (hc : ∀ i ≤ N, DifferentiableAt ℝ (c i) z) : DifferentiableAt ℝ (EulerFiniteGrades.assemble N u c n) z

theorem EulerPacketPointJets.fieldSum_assemble_from_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (N : ℕ) (κ : ℝ) (u c : ℕ → Domain → E) (hu : u 0 = 0) (hc : c 0 = 0) (z : Domain) : fieldSum (N + 1) κ (EulerFiniteGrades.assemble N u c) z = ∑ i ∈ Finset.range N, (κ ^ (i + 1) • u (i + 1) z + κ ^ (i + 2) • c (i + 1) z)

The extra degree N+1 is precisely the final divergence corrector in (13).