Nemytskii operators: RealIso

Adapted from madvorak/nemytskii-lebesgue (Apache-2.0).

noncomputable def NemytskiiLebesgue.realLIE : ℝ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin 1)

The canonical real linear isometry to one-dimensional Euclidean space.

Equations

• NemytskiiLebesgue.realLIE = { toLinearEquiv := (LinearEquiv.funUnique (Fin 1) ℝ ℝ).symm ≪≫ₗ (WithLp.linearEquiv 2 ℝ (Fin 1 → ℝ)).symm, norm_map' := NemytskiiLebesgue.realLIE._proof_3 }

theorem NemytskiiLebesgue.norm_realLIE (r : ℝ) : ‖realLIE r‖ = |r|

theorem NemytskiiLebesgue.realLIE_mul (c s : ℝ) : realLIE (c * s) = c • realLIE s

theorem NemytskiiLebesgue.normSMulSelf_realLIE {T : Type} (t : T) (s : ℝ) : normSMulSelf t (realLIE s) = realLIE (|s| * s)

theorem NemytskiiLebesgue.eLpNorm_realLIE {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {p : ENNReal} (u : Ω → ℝ) : MeasureTheory.eLpNorm (fun (ω : Ω) => realLIE (u ω)) p μ = MeasureTheory.eLpNorm u p μ

theorem NemytskiiLebesgue.memLp_realLIE {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {p : ENNReal} {u : Ω → ℝ} (hu : MeasureTheory.MemLp u p μ) : MeasureTheory.MemLp (fun (ω : Ω) => realLIE (u ω)) p μ