The maximal positive horizon of a fixed ordinary Euler datum. Existence below the supremum and failure above it follow from restriction; membership of the endpoint is deliberately left to a continuation theorem.

A genuine smooth endpoint under a finite gradient integral. Shorter Euler solutions are rescaled to a common interval; the already proved smooth limit supplies the endpoint, and uniqueness identifies it with every original partial solution. No analytic radius is assumed.

noncomputable def EulerOrdinarySobolev.endpointScale (n : ℕ) : ℝ

Endpoint scale, given by 1-1/((n : ℝ)+2).

Equations

• EulerOrdinarySobolev.endpointScale n = 1 - 1 / (↑n + 2)

theorem EulerOrdinarySobolev.endpointScale_pos (n : ℕ) : 0 < endpointScale n

theorem EulerOrdinarySobolev.endpointScale_lt_one (n : ℕ) : endpointScale n < 1

theorem EulerOrdinarySobolev.endpointScale_tendsto : Filter.Tendsto endpointScale Filter.atTop (nhds 1)

theorem EulerOrdinarySobolev.exists_smooth_endpoint (T : ℝ) (hT : 0 < T) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (G : ℝ) (hpartial : ∀ (S : ℝ) (hS : 0 < S), S < T → ∃ (U : Evolution S ⋯), U.velocity ⟨0, ⋯⟩ = A ∧ ∀ (t : ↑(Set.Icc 0 S)), U.gradientIntegral t ≤ G) : ∃ (U : Evolution T ⋯), U.velocity ⟨0, ⋯⟩ = A

theorem EulerOrdinarySobolev.endpoint_matches_partial {T : ℝ} {hT : 0 ≤ T} (W : Evolution T hT) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hW : W.velocity ⟨0, ⋯⟩ = A) (S : ℝ) (hS : 0 < S) (hST : S ≤ T) (U : Evolution S ⋯) (hU : U.velocity ⟨0, ⋯⟩ = A) (t : ↑(Set.Icc 0 S)) : W.velocity ⟨↑t, ⋯⟩ = U.velocity t ∧ W.pressureForce ⟨↑t, ⋯⟩ = U.pressureForce t

theorem EulerOrdinarySobolev.exists_smooth_endpoint_extension (T : ℝ) (hT : 0 < T) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (G : ℝ) (hpartial : ∀ (S : ℝ) (hS : 0 < S), S < T → ∃ (U : Evolution S ⋯), U.velocity ⟨0, ⋯⟩ = A ∧ ∀ (t : ↑(Set.Icc 0 S)), U.gradientIntegral t ≤ G) : ∃ (W : Evolution T ⋯), W.velocity ⟨0, ⋯⟩ = A ∧ ∀ (S : ℝ) (hS : 0 < S) (hST : S ≤ T) (U : Evolution S ⋯), U.velocity ⟨0, ⋯⟩ = A → ∀ (t : ↑(Set.Icc 0 S)), W.velocity ⟨↑t, ⋯⟩ = U.velocity t ∧ W.pressureForce ⟨↑t, ⋯⟩ = U.pressureForce t

def EulerOrdinarySobolev.HasEulerEvolution (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (T : ℝ) : Prop

Has euler evolution, given by ∃ hT : 0 < T, ∃ U : Evolution T hT.le, U.velocity ⟨0,le_rfl,hT.le⟩=A.

Equations

• EulerOrdinarySobolev.HasEulerEvolution A T = ∃ (hT : 0 < T) (U : EulerOrdinarySobolev.Evolution T ⋯), U.velocity ⟨0, ⋯⟩ = A

theorem EulerOrdinarySobolev.HasEulerEvolution.restrict {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} {T : ℝ} (h : HasEulerEvolution A T) (S : ℝ) (hS : 0 < S) (hST : S ≤ T) : HasEulerEvolution A S

theorem EulerOrdinarySobolev.HasEulerEvolution.lt_of_failure {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} {T B : ℝ} (h : HasEulerEvolution A T) (hB : 0 < B) (hfail : ¬HasEulerEvolution A B) : T < B

structure EulerOrdinarySobolev.FiniteLifespan (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : Type

A compatible family of smooth solutions on every strictly shorter positive interval, with no solution on any longer interval.

• duration : ℝ

  Duration of FiniteLifespan, of type ℝ.

• duration_pos : 0 < self.duration
• shorter (S : ℝ) : 0 < S → S < self.duration → HasEulerEvolution A S
• maximal (S : ℝ) : self.duration < S → ¬HasEulerEvolution A S

theorem EulerOrdinarySobolev.exists_finite_lifespan (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (B : ℝ) (hB : 0 < B) (hlocal : ∃ (T : ℝ), HasEulerEvolution A T) (hfail : ¬HasEulerEvolution A B) : ∃ (L : FiniteLifespan A), L.duration ≤ B

noncomputable def EulerOrdinarySobolev.FiniteLifespan.evolution {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (S : ℝ) (hS : 0 < S) (hST : S < L.duration) : Evolution S ⋯

Evolution, given by (L.shorter S hS hST).choose_spec.choose.

Equations

• L.evolution S hS hST = ⋯.choose

theorem EulerOrdinarySobolev.FiniteLifespan.evolution_initial {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (S : ℝ) (hS : 0 < S) (hST : S < L.duration) : (L.evolution S hS hST).velocity ⟨0, ⋯⟩ = A

theorem EulerOrdinarySobolev.FiniteLifespan.evolution_agrees {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (S T : ℝ) (hS : 0 < S) (hT : 0 < T) (hSL : S < L.duration) (hTL : T < L.duration) (hST : S ≤ T) (t : ↑(Set.Icc 0 S)) : (L.evolution T hT hTL).velocity ⟨↑t, ⋯⟩ = (L.evolution S hS hSL).velocity t ∧ (L.evolution T hT hTL).pressureForce ⟨↑t, ⋯⟩ = (L.evolution S hS hSL).pressureForce t

theorem EulerOrdinarySobolev.FiniteLifespan.endpoint_of_bounded_gradient {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (G : ℝ) (hG : ∀ (S : ℝ) (hS : 0 < S) (hST : S < L.duration) (t : ↑(Set.Icc 0 S)), (L.evolution S hS hST).gradientIntegral t ≤ G) : HasEulerEvolution A L.duration