Exact infinite upper limits at the maximal time. The endpoint filter is the pullback of the ordinary left-neighborhood filter, so its meaning does not depend on a chosen sequence of sampling times.

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

Endpoint filter, given by Filter.comap (fun t : L.Time => (t : ℝ)) (𝓝[<] L.duration).

Equations

• L.endpointFilter = Filter.comap (fun (t : L.Time) => ↑t) (nhdsWithin L.duration (Set.Iio L.duration))

theorem EulerOrdinarySobolev.FiniteLifespan.endpointFilter_eq_atTop {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) : L.endpointFilter = Filter.atTop

theorem EulerOrdinarySobolev.FiniteLifespan.map_time_atTop {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) : Filter.map (fun (t : L.Time) => ↑t) Filter.atTop = nhdsWithin L.duration (Set.Iio L.duration)

theorem EulerOrdinarySobolev.FiniteLifespan.endpointFilter_neBot {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) : L.endpointFilter.NeBot

theorem EulerOrdinarySobolev.FiniteLifespan.time_tendsto_endpoint {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) : Filter.Tendsto (fun (t : L.Time) => ↑t) Filter.atTop (nhdsWithin L.duration (Set.Iio L.duration))

theorem EulerOrdinarySobolev.FiniteLifespan.ofReal_limsup_eq_top_of_unbounded {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) (f : L.Time → ℝ) (hf : ∀ τ < L.duration, ∀ (K : ℝ), ∃ (t : L.Time), τ < ↑t ∧ K < f t) : Filter.limsup (fun (t : L.Time) => ENNReal.ofReal (f t)) L.endpointFilter = ⊤

Arbitrarily large values in every terminal interval force the actual extended nonnegative upper limit to be infinity.

theorem EulerOrdinarySobolev.FiniteLifespan.maximalGradientNorm_limsup {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) : Filter.limsup (fun (t : L.Time) => ENNReal.ofReal (L.maximalGradientNorm t)) L.endpointFilter = ⊤

theorem EulerOrdinarySobolev.FiniteLifespan.maximalC1Norm_limsup {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) : Filter.limsup (fun (t : L.Time) => ENNReal.ofReal (L.maximalC1Norm t)) L.endpointFilter = ⊤

theorem EulerOrdinarySobolev.FiniteLifespan.maximalC1Norm_limsup_atTop {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} (L : FiniteLifespan A) : Filter.limsup (fun (t : L.Time) => ENNReal.ofReal (L.maximalC1Norm t)) Filter.atTop = ⊤

theorem EulerPacketInduction.maximalTime_map_atTop : Filter.map (fun (t : MaximalTime) => ↑t) Filter.atTop = nhdsWithin lifespan.duration (Set.Iio lifespan.duration)

theorem EulerPacketInduction.maximalGradientNorm_limsup : Filter.limsup (fun (t : MaximalTime) => ENNReal.ofReal (maximalGradientNorm t)) (Filter.comap (fun (t : MaximalTime) => ↑t) (nhdsWithin lifespan.duration (Set.Iio lifespan.duration))) = ⊤

theorem EulerPacketInduction.maximalC1Norm_limsup : Filter.limsup (fun (t : MaximalTime) => ENNReal.ofReal (maximalC1Norm t)) (Filter.comap (fun (t : MaximalTime) => ↑t) (nhdsWithin lifespan.duration (Set.Iio lifespan.duration))) = ⊤