Integrability of the Hopf–Lax value #
For the cost L w = ‖w‖ ^ p with 0 < p and a bounded initial datum, the Hopf–Lax value at a
positive time is bounded and upper semicontinuous, hence measurable, and so integrable against a
finite measure.
Main results #
TauCeti.integrable_hopfLax_norm_rpow: for the cost‖w‖ ^ pwith0 < p, in a real seminormed space, the Hopf–Lax value of a bounded function at a positive time is integrable against a finite measure.
theorem
TauCeti.integrable_hopfLax_norm_rpow
{E : Type u_1}
[SeminormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[OpensMeasurableSpace E]
{p : ℝ}
(hp : 0 < p)
{g : E → ℝ}
{C : ℝ}
(hgC : ∀ (x : E), |g x| ≤ C)
{s : ℝ}
(hs : 0 < s)
(μ : MeasureTheory.Measure E)
[MeasureTheory.IsFiniteMeasure μ]
:
MeasureTheory.Integrable (fun (x : E) => hopfLax (fun (x : E) => ‖x‖ ^ p) g s x) μ
For the cost L w = ‖w‖ ^ p with 0 < p, in a real seminormed space, the Hopf–Lax value of a
bounded function at a positive time is integrable against a finite measure.