MeasureTheory.representationLp

lemma representationLp {μ : Measure α} [SigmaFinite μ] {f : α → ℝ≥0∞}    (hf : AEMeasurable f μ) {p q : ℝ} (hp : p > 1) (hq : q ≥ 1)    (hpq : p⁻¹ + q⁻¹ = 1) :    (∫⁻ x : α, (f x) ^ p ∂μ) ^ (1 / p) =    ⨆ g ∈ {g' : α → ℝ≥0∞ | AEMeasurable g' μ ∧ ∫⁻ x : α, (g' x) ^ q ∂μ ≤ 1},    ∫⁻ x : α, (f x) * g x ∂μ := by  let A := spanningSets μ  let g := truncCut f μ  have hpq' : p.HolderConjugate q := Real.holderConjugate_iff.mpr ⟨hp, hpq⟩  have f_mul : ∀ n : ℕ, (g n) ^ p ≤ f * (g n) ^ (p - 1) := by    intro n x    simp only [g, Pi.pow_apply, Pi.mul_apply, truncCut, indicator]    split_ifs    · refine le_trans (b := (min (f x) ↑n) * min (f x) ↑n ^ (p - 1)) ?_ ?_      · nth_rewrite 1 [← add_sub_cancel 1 p]        rw [rpow_add_of_pos, ENNReal.rpow_one] <;> try linarith      · exact mul_le_mul_left (min_le_left (f x) ↑n) (min (f x) ↑n ^ (p - 1))    · rw [ENNReal.zero_rpow_of_pos] <;> positivity  have g_lim : ∀ x : α, Filter.Tendsto (fun n ↦ g n x) Filter.atTop (nhds (f x)) := by    intro x    apply tendsto_atTop_isLUB (truncCut_mono _)    exact isLUB_iff_sSup_eq.mpr (truncCut_sup _)  have g_sup' : (fun x ↦ ⨆ n : ℕ, (g n x) ^ p) = fun x ↦ (f x) ^ p := by    ext x    apply iSup_eq_of_tendsto    · intro m n hmn      dsimp only      gcongr      exact truncCut_mono _ hmn    · exact (g_lim x).ennrpow_const p  have g_meas (n : ℕ): AEMeasurable (g n) μ := by    exact AEMeasurable.indicator (by fun_prop) (measurableSet_spanningSets μ n)  have g_fin (n : ℕ): ∫⁻ (z : α), g n z ^ p ∂μ < ⊤ := by    calc    _ = ∫⁻ (z : α) in A n, g n z ^ p ∂μ := by      unfold g truncCut      rw [← lintegral_indicator]; swap; · exact measurableSet_spanningSets μ n      congr 1      ext x      dsimp only [indicator]      split_ifs      · rfl      · simp only [ENNReal.rpow_eq_zero_iff, true_and, zero_ne_top, false_and, or_false]; positivity    _ ≤ ∫⁻ (_x : α) in A n, n ^ p ∂μ := by      apply setLIntegral_mono measurable_const      · intro x hx        gcongr        unfold g truncCut indicator        split_ifs        · exact min_le_right (f x) ↑n        · contradiction    _ = n ^ p * μ (A n) := setLIntegral_const (A n) (↑n ^ p)    _ < ⊤ := by finiteness [measure_spanningSets_lt_top μ n]  have obs (n : ℕ) :∫⁻ x : α, (f x) * ((g n x) ^ (p - 1) /      (∫⁻ y : α, ((g n y) ^ (p - 1)) ^ q ∂μ) ^ q⁻¹) ∂μ ≥      (∫⁻ x : α, (g n x) ^ p ∂μ) ^ p⁻¹ := by    obtain (int_eq_zero | int_ne_zero) := eq_or_ne (∫⁻ x : α, (g n x) ^ p ∂μ) 0    · rw [int_eq_zero, ENNReal.zero_rpow_of_pos]      · exact zero_le      · exact inv_pos_of_pos (by positivity)    · calc      _ = (∫⁻ x : α, (f x) * (g n x) ^ (p - 1) ∂μ) * (          (∫⁻ y : α, ((g n y) ^ (p - 1)) ^ q ∂μ) ^ q⁻¹)⁻¹ := by        simp_rw [div_eq_mul_inv, ← mul_assoc]        rw [lintegral_mul_const'' _ (by fun_prop)]      _ ≥ (∫⁻ x : α, (g n x) ^ (p) ∂μ) * ((∫⁻ y : α, ((g n y) ^ (p - 1)) ^ q ∂μ) ^ q⁻¹)⁻¹ := by        gcongr        apply f_mul      _ = (∫⁻ x : α, (g n x) ^ (p) ∂μ) * ((∫⁻ y : α, (g n y) ^ p ∂μ) ^ q⁻¹)⁻¹ := by        congr        ext x        rw [← ENNReal.rpow_mul]        congr        exact Real.HolderConjugate.sub_one_mul_conj hpq'      _ = (∫⁻ x : α, (g n x) ^ p ∂μ) ^ p⁻¹ := by        rw [← ENNReal.rpow_neg]        nth_rw 1 [← ENNReal.rpow_one (x := (∫⁻ x : α, (g n x) ^ (p) ∂μ))]        rw [← ENNReal.rpow_add _ _ int_ne_zero (g_fin n).ne]        congr        exact add_neg_eq_of_eq_add hpq.symm  have int_fg : ∫⁻ (x : α), f x ^ p ∂μ = ⨆ n : ℕ, ∫⁻ x : α, g n x ^ p ∂μ := by    rw [← g_sup']    apply lintegral_iSup' (fun n ↦ by fun_prop) (ae_of_all _ fun x m n hmn ↦ ?_)    dsimp only    gcongr    exact truncCut_mono _ hmn  have sup_rpow : (⨆ n : ℕ, ∫⁻ x : α, g n x ^ p ∂μ) ^ (1 / p) =      ⨆ n : ℕ, (∫⁻ x : α, g n x ^ p ∂μ) ^ (1 / p) := by    apply Monotone.map_iSup_of_continuousAt (f := fun (x : ℝ≥0∞) ↦ x ^ (1 / p))    · fun_prop    · apply ENNReal.monotone_rpow_of_nonneg (by positivity)    · simp; positivity  let h := fun n : ℕ ↦ (fun x ↦ g n x ^ (p - 1) / (∫⁻ y : α, ((g n y) ^ (p - 1)) ^ q ∂μ) ^ q⁻¹)  have comp_sup : (⨆ n : ℕ, ∫⁻ (x : α), f x * h n x ∂μ) ≤      ⨆ g ∈ {g' : α → ℝ≥0∞ | AEMeasurable g' μ ∧ ∫⁻ (z : α), (g' z) ^ q ∂μ ≤ 1},      ∫⁻ (x : α), f x * g x ∂μ := by    nth_rw 1 [← iSup_range (f := fun n : ℕ ↦ h n) (g := fun r ↦ ∫⁻ x : α, f x * r x ∂μ)]    apply iSup_le_iSup_of_subset fun r exists_n ↦ ?_    rcases exists_n with ⟨n, wn⟩    simp_rw [← wn]    unfold h    refine ⟨by fun_prop, ?_⟩    simp_rw [div_eq_mul_inv]    calc    _ = ∫⁻ (z : α), ((g n z ^ (p - 1)) ^ q) *        ((∫⁻ (y : α), (g n y ^ (p - 1)) ^ q ∂μ) ^ q⁻¹)⁻¹ ^ q ∂μ := by      congr 1      ext z      rw [ENNReal.mul_rpow_of_nonneg]      linarith    _ = (∫⁻ (z : α), ((g n z ^ (p - 1)) ^ q) ∂μ) *        ((∫⁻ (y : α), (g n y ^ (p - 1)) ^ q ∂μ) ^ q⁻¹)⁻¹ ^ q := by      rw [lintegral_mul_const'' _ (by fun_prop)]    _ ≤ _ := by      rcases eq_or_ne (∫⁻ x : α, ((g n x) ^ (p - 1)) ^ q ∂μ) 0 with int_eq_zero | int_ne_zero      · rw [int_eq_zero]        simp      · rw [ENNReal.inv_rpow, ENNReal.rpow_inv_rpow]        · apply le_of_eq          refine ENNReal.mul_inv_cancel int_ne_zero ?inr.a.ht          · apply ne_of_lt            calc            _ = ∫⁻ (z : α), g n z ^ p ∂μ := by              congr 1              ext z              rw [← ENNReal.rpow_mul]              congr              exact Real.HolderConjugate.sub_one_mul_conj hpq'            _ < ⊤ := g_fin n        · linarith  apply eq_of_le_of_le  · rw [int_fg, sup_rpow]    calc    _ ≤ ⨆ n : ℕ, ∫⁻ x : α, (f x) * ((g n x) ^ (p - 1) /        (∫⁻ y : α, ((g n y) ^ (p - 1)) ^ q ∂μ) ^ q⁻¹) ∂μ := by      gcongr      rw [one_div]      apply obs    _ ≤ _ := comp_sup  · refine iSup_le fun r ↦ iSup_le fun hr ↦ ?_    calc    _ ≤ (∫⁻ x : α, f x ^ p ∂μ) ^ (1 / p) * (∫⁻ x : α, r x ^ q ∂μ) ^ (1 / q) :=      ENNReal.lintegral_mul_le_Lp_mul_Lq _ hpq' hf hr.1    _ ≤ (∫⁻ x : α, f x ^ p ∂μ) ^ (1 / p) * (1) ^ (1 / q) := by      gcongr      exact hr.2    _ = _ := by simp