Bounds for essentially bounded functions #
The norm bound and almost-everywhere evaluation bound apply to arbitrary measures and normed additive groups. Both the half-line input API and periodic-mean examples use this shared implementation.
theorem
AbstractLinearControl.ALCS.lp_norm_le
{α : Type u_1}
{U : Type u_2}
[MeasurableSpace α]
[NormedAddCommGroup U]
{μ : MeasureTheory.Measure α}
{u : ↥(MeasureTheory.Lp U ⊤ μ)}
{C : ℝ}
(hC : 0 ≤ C)
(hb : ∀ᵐ (t : α) ∂μ, ‖↑↑u t‖ ≤ C)
:
The L^∞ norm is bounded by any nonnegative a.e. bound.
theorem
AbstractLinearControl.ALCS.ae_norm_le
{α : Type u_1}
{U : Type u_2}
[MeasurableSpace α]
[NormedAddCommGroup U]
{μ : MeasureTheory.Measure α}
(u : ↥(MeasureTheory.Lp U ⊤ μ))
:
The representative of an L^∞ class obeys its norm bound a.e.