Restriction of a genuine ordinary Euler evolution to an initial closed interval. The reference size of the original solution still bounds every restricted velocity.

def EulerOrdinarySobolev.Evolution.restrictTime {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (S : ℝ) (hS : 0 ≤ S) (hST : S ≤ T) : Evolution S hS

Restrict time, bundling velocity, pressureForce, velocity_continuous, pressure_continuous and the required compatibility proofs.

Equations

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

theorem EulerOrdinarySobolev.Evolution.restrictTime_velocity {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (S : ℝ) (hS : 0 ≤ S) (hST : S ≤ T) (t : ↑(Set.Icc 0 S)) : (U.restrictTime S hS hST).velocity t = U.velocity ((EulerTimeIntervalRestriction.initialInclusion T S hST) t)

theorem EulerOrdinarySobolev.Evolution.restrictTime_initial {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (S : ℝ) (hS : 0 ≤ S) (hST : S ≤ T) : (U.restrictTime S hS hST).velocity ⟨0, ⋯⟩ = U.velocity ⟨0, ⋯⟩

theorem EulerOrdinarySobolev.Evolution.restrictTime_referenceWordBound {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (S : ℝ) (hS : 0 ≤ S) (hST : S ≤ T) (t : ↑(Set.Icc 0 S)) : WordBound 4 U.referenceSize ((U.restrictTime S hS hST).velocity t)