English
Equality of the uncentered covariance bilinear dual with the evaluation on dual elements.
Русский
Равенство нецентрированной ковариационной билинейной двойственной карты и оценки на двойственных элементaх.
LaTeX
$$$\\text{uncenteredCovarianceBilinDual}(μ) = \\text{bilinear map on duals}$$$
Lean4
/-- Continuous linear map from the dual to `Lp` equal to `MemLp.toLp` if `MemLp id p μ`
and to 0 otherwise. -/
noncomputable def toLp (μ : Measure E) (p : ℝ≥0∞) [Fact (1 ≤ p)] : StrongDual 𝕜 E →L[𝕜] Lp 𝕜 p μ
where
toLinearMap := StrongDual.toLpₗ μ p
cont := by
refine LinearMap.continuous_of_locally_bounded _ fun s hs ↦ ?_
rw [image_isVonNBounded_iff]
simp_rw [isVonNBounded_iff'] at hs
obtain ⟨r, hxr⟩ := hs
refine ⟨r * (eLpNorm id p μ).toReal, fun L hLs ↦ ?_⟩
specialize hxr L hLs
refine (StrongDual.norm_toLpₗ_le L).trans ?_
gcongr
