Nemytskii operators: Nemytskii #
Adapted from madvorak/nemytskii-lebesgue (Apache-2.0).
theorem
NemytskiiLebesgue.IsCaratheodory.monotone_integral
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{E : Type u_2}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
{f : Ω → E → E}
(hf : IsCaratheodory f μ)
{p q : ℝ}
(hpq : p.HolderConjugate q)
{a : Ω → ℝ}
(haq : MeasureTheory.MemLp a (ENNReal.ofReal q) μ)
{C : ℝ}
(hC : 0 ≤ C)
(hfaCpq : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : E), ‖f ω ξ‖ ≤ |a ω| + C * ‖ξ‖ ^ (p / q))
(hf0 : ∀ᵐ (ω : Ω) ∂μ, ∀ (s t : E), inner ℝ (f ω s - f ω t) (s - t) ≥ 0)
{u : Ω → E}
(hup : MeasureTheory.MemLp u (ENNReal.ofReal p) μ)
{v : Ω → E}
(hvp : MeasureTheory.MemLp v (ENNReal.ofReal p) μ)
:
theorem
NemytskiiLebesgue.IsCaratheodory.monotone_integral_real
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
{f : Ω → ℝ → ℝ}
(hf : IsCaratheodory f μ)
{p q : ℝ}
(hpq : p.HolderConjugate q)
{a : Ω → ℝ}
(haq : MeasureTheory.MemLp a (ENNReal.ofReal q) μ)
{C : ℝ}
(hC : 0 ≤ C)
(hfaCpq : ∀ᵐ (ω : Ω) ∂μ, ∀ (ξ : ℝ), |f ω ξ| ≤ |a ω| + C * |ξ| ^ (p / q))
(hf0 : ∀ᵐ (ω : Ω) ∂μ, ∀ (s t : ℝ), (f ω s - f ω t) * (s - t) ≥ 0)
{u : Ω → ℝ}
(hup : MeasureTheory.MemLp u (ENNReal.ofReal p) μ)
{v : Ω → ℝ}
(hvp : MeasureTheory.MemLp v (ENNReal.ofReal p) μ)
: