One actual Euler field on the half-open maximal interval. Values are chosen on intermediate horizons, and genuine Euler uniqueness removes the dependence on that choice. No continuation criterion is assumed.

@[reducible, inline]

abbrev EulerOrdinarySobolev.FiniteLifespan.Time {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) : Type

Time: an abbreviation for Ico (0 : ℝ) L.duration.

Equations

• L.Time = ↑(Set.Ico 0 L.duration)

def EulerOrdinarySobolev.FiniteLifespan.initialTime {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) : L.Time

Initial time, given by ⟨0,le_rfl,L.duration_pos⟩.

Equations

• L.initialTime = ⟨0, ⋯⟩

noncomputable def EulerOrdinarySobolev.FiniteLifespan.intermediateHorizon {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (t : L.Time) : ℝ

Intermediate horizon, given by ((t : ℝ)+L.duration)/2.

Equations

• L.intermediateHorizon t = (↑t + L.duration) / 2

theorem EulerOrdinarySobolev.FiniteLifespan.intermediateHorizon_pos {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (t : L.Time) : 0 < L.intermediateHorizon t

theorem EulerOrdinarySobolev.FiniteLifespan.time_lt_intermediateHorizon {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (t : L.Time) : ↑t < L.intermediateHorizon t

theorem EulerOrdinarySobolev.FiniteLifespan.intermediateHorizon_lt {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (t : L.Time) : L.intermediateHorizon t < L.duration

def EulerOrdinarySobolev.FiniteLifespan.intermediateTime {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (t : L.Time) : ↑(Set.Icc 0 (L.intermediateHorizon t))

Intermediate time, given by ⟨t,t.property.1,(L.time_lt_intermediateHorizon t).le⟩.

Equations

• L.intermediateTime t = ⟨↑t, ⋯⟩

def EulerOrdinarySobolev.FiniteLifespan.shorterTime {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (S : ℝ) (hSL : S < L.duration) (t : ↑(Set.Icc 0 S)) : L.Time

Shorter time, given by ⟨t,t.property.1,t.property.2.trans_lt hSL⟩.

Equations

• L.shorterTime S hSL t = ⟨↑t, ⋯⟩

noncomputable def EulerOrdinarySobolev.FiniteLifespan.maximalField {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (t : L.Time) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Maximal field, given by (L.evolution (L.intermediateHorizon t) (L.intermediateHorizon_pos t) (L.intermediateHorizon_lt t)).velocity (L.intermediateTime t).

Equations

• L.maximalField t = (L.evolution (L.intermediateHorizon t) ⋯ ⋯).velocity (L.intermediateTime t)

noncomputable def EulerOrdinarySobolev.FiniteLifespan.maximalPressureField {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (t : L.Time) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Maximal pressure field as an element of SmoothL2Field Space.

Equations

• L.maximalPressureField t = (L.evolution (L.intermediateHorizon t) ⋯ ⋯).pressureForce (L.intermediateTime t)

theorem EulerOrdinarySobolev.FiniteLifespan.maximalFields_eq_evolution {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (S : ℝ) (hS : 0 < S) (hSL : S < L.duration) (t : ↑(Set.Icc 0 S)) : L.maximalField (L.shorterTime S hSL t) = (L.evolution S hS hSL).velocity t ∧ L.maximalPressureField (L.shorterTime S hSL t) = (L.evolution S hS hSL).pressureForce t

theorem EulerOrdinarySobolev.FiniteLifespan.maximalField_eq_evolution {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (S : ℝ) (hS : 0 < S) (hSL : S < L.duration) (t : ↑(Set.Icc 0 S)) : L.maximalField (L.shorterTime S hSL t) = (L.evolution S hS hSL).velocity t

theorem EulerOrdinarySobolev.FiniteLifespan.maximalPressureField_eq_evolution {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (S : ℝ) (hS : 0 < S) (hSL : S < L.duration) (t : ↑(Set.Icc 0 S)) : L.maximalPressureField (L.shorterTime S hSL t) = (L.evolution S hS hSL).pressureForce t

theorem EulerOrdinarySobolev.FiniteLifespan.continuous_of_shorter_restrictions {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) {E : Type u_1} [TopologicalSpace E] (f : L.Time → E) (hf : ∀ (S : ℝ), 0 < S → ∀ (hSL : S < L.duration), Continuous fun (t : ↑(Set.Icc 0 S)) => f (L.shorterTime S hSL t)) : Continuous f

Continuous restrictions on all shorter initial intervals determine a continuous curve on the actual half-open lifespan.

theorem EulerOrdinarySobolev.FiniteLifespan.maximalField_jet_continuous {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (n : ℕ) : Continuous fun (t : L.Time) => (L.maximalField t).jetLp n

theorem EulerOrdinarySobolev.FiniteLifespan.maximalPressureField_jet_continuous {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (n : ℕ) : Continuous fun (t : L.Time) => (L.maximalPressureField t).jetLp n

theorem EulerOrdinarySobolev.FiniteLifespan.maximalField_initial {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) : L.maximalField L.initialTime = A

theorem EulerOrdinarySobolev.FiniteLifespan.maximalField_solenoidal {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (t : L.Time) : (L.maximalField t).toLp ∈ EulerMeanSolenoidal.solenoidalSpace

theorem EulerOrdinarySobolev.FiniteLifespan.maximalPressureField_gradient {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (t : L.Time) : (L.maximalPressureField t).toLp ∈ EulerMeanSolenoidal.gradientSpace

noncomputable def EulerOrdinarySobolev.FiniteLifespan.maximalVelocity {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (t : L.Time) : EulerSmoothLimit.Space → EulerSmoothLimit.Space

Maximal velocity, given by (L.maximalField t).field.

Equations

• L.maximalVelocity t = (L.maximalField t).field

noncomputable def EulerOrdinarySobolev.FiniteLifespan.maximalPressure {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (t : L.Time) : EulerSmoothLimit.Space → ℝ

Maximal pressure, given by EulerCanonicalGraphPotential.radialPotential (L.maximalPressureField t).field.

Equations

• L.maximalPressure t = EulerCanonicalGraphPotential.radialPotential (L.maximalPressureField t).field

theorem EulerOrdinarySobolev.FiniteLifespan.maximalVelocity_eq_evolution {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (S : ℝ) (hS : 0 < S) (hSL : S < L.duration) (t : ↑(Set.Icc 0 S)) : L.maximalVelocity (L.shorterTime S hSL t) = ((L.evolution S hS hSL).velocity t).field

theorem EulerOrdinarySobolev.FiniteLifespan.maximalPressure_eq_evolution {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (S : ℝ) (hS : 0 < S) (hSL : S < L.duration) (t : ↑(Set.Icc 0 S)) : L.maximalPressure (L.shorterTime S hSL t) = (L.evolution S hS hSL).scalarPressure t

theorem EulerOrdinarySobolev.FiniteLifespan.maximalVelocity_initial {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) : L.maximalVelocity L.initialTime = A.field

theorem EulerOrdinarySobolev.FiniteLifespan.maximalVelocity_smooth {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (t : L.Time) : ContDiff ℝ (↑⊤) (L.maximalVelocity t)

theorem EulerOrdinarySobolev.FiniteLifespan.maximalVelocity_joint_continuous {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) : Continuous fun (z : L.Time × EulerSmoothLimit.Space) => L.maximalVelocity z.1 z.2

theorem EulerOrdinarySobolev.FiniteLifespan.maximalPressureField_joint_continuous {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) : Continuous fun (z : L.Time × EulerSmoothLimit.Space) => (L.maximalPressureField z.1).field z.2

theorem EulerOrdinarySobolev.FiniteLifespan.maximalVelocity_divergence {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (t : L.Time) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.divergence (L.maximalVelocity t) x = 0

theorem EulerOrdinarySobolev.FiniteLifespan.maximalPressure_spec {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (t : L.Time) : ContDiff ℝ (↑⊤) (L.maximalPressure t) ∧ L.maximalPressure t 0 = 0 ∧ ∀ (x : EulerSmoothLimit.Space), gradient (L.maximalPressure t) x = (L.maximalPressureField t).field x

theorem EulerOrdinarySobolev.FiniteLifespan.maximal_restriction_is_evolution {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (S : ℝ) (hS : 0 < S) (hSL : S < L.duration) : ∃ (U : Evolution S ⋯), (U.velocity = fun (t : ↑(Set.Icc 0 S)) => L.maximalField (L.shorterTime S hSL t)) ∧ (U.pressureForce = fun (t : ↑(Set.Icc 0 S)) => L.maximalPressureField (L.shorterTime S hSL t)) ∧ U.velocity ⟨0, ⋯⟩ = A

Every compact initial subinterval is exactly an actual Euler evolution, with both its velocity and its pressure force equal to the maximal fields.

theorem EulerOrdinarySobolev.FiniteLifespan.maximalVelocity_time_law {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (S : ℝ) (hS : 0 < S) (hSL : S < L.duration) (t : ℝ) (ht : t ∈ Set.Ioo 0 S) (x : EulerSmoothLimit.Space) : HasDerivAt (fun (r : ℝ) => L.maximalVelocity (L.shorterTime S hSL (Set.projIcc 0 S ⋯ r)) x) (-(fderiv ℝ (L.maximalVelocity (L.shorterTime S hSL ⟨t, ⋯⟩)) x) (L.maximalVelocity (L.shorterTime S hSL ⟨t, ⋯⟩) x) - gradient (L.maximalPressure (L.shorterTime S hSL ⟨t, ⋯⟩)) x) t