Identification after local regularity recovery

The only analytic input of this module is a local conversion of a classical Comparator solution with compact initial vorticity into an ordinary smooth Euler evolution. Restarting that conversion at times of agreement, ordinary Euler uniqueness and continuity identify the entire maximal interval.

Restriction of an ordinary Euler evolution to a translated closed interval.

def EulerOrdinarySobolev.shiftTimeMap (S T a : ℝ) (ha : 0 ≤ a) (haT : a + T ≤ S) : C(↑(Set.Icc 0 T), ↑(Set.Icc 0 S))

Embed the shifted time interval into the original evolution interval.

Equations

• EulerOrdinarySobolev.shiftTimeMap S T a ha haT = { toFun := fun (t : ↑(Set.Icc 0 T)) => ⟨a + ↑t, ⋯⟩, continuous_toFun := ⋯ }

@[simp]

theorem EulerOrdinarySobolev.shiftTimeMap_val (S T a : ℝ) (ha : 0 ≤ a) (haT : a + T ≤ S) (t : ↑(Set.Icc 0 T)) : ↑((shiftTimeMap S T a ha haT) t) = a + ↑t

def EulerOrdinarySobolev.Evolution.shiftTime {S : ℝ} {hS : 0 ≤ S} (U : Evolution S hS) (a : ℝ) (ha : 0 ≤ a) (T : ℝ) (hT : 0 ≤ T) (haT : a + T ≤ S) : Evolution T hT

Restart an evolution at time a, retaining its next T units of time.

Equations

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

@[simp]

theorem EulerOrdinarySobolev.Evolution.shiftTime_velocity {S : ℝ} {hS : 0 ≤ S} (U : Evolution S hS) (a : ℝ) (ha : 0 ≤ a) (T : ℝ) (hT : 0 ≤ T) (haT : a + T ≤ S) (t : ↑(Set.Icc 0 T)) : (U.shiftTime a ha T hT haT).velocity t = U.velocity ((shiftTimeMap S T a ha haT) t)

@[simp]

theorem EulerOrdinarySobolev.Evolution.shiftTime_pressureForce {S : ℝ} {hS : 0 ≤ S} (U : Evolution S hS) (a : ℝ) (ha : 0 ≤ a) (T : ℝ) (hT : 0 ≤ T) (haT : a + T ≤ S) (t : ↑(Set.Icc 0 T)) : (U.shiftTime a ha T hT haT).pressureForce t = U.pressureForce ((shiftTimeMap S T a ha haT) t)

theorem EulerOrdinarySobolev.Evolution.shiftTime_initial {S : ℝ} {hS : 0 ≤ S} (U : Evolution S hS) (a : ℝ) (ha : 0 ≤ a) (T : ℝ) (hT : 0 ≤ T) (haT : a + T ≤ S) : (U.shiftTime a ha T hT haT).velocity ⟨0, ⋯⟩ = U.velocity ⟨a, ⋯⟩

Time translation preserves the independent whole-space Euler class, including its one-sided initial-time equation and uniform energy bound.

theorem Euler.EulerExistenceAndSmoothnessR3.shiftTime {u₀ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)} {v : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)} {p : EuclideanSpace ℝ (Fin 3) → ℝ → ℝ} (h : EulerExistenceAndSmoothnessR3 u₀ v p) (a : ℝ) (ha : 0 ≤ a) : EulerExistenceAndSmoothnessR3 (fun (x : EuclideanSpace ℝ (Fin 3)) => v x a) (fun (x : EuclideanSpace ℝ (Fin 3)) (t : ℝ) => v x (a + t)) fun (x : EuclideanSpace ℝ (Fin 3)) (t : ℝ) => p x (a + t)

def Euler.ComparatorBridge.HasLocalEvolutionAtCompactCurl (v : EulerSmoothLimit.Space → ℝ → EulerSmoothLimit.Space) : Prop

Local recovery is needed only at compact-vorticity slices. It asks for an actual ordinary evolution representing the given velocity, so it contains no comparison or uniqueness conclusion.

Equations

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

def Euler.ComparatorBridge.CompactCurlLocalUpgrade : Prop

The reusable analytic conversion obligation, before any uniqueness argument: compact initial vorticity gives a short ordinary realization.

Equations

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

theorem Euler.ComparatorBridge.hasLocalEvolutionAtCompactCurl_of_upgrade {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} {v : EulerSmoothLimit.Space → ℝ → EulerSmoothLimit.Space} {p : EulerSmoothLimit.Space → ℝ → ℝ} (h : EulerExistenceAndSmoothnessR3 A.field v p) (hupgrade : CompactCurlLocalUpgrade) : HasLocalEvolutionAtCompactCurl v

theorem Euler.ComparatorBridge.evolution_field_eq_of_local_evolution {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} {v : EulerSmoothLimit.Space → ℝ → EulerSmoothLimit.Space} {p : EulerSmoothLimit.Space → ℝ → ℝ} {S : ℝ} {hS : 0 ≤ S} (U : EulerOrdinarySobolev.Evolution S hS) (h : EulerExistenceAndSmoothnessR3 A.field v p) (hU : U.velocity ⟨0, ⋯⟩ = A) (hcompact : ∀ (t : ↑(Set.Icc 0 S)), HasCompactSupport (EulerMeanCutoffCurl.vectorCurl (U.velocity t).field)) (hlocal : HasLocalEvolutionAtCompactCurl v) (t : ↑(Set.Icc 0 S)) : (U.velocity t).field = fun (x : EulerSmoothLimit.Space) => v x ↑t

A classical field locally recoverable as an ordinary evolution agrees with every ordinary evolution from the same data whose vorticity stays compact.