The genuine time/amplitude symmetry of ordinary Euler, including restriction to a shorter closed time interval.

def EulerOrdinarySobolev.scaleTimeMap (S T c : ℝ) (hc : 0 ≤ c) (hct : c * T ≤ S) : C(↑(Set.Icc 0 T), ↑(Set.Icc 0 S))

Scale time map, bundling toFun, continuous_toFun.

Equations

• EulerOrdinarySobolev.scaleTimeMap S T c hc hct = { toFun := fun (t : ↑(Set.Icc 0 T)) => ⟨c * ↑t, ⋯⟩, continuous_toFun := ⋯ }

@[simp]

theorem EulerOrdinarySobolev.scaleTimeMap_val (S T c : ℝ) (hc : 0 ≤ c) (hct : c * T ≤ S) (t : ↑(Set.Icc 0 T)) : ↑((scaleTimeMap S T c hc hct) t) = c * ↑t

noncomputable def EulerOrdinarySobolev.Evolution.rescale {S : ℝ} {hS : 0 ≤ S} (U : Evolution S hS) (T : ℝ) (hT : 0 ≤ T) (c : ℝ) (hc : 0 < c) (hct : c * T ≤ S) : Evolution T hT

Rescale, 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.

@[simp]

theorem EulerOrdinarySobolev.Evolution.rescale_velocity {S : ℝ} {hS : 0 ≤ S} (U : Evolution S hS) (T : ℝ) (hT : 0 ≤ T) (c : ℝ) (hc : 0 < c) (hct : c * T ≤ S) (t : ↑(Set.Icc 0 T)) : (U.rescale T hT c hc hct).velocity t = scaleField c (U.velocity ((scaleTimeMap S T c ⋯ hct) t))

theorem EulerOrdinarySobolev.Evolution.rescale_initial {S : ℝ} {hS : 0 ≤ S} (U : Evolution S hS) (T : ℝ) (hT : 0 ≤ T) (c : ℝ) (hc : 0 < c) (hct : c * T ≤ S) : (U.rescale T hT c hc hct).velocity ⟨0, ⋯⟩ = scaleField c (U.velocity ⟨0, ⋯⟩)