Documentation

LeanPool.NavierStokesAndEuler.Euler.PacketSlicedAssembly

Finite packet assembly commutes with the genuine time-within/spatial jets.

def EulerPacketPointJets.SliceDifferentiable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : Set ℝ) (f : Domain → E) (z : Domain) :

Slice differentiable, given by DifferentiableWithinAt ℝ (fun t => f (t,z.2)) s z.1 ∧ DifferentiableAt ℝ (fun y => f (z.1,y)) z.2.

Equations

EulerPacketPointJets.SliceDifferentiable s f z = (DifferentiableWithinAt ℝ (fun (t : ℝ) => f (t, z.2)) s z.1 ∧ DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => f (z.1, y)) z.2)

Instances For

theorem EulerPacketPointJets.SliceDifferentiable.add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set ℝ} {f g : Domain → E} {z : Domain} (hf : SliceDifferentiable s f z) (hg : SliceDifferentiable s g z) :

SliceDifferentiable s (f + g) z

theorem EulerPacketPointJets.sliceDifferentiable_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : Set ℝ) (z : Domain) :

SliceDifferentiable s 0 z

theorem EulerPacketPointJets.joinDerivative_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (v w : E) (A B : SpatialDomain →L[ℝ ] E) :

joinDerivative (v + w) (A + B) = joinDerivative v A + joinDerivative w B

theorem EulerPacketPointJets.slicedJet_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Set ℝ} {f g : Domain → E} {z : Domain} (hf : SliceDifferentiable s f z) (hg : SliceDifferentiable s g z) :

slicedJet s (f + g) z = slicedJet s f z + slicedJet s g z

theorem EulerPacketPointJets.slicedJet_zero' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : Set ℝ) (z : Domain) :

slicedJet s 0 z = 0

theorem EulerPacketPointJets.sliceDifferentiable_truncate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : Set ℝ) (N n : ℕ) (u : ℕ → Domain → E) (z : Domain) (hu : ∀ i ≤ N, SliceDifferentiable s (u i) z) :

SliceDifferentiable s (EulerFiniteGrades.truncate N u n) z

theorem EulerPacketPointJets.slicedJet_truncate {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : Set ℝ) (N n : ℕ) (u : ℕ → Domain → E) (z : Domain) :

slicedJet s (EulerFiniteGrades.truncate N u n) z = EulerFiniteGrades.truncate N (fun (i : ℕ) => slicedJet s (u i) z) n

theorem EulerPacketPointJets.sliceDifferentiable_shiftUp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : Set ℝ) (N n : ℕ) (u : ℕ → Domain → E) (z : Domain) (hu : ∀ i ≤ N, SliceDifferentiable s (u i) z) :

SliceDifferentiable s (EulerFiniteGrades.shiftUp N u n) z

theorem EulerPacketPointJets.slicedJet_shiftUp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : Set ℝ) (N n : ℕ) (u : ℕ → Domain → E) (z : Domain) :

slicedJet s (EulerFiniteGrades.shiftUp N u n) z = EulerFiniteGrades.shiftUp N (fun (i : ℕ) => slicedJet s (u i) z) n

theorem EulerPacketPointJets.slicedJet_assemble {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : Set ℝ) (N n : ℕ) (u c : ℕ → Domain → E) (z : Domain) (hu : ∀ i ≤ N, SliceDifferentiable s (u i) z) (hc : ∀ i ≤ N, SliceDifferentiable s (c i) z) :

slicedJet s (EulerFiniteGrades.assemble N u c n) z = EulerFiniteGrades.assemble N (fun (i : ℕ) => slicedJet s (u i) z) (fun (i : ℕ) => slicedJet s (c i) z) n

theorem EulerPacketPointJets.sliceDifferentiable_assemble {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : Set ℝ) (N n : ℕ) (u c : ℕ → Domain → E) (z : Domain) (hu : ∀ i ≤ N, SliceDifferentiable s (u i) z) (hc : ∀ i ≤ N, SliceDifferentiable s (c i) z) :

SliceDifferentiable s (EulerFiniteGrades.assemble N u c n) z

theorem EulerPacketPointJets.pressureJet_zero (z : Domain) :

pressureJet 0 z = 0

theorem EulerPacketPointJets.pressureJet_add (f g : Domain → ℝ) (z : Domain) (hf : DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => f (z.1, y)) z.2) (hg : DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => g (z.1, y)) z.2) :

pressureJet (f + g) z = pressureJet f z + pressureJet g z

theorem EulerPacketPointJets.pressureJet_truncate (N n : ℕ) (u : ℕ → Domain → ℝ) (z : Domain) :

pressureJet (EulerFiniteGrades.truncate N u n) z = EulerFiniteGrades.truncate N (fun (i : ℕ) => pressureJet (u i) z) n

theorem EulerPacketPointJets.pressureJet_shiftUp (N n : ℕ) (u : ℕ → Domain → ℝ) (z : Domain) :

pressureJet (EulerFiniteGrades.shiftUp N u n) z = EulerFiniteGrades.shiftUp N (fun (i : ℕ) => pressureJet (u i) z) n

theorem EulerPacketPointJets.pressureJet_assemble (N n : ℕ) (u c : ℕ → Domain → ℝ) (z : Domain) (hu : ∀ i ≤ N, DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => u i (z.1, y)) z.2) (hc : ∀ i ≤ N, DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => c i (z.1, y)) z.2) :

pressureJet (EulerFiniteGrades.assemble N u c n) z = EulerFiniteGrades.assemble N (fun (i : ℕ) => pressureJet (u i) z) (fun (i : ℕ) => pressureJet (c i) z) n

theorem EulerPacketPointJets.spatialDifferentiable_assemble {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (N n : ℕ) (u c : ℕ → Domain → E) (z : Domain) (hu : ∀ i ≤ N, DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => u i (z.1, y)) z.2) (hc : ∀ i ≤ N, DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => c i (z.1, y)) z.2) :

DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => EulerFiniteGrades.assemble N u c n (z.1, y)) z.2