E Lp Norm const average le

theorem eLpNorm_const_average_le    {α : Type*} [MeasurableSpace α] {μ : Measure α} [IsFiniteMeasure μ]    {p : ℝ≥0∞} (hp : 1 ≤ p) (hp_top : p ≠ ⊤)    {f : α → ℝ} (hf : Integrable f μ) :    eLpNorm (fun _ => ⨍ x, f x ∂μ) p μ ≤ eLpNorm f p μ := by  let _ := hp_top  -- Trivial case: μ = 0  rcases eq_or_ne μ 0 with rfl | hμ  · simp [eLpNorm_measure_zero]  have hμ_ne : μ Set.univ ≠ 0 := by rwa [ne_eq, Measure.measure_univ_eq_zero]  have hμ_top : μ Set.univ ≠ ⊤ := measure_ne_top μ _  have hp_ne : p ≠ 0 := (lt_of_lt_of_le one_pos hp).ne'  -- Proof: ‖⨍ f‖ ≤ (μ.real univ)⁻¹ * ‖∫ f‖ ≤ (μ.real univ)⁻¹ * (eLpNorm f 1 μ).toReal  -- Then convert to ENNReal.  have h_avg_enorm_le :      ‖⨍ x, f x ∂μ‖ₑ ≤ (μ Set.univ)⁻¹ * eLpNorm f 1 μ := by    have h_avg_bound : ‖⨍ x, f x ∂μ‖ ≤        (μ.real Set.univ)⁻¹ * (eLpNorm f 1 μ).toReal := by      simp only [average_eq]      calc ‖(μ.real Set.univ)⁻¹ • ∫ x, f x ∂μ‖          ≤ ‖(μ.real Set.univ)⁻¹‖ * ‖∫ x, f x ∂μ‖ := norm_smul_le _ _        _ = (μ.real Set.univ)⁻¹ * ‖∫ x, f x ∂μ‖ := by            rw [Real.norm_of_nonneg (inv_nonneg.mpr measureReal_nonneg)]        _ ≤ (μ.real Set.univ)⁻¹ * (eLpNorm f 1 μ).toReal := by            gcongr            calc ‖∫ x, f x ∂μ‖                ≤ ∫ x, ‖f x‖ ∂μ := norm_integral_le_integral_norm _              _ = (∫⁻ x, ‖f x‖ₑ ∂μ).toReal :=                  integral_norm_eq_lintegral_enorm hf.aestronglyMeasurable              _ = (eLpNorm f 1 μ).toReal := by rw [eLpNorm_one_eq_lintegral_enorm]    -- Convert ℝ bound to ENNReal    have h_inv_eq : ENNReal.ofReal (μ.real Set.univ)⁻¹ = (μ Set.univ)⁻¹ := by      rw [measureReal_def, ENNReal.ofReal_inv_of_pos (ENNReal.toReal_pos hμ_ne hμ_top),        ENNReal.ofReal_toReal hμ_top]    calc ‖⨍ x, f x ∂μ‖ₑ        ≤ ENNReal.ofReal ((μ.real Set.univ)⁻¹ * (eLpNorm f 1 μ).toReal) := by          simp only [Real.enorm_eq_ofReal_abs, ← Real.norm_eq_abs]          exact ENNReal.ofReal_le_ofReal h_avg_bound      _ = ENNReal.ofReal (μ.real Set.univ)⁻¹ * ENNReal.ofReal (eLpNorm f 1 μ).toReal :=          ENNReal.ofReal_mul (inv_nonneg.mpr measureReal_nonneg)      _ ≤ (μ Set.univ)⁻¹ * eLpNorm f 1 μ := by          rw [h_inv_eq]; gcongr; exact ENNReal.ofReal_toReal_le  set exp := 1 / (1 : ℝ≥0∞).toReal - 1 / p.toReal with hexp_def  have h_holder : eLpNorm f 1 μ ≤      eLpNorm f p μ * μ Set.univ ^ exp :=    eLpNorm_le_eLpNorm_mul_rpow_measure_univ hp hf.aestronglyMeasurable  -- eLpNorm(const c) = ‖c‖ₑ * μ(univ)^{1/p}  [eLpNorm_const]  -- ≤ (μ univ)⁻¹ * eLpNorm f p μ * μ(univ)^exp * μ(univ)^{1/p}  -- = eLpNorm f p μ * ((μ univ)⁻¹ * μ(univ)^{exp + 1/p})  -- Since exp + 1/p = 1/1 - 1/p + 1/p = 1: = eLpNorm f p μ * (μ univ)⁻¹ * μ univ = eLpNorm f p μ  have hexp_simp : exp + 1 / p.toReal = 1 := by    simp [hexp_def, show (1 : ℝ≥0∞).toReal = 1 from ENNReal.toReal_one]  calc eLpNorm (fun _ => ⨍ x, f x ∂μ) p μ      = ‖⨍ x, f x ∂μ‖ₑ * μ Set.univ ^ (1 / p.toReal) := eLpNorm_const _ hp_ne hμ    _ ≤ ((μ Set.univ)⁻¹ * eLpNorm f 1 μ) * μ Set.univ ^ (1 / p.toReal) := by        gcongr    _ ≤ ((μ Set.univ)⁻¹ * (eLpNorm f p μ * μ Set.univ ^ exp)) *          μ Set.univ ^ (1 / p.toReal) := by gcongr    _ = eLpNorm f p μ * ((μ Set.univ)⁻¹ * (μ Set.univ ^ exp *          μ Set.univ ^ (1 / p.toReal))) := by ring    _ = eLpNorm f p μ * ((μ Set.univ)⁻¹ * μ Set.univ ^ (exp + 1 / p.toReal)) := by        congr 2; exact (ENNReal.rpow_add exp (1 / p.toReal) hμ_ne hμ_top).symm    _ = eLpNorm f p μ * ((μ Set.univ)⁻¹ * μ Set.univ ^ (1 : ℝ)) := by        rw [hexp_simp]    _ = eLpNorm f p μ * ((μ Set.univ)⁻¹ * μ Set.univ) := by        rw [ENNReal.rpow_one]    _ = eLpNorm f p μ := by rw [ENNReal.inv_mul_cancel hμ_ne hμ_top, mul_one]