Time regularity from the projected weak equation

Uniform bounds for the genuine spatial Sobolev norms upgrade strong L² continuity to continuity of every spatial jet. This is the interpolation step in the Comparator bridge. In particular, its higher Sobolev continuity conclusion is not assumed in any of its hypotheses.

Upgrading an equation tested against a dense set

These Hilbert-space lemmas separate the time regularity argument from the PDE. Uniform bounds for scalar derivatives against dense test vectors imply strong Lipschitz continuity. Only scalar continuity is required at the time endpoints. Likewise, an integral equation on dense tests determines the vector-valued integral equation and hence its strong derivative when the right-hand side is continuous.

theorem Euler.WeakHilbertODE.norm_le_of_dense_inner_bound {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {D : Set H} (hD : Dense D) {z : H} {C : ℝ} (hC : 0 ≤ C) (hbound : ∀ φ ∈ D, ‖inner ℝ φ z‖ ≤ C * ‖φ‖) : ‖z‖ ≤ C

A norm bound tested on a dense subset is a norm bound in the Hilbert space.

theorem Euler.WeakHilbertODE.eq_of_dense_inner_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {D : Set H} (hD : Dense D) {x y : H} (heq : ∀ φ ∈ D, inner ℝ φ x = inner ℝ φ y) : x = y

Dense scalar testing determines a vector uniquely.

theorem Euler.WeakHilbertODE.lipschitzOnWith_of_dense_scalar_derivative {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {D : Set H} (hD : Dense D) {u : ℝ → H} {a c : ℝ} (hac : a < c) (C : NNReal) (hcont : ∀ φ ∈ D, ContinuousOn (fun (t : ℝ) => inner ℝ φ (u t)) (Set.Icc a c)) (hderiv : ∀ φ ∈ D, ∀ t ∈ Set.Ioo a c, ∃ (d : ℝ), HasDerivAt (fun (s : ℝ) => inner ℝ φ (u s)) d t ∧ ‖d‖ ≤ ↑C * ‖φ‖) : LipschitzOnWith C u (Set.Icc a c)

Bounded scalar derivatives on the open interval give a strong Lipschitz bound on the closed interval. No strong continuity of the path is assumed.

theorem Euler.WeakHilbertODE.continuousOn_of_dense_scalar_derivative {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {D : Set H} (hD : Dense D) {u : ℝ → H} {a c : ℝ} (hac : a < c) (C : NNReal) (hcont : ∀ φ ∈ D, ContinuousOn (fun (t : ℝ) => inner ℝ φ (u t)) (Set.Icc a c)) (hderiv : ∀ φ ∈ D, ∀ t ∈ Set.Ioo a c, ∃ (d : ℝ), HasDerivAt (fun (s : ℝ) => inner ℝ φ (u s)) d t ∧ ‖d‖ ≤ ↑C * ‖φ‖) : ContinuousOn u (Set.Icc a c)

Strong continuity follows from weak scalar equations with uniformly bounded derivatives, including at the endpoints.

theorem Euler.WeakHilbertODE.lipschitzOnWith_of_dense_weak_equation {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {D : Set H} (hD : Dense D) {u b : ℝ → H} {a c : ℝ} (hac : a < c) (C : NNReal) (hcont : ∀ φ ∈ D, ContinuousOn (fun (t : ℝ) => inner ℝ φ (u t)) (Set.Icc a c)) (hderiv : ∀ φ ∈ D, ∀ t ∈ Set.Ioo a c, HasDerivAt (fun (s : ℝ) => inner ℝ φ (u s)) (inner ℝ φ (b t)) t) (hbound : ∀ t ∈ Set.Ioo a c, ‖b t‖ ≤ ↑C) : LipschitzOnWith C u (Set.Icc a c)

A bounded vector right-hand side provides the scalar derivative bounds.

theorem Euler.WeakHilbertODE.sub_eq_integral_of_dense_pairing {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {D : Set H} (hD : Dense D) {u b : ℝ → H} {a t : ℝ} (hb : IntervalIntegrable b MeasureTheory.volume a t) (hweak : ∀ φ ∈ D, inner ℝ φ (u t) - inner ℝ φ (u a) = ∫ (s : ℝ) in a..t, inner ℝ φ (b s)) : u t - u a = ∫ (s : ℝ) in a..t, b s

Dense scalar integral identities imply the vector integral identity.

theorem Euler.WeakHilbertODE.continuousOn_of_dense_integral_equation {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {D : Set H} (hD : Dense D) {u b : ℝ → H} {a c : ℝ} (hb : IntervalIntegrable b MeasureTheory.volume a c) (hweak : ∀ t ∈ Set.Icc a c, ∀ φ ∈ D, inner ℝ φ (u t) - inner ℝ φ (u a) = ∫ (s : ℝ) in a..t, inner ℝ φ (b s)) : ContinuousOn u (Set.Icc a c)

Scalar integral identities supply strong continuity without a prior strong measurability or continuity assumption on the path itself.

theorem Euler.WeakHilbertODE.hasDerivWithinAt_of_dense_integral_equation {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {D : Set H} (hD : Dense D) {u b : ℝ → H} {a c t : ℝ} (hb : ContinuousOn b (Set.Icc a c)) (ht : t ∈ Set.Icc a c) (hweak : ∀ s ∈ Set.Icc a c, ∀ φ ∈ D, inner ℝ φ (u s) - inner ℝ φ (u a) = ∫ (r : ℝ) in a..s, inner ℝ φ (b r)) : HasDerivWithinAt u (b t) (Set.Icc a c) t

Continuous right-hand sides give a strong derivative of a path satisfying the integral equation on dense tests, including one-sided endpoint derivatives.

theorem Euler.WeakHilbertODE.sub_eq_integral_of_dense_weak_equation {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {D : Set H} (hD : Dense D) {u b : ℝ → H} {a c t : ℝ} (hu : ∀ φ ∈ D, ContinuousOn (fun (s : ℝ) => inner ℝ φ (u s)) (Set.Icc a c)) (hb : ContinuousOn b (Set.Icc a c)) (hderiv : ∀ φ ∈ D, ∀ s ∈ Set.Ioo a c, HasDerivAt (fun (r : ℝ) => inner ℝ φ (u r)) (inner ℝ φ (b s)) s) (ht : t ∈ Set.Icc a c) : u t - u a = ∫ (s : ℝ) in a..t, b s

Weak derivatives against a dense set and continuity of the vector right-hand side imply the exact vector integral equation.

theorem Euler.WeakHilbertODE.hasDerivWithinAt_of_dense_weak_equation {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {D : Set H} (hD : Dense D) {u b : ℝ → H} {a c t : ℝ} (hu : ∀ φ ∈ D, ContinuousOn (fun (s : ℝ) => inner ℝ φ (u s)) (Set.Icc a c)) (hb : ContinuousOn b (Set.Icc a c)) (hderiv : ∀ φ ∈ D, ∀ s ∈ Set.Ioo a c, HasDerivAt (fun (r : ℝ) => inner ℝ φ (u r)) (inner ℝ φ (b s)) s) (ht : t ∈ Set.Icc a c) : HasDerivWithinAt u (b t) (Set.Icc a c) t

A weak Hilbert-space ODE with a continuous right-hand side is a strong ODE. It is enough to test on a dense set; the path need not be known to be strongly continuous or strongly measurable beforehand.

theorem Euler.WeakHilbertODE.hasDerivAt_of_dense_weak_equation {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {D : Set H} (hD : Dense D) {u b : ℝ → H} {a c t : ℝ} (hu : ∀ φ ∈ D, ContinuousOn (fun (s : ℝ) => inner ℝ φ (u s)) (Set.Icc a c)) (hb : ContinuousOn b (Set.Icc a c)) (hderiv : ∀ φ ∈ D, ∀ s ∈ Set.Ioo a c, HasDerivAt (fun (r : ℝ) => inner ℝ φ (u r)) (inner ℝ φ (b s)) s) (ht : t ∈ Set.Ioo a c) : HasDerivAt u (b t) t

Interior-point form of the strong derivative supplied by the weak ODE.

theorem Euler.ComparatorBridge.comparator_weak_pairings_continuous {u₀ : EulerSmoothLimit.Space → EulerSmoothLimit.Space} {v : EulerSmoothLimit.Space → ℝ → EulerSmoothLimit.Space} {p : EulerSmoothLimit.Space → ℝ → ℝ} (h : EulerExistenceAndSmoothnessR3 u₀ v p) {T : ℝ} (A : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (t : ↑(Set.Icc 0 T)), (A t).field = fun (x : EulerSmoothLimit.Space) => v x ↑t) (φ : ↥EulerMeanSolenoidal.L2) : Continuous fun (t : ↑(Set.Icc 0 T)) => inner ℝ φ (A t).toLp

A recovered smooth-L² representative inherits the Comparator's weak time continuity. No continuity of its higher derivatives is used here.

theorem Euler.ComparatorBridge.comparator_velocity_mem_solenoidal {u₀ : EulerSmoothLimit.Space → EulerSmoothLimit.Space} {v : EulerSmoothLimit.Space → ℝ → EulerSmoothLimit.Space} {p : EulerSmoothLimit.Space → ℝ → ℝ} (h : EulerExistenceAndSmoothnessR3 u₀ v p) {T : ℝ} (A : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (t : ↑(Set.Icc 0 T)), (A t).field = fun (x : EulerSmoothLimit.Space) => v x ↑t) (t : ↑(Set.Icc 0 T)) : (A t).toLp ∈ EulerMeanSolenoidal.solenoidalSpace

The Comparator's classical divergence constraint gives the genuine Hilbert-space solenoidal constraint on every recovered velocity slice.

theorem Euler.ComparatorBridge.tensorNorm_fieldSub_le (A B : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (q : ℕ) : EulerOrdinarySobolev.tensorNorm q (EulerOrdinarySobolev.fieldSub A B) ≤ EulerOrdinarySobolev.tensorNorm q A + EulerOrdinarySobolev.tensorNorm q B

The actual tensor Sobolev norm of a difference is controlled by the sum of the two actual norms.

theorem Euler.ComparatorBridge.jetLp_norm_le_tensorNorm (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (q : ℕ) : ‖A.jetLp q‖ ≤ EulerOrdinarySobolev.tensorNorm q A

A fixed jet is bounded by the finite tensor norm containing it.

theorem Euler.ComparatorBridge.tensorNorm_uniform_of_jetLp_uniform {K : Type u_1} (A : K → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hb : ∀ (n : ℕ), ∃ (M : ℝ), ∀ (t : K), ‖(A t).jetLp n‖ ≤ M) (q : ℕ) : ∃ (M : ℝ), ∀ (t : K), EulerOrdinarySobolev.tensorNorm q (A t) ≤ M

Per-order jet bounds give the finite tensor bounds used below.

theorem Euler.ComparatorBridge.jetLp_continuous_of_toLp_continuous {K : Type u_1} [TopologicalSpace K] (A : K → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (h0 : Continuous fun (t : K) => (A t).toLp) (hb : ∀ (q : ℕ), ∃ (M : ℝ), ∀ (t : K), EulerOrdinarySobolev.tensorNorm q (A t) ≤ M) (q : ℕ) : Continuous fun (t : K) => (A t).jetLp q

Strong L² continuity plus uniform higher spatial Sobolev bounds implies continuity of every actual spatial L² jet.

theorem Euler.ComparatorBridge.projectedRhs_norm_le_of_tensorNorm_le (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (M : ℝ) (hM : EulerOrdinarySobolev.tensorNorm 2 A ≤ M) : ‖(EulerOrdinarySobolev.projectedRhs A).toLp‖ ≤ 39 * EulerSmoothSobolev.smoothEmbeddingConstant * M ^ 2

A bounded spatial H² norm bounds the projected Euler right-hand side in L². This estimate does not use time regularity.

theorem Euler.ComparatorBridge.projectedRhs_uniform_bound {K : Type u_1} (A : K → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hb : ∃ (M : ℝ), ∀ (t : K), EulerOrdinarySobolev.tensorNorm 2 (A t) ≤ M) : ∃ (C : NNReal), ∀ (t : K), ‖(EulerOrdinarySobolev.projectedRhs (A t)).toLp‖ ≤ ↑C

Uniform spatial bounds supply a uniform bound for the projected right-hand side even before strong time continuity has been established.

theorem Euler.ComparatorBridge.isSmoothScalarEuler_of_weak_projectedEquation {T : ℝ} (hT : 0 < T) (A : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hs : ∀ (t : ↑(Set.Icc 0 T)), (A t).toLp ∈ EulerMeanSolenoidal.solenoidalSpace) (hb : ∀ (q : ℕ), ∃ (M : ℝ), ∀ (t : ↑(Set.Icc 0 T)), EulerOrdinarySobolev.tensorNorm q (A t) ≤ M) (D : Set ↥EulerMeanSolenoidal.solenoidalSpace) (hD : Dense D) (hc : ∀ φ ∈ D, Continuous fun (t : ↑(Set.Icc 0 T)) => inner ℝ (↑φ) (A t).toLp) (hd : ∀ φ ∈ D, ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T), HasDerivAt (fun (r : ℝ) => inner ℝ (↑φ) (A (Set.projIcc 0 T ⋯ r)).toLp) (inner ℝ (↑φ) (EulerOrdinarySobolev.projectedRhs (A ⟨t, ⋯⟩)).toLp) t) : EulerOrdinarySobolev.IsSmoothScalarEuler A

A projected Euler equation tested against a dense family is enough to recover the development's full scalar-pressure class. The hypotheses require only weak time continuity and uniform spatial bounds; both strong L² time regularity and continuity of every higher spatial Sobolev norm are proved.