English
Equality in the identification of uncentered covariance bilinear dual with a bilinear map on dual spaces.
Русский
Равенство в идентификации нецентрированной ковариационной билинейной двойственной карты с билинейной отображением на двойственных пространствах.
LaTeX
$$$\\text{uncenteredCovarianceBilinDual}(μ) = \\text{bilinear map on duals}$$$
Lean4
theorem norm_toLpₗ_le [OpensMeasurableSpace E] (L : StrongDual 𝕜 E) : ‖L.toLpₗ μ p‖ ≤ ‖L‖ * (eLpNorm id p μ).toReal :=
by
by_cases h_Lp : MemLp id p μ
swap
· simp only [h_Lp, not_false_eq_true, toLpₗ_of_not_memLp, Lp.norm_zero]
positivity
by_cases hp : p = 0
· simp only [h_Lp, toLpₗ_apply, Lp.norm_toLp]
simp [hp]
by_cases hp_top : p = ∞
· simp only [hp_top, StrongDual.toLpₗ_apply h_Lp, Lp.norm_toLp, eLpNorm_exponent_top] at h_Lp ⊢
simp only [eLpNormEssSup, id_eq]
suffices (essSup (fun x ↦ ‖L x‖ₑ) μ).toReal ≤ (essSup (fun x ↦ ‖L‖ₑ * ‖x‖ₑ) μ).toReal by
rwa [ENNReal.essSup_const_mul, ENNReal.toReal_mul, toReal_enorm] at this
gcongr
· rw [ENNReal.essSup_const_mul]
exact ENNReal.mul_ne_top (by simp) h_Lp.eLpNorm_ne_top
· exact essSup_mono_ae <| ae_of_all _ L.le_opNorm_enorm
have h0 : 0 < p.toReal := by simp [ENNReal.toReal_pos_iff, pos_iff_ne_zero, hp, Ne.lt_top hp_top]
suffices ‖L.toLpₗ μ p‖ ≤ (‖L‖ₑ ^ p.toReal * ∫⁻ x, ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹
by
refine this.trans_eq ?_
simp only [ENNReal.toReal_mul]
rw [← ENNReal.toReal_rpow, Real.mul_rpow (by positivity) (by positivity), ← Real.rpow_mul (by positivity),
mul_inv_cancel₀ h0.ne', Real.rpow_one, toReal_enorm]
rw [eLpNorm_eq_lintegral_rpow_enorm (by simp [hp]) hp_top, ENNReal.toReal_rpow]
simp
rw [StrongDual.toLpₗ_apply h_Lp, Lp.norm_toLp, eLpNorm_eq_lintegral_rpow_enorm (by simp [hp]) hp_top]
simp only [one_div]
refine ENNReal.toReal_le_of_le_ofReal (by positivity) ?_
suffices ∫⁻ x, ‖L x‖ₑ ^ p.toReal ∂μ ≤ ‖L‖ₑ ^ p.toReal * ∫⁻ x, ‖x‖ₑ ^ p.toReal ∂μ
by
rw [← ENNReal.ofReal_rpow_of_nonneg (by positivity) (by positivity)]
gcongr
rwa [ENNReal.ofReal_toReal]
refine ENNReal.mul_ne_top (by simp) ?_
have h := h_Lp.eLpNorm_ne_top
rw [eLpNorm_eq_lintegral_rpow_enorm (by simp [hp]) hp_top] at h
simpa [h0] using h
calc
∫⁻ x, ‖L x‖ₑ ^ p.toReal ∂μ
_ ≤ ∫⁻ x, ‖L‖ₑ ^ p.toReal * ‖x‖ₑ ^ p.toReal ∂μ :=
by
refine lintegral_mono fun x ↦ ?_
rw [← ENNReal.mul_rpow_of_nonneg]
swap; · positivity
gcongr
exact L.le_opNorm_enorm x
_ = ‖L‖ₑ ^ p.toReal * ∫⁻ x, ‖x‖ₑ ^ p.toReal ∂μ := by rw [lintegral_const_mul]; fun_prop
