Documentation

LeanPool.NavierStokesAndEuler.Euler.ParentPacketParity

Oddness of the actual displacement propagates to its true velocity and acceleration, fixes the origin, and gives every even source coefficient used by the packet. The genuine child flow preserves it.

Spatial derivatives and genuine within-time derivatives preserve the expected parity, including the closed interval's endpoints.

theorem SmoothTimeField.fderiv_even_of_odd {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (f : E → V) (hf : ContDiff ℝ (↑⊤) f) (ho : Function.Odd f) :

Function.Even (fderiv ℝ f)

theorem SmoothTimeField.TimeDerivative.odd {E V : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {T : ℝ} {hT : 0 ≤ T} {A A1 : SmoothTimeField (↑(Set.Icc 0 T)) E V} (hd : TimeDerivative T hT A A1) (hTpos : 0 < T) (ho : ∀ (t : ↑(Set.Icc 0 T)), Function.Odd ⇑(A.field t)) (t : ↑(Set.Icc 0 T)) :

Function.Odd ⇑(A1.field t)

theorem EulerGraphInvariantFlow.physicalCoefficient_odd (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (T : ℝ) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (ell : ℝ) (ho : ∀ (t : ↑(Set.Icc 0 T)), Function.Odd ⇑(A.field t)) (t : ↑(Set.Icc 0 T)) :

Function.Odd ⇑((physicalCoefficient k m T A ell).field t)

structure EulerParentPacketFrames.OddData (A : Parent) :

Odd data, collecting displacement.

displacement (t : ↑(Set.Icc 0 A.T)) : Function.Odd ⇑(A.displacement.field t)

Instances For

theorem EulerParentPacketFrames.OddData.velocity {A : Parent} (O : OddData A) (t : ↑(Set.Icc 0 A.T)) :

Function.Odd ⇑(A.velocity.field t)

theorem EulerParentPacketFrames.OddData.acceleration {A : Parent} (O : OddData A) (t : ↑(Set.Icc 0 A.T)) :

Function.Odd ⇑(A.acceleration.field t)

theorem EulerParentPacketFrames.OddData.position_odd {A : Parent} (O : OddData A) (t : ↑(Set.Icc 0 A.T)) :

Function.Odd (A.position t)

theorem EulerParentPacketFrames.OddData.position_zero {A : Parent} (O : OddData A) (t : ↑(Set.Icc 0 A.T)) :

A.position t 0 = 0

theorem EulerParentPacketFrames.OddData.frame_even {A : Parent} (O : OddData A) (t : ↑(Set.Icc 0 A.T)) :

Function.Even ⇑(A.frame.field t)

theorem EulerParentPacketFrames.OddData.first_even {A : Parent} (O : OddData A) (t : ↑(Set.Icc 0 A.T)) :

Function.Even ⇑(A.first.field t)

theorem EulerParentPacketFrames.OddData.second_even {A : Parent} (O : OddData A) (t : ↑(Set.Icc 0 A.T)) :

Function.Even ⇑(A.second.field t)

theorem EulerParentPacketFrames.OddData.inverse_even {A : Parent} (O : OddData A) (t : ↑(Set.Icc 0 A.T)) :

Function.Even ⇑(A.inverse.field t)

theorem EulerParentPacketFrames.OddData.strain_even {A : Parent} (O : OddData A) (t : ↑(Set.Icc 0 A.T)) :

Function.Even ⇑(A.strain.field t)

theorem EulerParentPacketFrames.OddData.curvature_even {A : Parent} (O : OddData A) (t : ↑(Set.Icc 0 A.T)) :

Function.Even ⇑(A.curvature.field t)

theorem EulerParentPacketFrames.OddData.initialStrain_even {A : Parent} (O : OddData A) :

Function.Even ⇑A.initialStrain.field

theorem EulerParentPacketFrames.OddData.meanEvenData {A : Parent} (O : OddData A) (H : LowBounds A) :

EulerMeanPacketProvider.EvenData (A.meanData H)

theorem EulerParentPacketFrames.OddData.restrictTime {A : Parent} (O : OddData A) (S : ℝ) (hS : 0 < S) (hST : S ≤ A.T) :

OddData (A.restrictTime S hS hST)

theorem EulerParentPacketFrames.OddData.child {A : Parent} (O : OddData A) {P : ℝ} [Fact (0 < P)] (G : EulerPhysicalGraphFlowBounds.Data P A.T) (ho : ∀ (t : ↑(Set.Icc 0 A.T)), Function.Odd ⇑(G.A.field t)) (k : ℝ) (m : EulerSmoothLimit.Space) (hgraph : ∀ (t : ↑(Set.Icc 0 A.T)) (z : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) z) = 0) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) :

OddData (A.child G k m hgraph nextEll hnext hnext1)

theorem EulerParentPacketFrames.ParticleInverse.odd {A : Parent} (I : ParticleInverse A) (O : OddData A) (t : ↑(Set.Icc 0 A.T)) :

Function.Odd (I.field t)

theorem EulerParentPacketFrames.ParticleInverse.zero {A : Parent} (I : ParticleInverse A) (O : OddData A) (t : ↑(Set.Icc 0 A.T)) :

I.field t 0 = 0