Weak time continuity in L²

A Comparator solution is jointly smooth on the closed nonnegative time half-space. Consequently its pairings with continuous compactly supported test fields vary continuously, including at time zero. The uniform energy bound and density of compactly supported continuous functions extend this to all L² test fields. No spatial derivative integrability or energy conservation assumption is used here.

theorem Euler.EulerExistenceAndSmoothnessR3.velocity_test_pairing_continuousOn {u₀ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)} {v : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)} {p : EuclideanSpace ℝ (Fin 3) → ℝ → ℝ} (h : EulerExistenceAndSmoothnessR3 u₀ v p) (φ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) (hφ : Continuous φ) (hφc : HasCompactSupport φ) : ContinuousOn (fun (t : ℝ) => ∫ (x : EuclideanSpace ℝ (Fin 3)), inner ℝ (φ x) (v x t)) (Set.Ici 0)

Pairing the velocity with a continuous compactly supported test field is continuous on the entire nonnegative time interval.

noncomputable def Euler.EulerExistenceAndSmoothnessR3.velocityLp {u₀ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)} {v : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)} {p : EuclideanSpace ℝ (Fin 3) → ℝ → ℝ} (h : EulerExistenceAndSmoothnessR3 u₀ v p) (t : ↑(Set.Ici 0)) : ↥(MeasureTheory.Lp (EuclideanSpace ℝ (Fin 3)) 2 MeasureTheory.volume)

The natural velocity path in the Hilbert space L².

Equations

• h.velocityLp t = MeasureTheory.MemLp.toLp (fun (x : EuclideanSpace ℝ (Fin 3)) => v x ↑t) ⋯

theorem Euler.EulerExistenceAndSmoothnessR3.velocityLp_norm_sq {u₀ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)} {v : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)} {p : EuclideanSpace ℝ (Fin 3) → ℝ → ℝ} (h : EulerExistenceAndSmoothnessR3 u₀ v p) (t : ↑(Set.Ici 0)) : ‖h.velocityLp t‖ ^ 2 = ∫ (x : EuclideanSpace ℝ (Fin 3)), ‖v x ↑t‖ ^ 2

theorem Euler.EulerExistenceAndSmoothnessR3.velocityLp_norm_bounded {u₀ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)} {v : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)} {p : EuclideanSpace ℝ (Fin 3) → ℝ → ℝ} (h : EulerExistenceAndSmoothnessR3 u₀ v p) : ∃ (M : ℝ), 0 < M ∧ ∀ (t : ↑(Set.Ici 0)), ‖h.velocityLp t‖ ≤ M

The Comparator energy condition gives a uniform Hilbert space norm bound.

theorem Euler.EulerExistenceAndSmoothnessR3.velocityLp_weakly_continuous {u₀ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)} {v : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)} {p : EuclideanSpace ℝ (Fin 3) → ℝ → ℝ} (h : EulerExistenceAndSmoothnessR3 u₀ v p) (φ : ↥(MeasureTheory.Lp (EuclideanSpace ℝ (Fin 3)) 2 MeasureTheory.volume)) : Continuous fun (t : ↑(Set.Ici 0)) => inner ℝ φ (h.velocityLp t)

Every L² test pairing is continuous. This is weak time continuity of the velocity in L², derived from the exact Comparator hypotheses.

theorem Euler.EulerExistenceAndSmoothnessR3.velocity_pairing_continuousOn {u₀ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)} {v : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)} {p : EuclideanSpace ℝ (Fin 3) → ℝ → ℝ} (h : EulerExistenceAndSmoothnessR3 u₀ v p) (φ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) (hφ : MeasureTheory.MemLp φ 2 MeasureTheory.volume) : ContinuousOn (fun (t : ℝ) => ∫ (x : EuclideanSpace ℝ (Fin 3)), inner ℝ (φ x) (v x t)) (Set.Ici 0)

Function-level form of weak L² continuity, without quotient representatives.

theorem Euler.EulerExistenceAndSmoothnessR3.velocity_pairing_tendsto_initial {u₀ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)} {v : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)} {p : EuclideanSpace ℝ (Fin 3) → ℝ → ℝ} (h : EulerExistenceAndSmoothnessR3 u₀ v p) (φ : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)) (hφ : MeasureTheory.MemLp φ 2 MeasureTheory.volume) : Filter.Tendsto (fun (t : ℝ) => ∫ (x : EuclideanSpace ℝ (Fin 3)), inner ℝ (φ x) (v x t)) (nhdsWithin 0 (Set.Ici 0)) (nhds (∫ (x : EuclideanSpace ℝ (Fin 3)), inner ℝ (φ x) (u₀ x)))

Every finite-energy test pairing attains the prescribed initial data weakly.