MeasureTheory.lintegral_lintegral_pow_swap

lemma lintegral_lintegral_pow_swap {α : Type u_1} {β : Type u_3} {p : ℝ} (hp : 1 ≤ p)    [MeasurableSpace α] [MeasurableSpace β]    {μ : Measure α} {ν : Measure β} [SFinite ν]    [SigmaFinite μ] ⦃f : α → β → ENNReal⦄    (hf : AEMeasurable (Function.uncurry f) (μ.prod ν)) :    (∫⁻ (x : α), (∫⁻ (y : β), f x y ∂ν) ^ p ∂μ) ^ p⁻¹ ≤    ∫⁻ (y : β), (∫⁻ (x : α), (f x y) ^ p ∂μ) ^ p⁻¹ ∂ν := by  rcases Decidable.lt_or_eq_of_le hp with one_lt_p | one_eq_p  · let q := Real.conjExponent p    have hpq' : p.HolderConjugate q := Real.HolderConjugate.conjExponent one_lt_p    have one_lt_q : 1 < q := (Real.HolderConjugate.symm hpq').lt    have ineq : ∀ g ∈ {g' : α → ℝ≥0∞ | AEMeasurable g' μ ∧ ∫⁻ (z : α), (g' z) ^ q ∂μ ≤ 1},        ∫⁻ x : α, (∫⁻ y : β, f x y ∂ν) * g x ∂μ ≤        ∫⁻ (y : β), (∫⁻ (x : α), f x y ^ p ∂μ) ^ p⁻¹ ∂ν := by      intro g ⟨hg1, hg2⟩      have ae_meas₁ : ∀ᵐ x : α ∂μ, AEMeasurable (f x) ν :=        aemeasurability_prod₁ (f := Function.uncurry f) hf      calc      _ = ∫⁻ x : α, (∫⁻ y : β, f x y * g x ∂ν) ∂μ := by        apply lintegral_congr_ae        filter_upwards [ae_meas₁] with a ha using (lintegral_mul_const'' _ ha).symm      _ = ∫⁻ y : β, (∫⁻ x : α, f x y * g x ∂μ) ∂ν := lintegral_lintegral_swap (hf.mul hg1.comp_fst)      _ ≤ ∫⁻ (y : β), (∫⁻ (x : α), f x y ^ p ∂μ) ^ p⁻¹ ∂ν := by        apply lintegral_mono_ae        filter_upwards [aemeasurability_prod₂ hf] with y hy        calc        _ ≤ (∫⁻ (x : α), f x y ^ p ∂μ) ^ (1 / p) * (∫⁻ (x : α), g x ^ q ∂μ) ^ (1 / q) :=          ENNReal.lintegral_mul_le_Lp_mul_Lq μ hpq' hy hg1        _ ≤ (∫⁻ (x : α), f x y ^ p ∂μ) ^ (1 / p) * 1 ^ (1 / q) := by          gcongr        _ = (∫⁻ (x : α), f x y ^ p ∂μ) ^ p⁻¹ := by          simp [one_div]    nth_rw 1 [← one_div]    rw [representationLp (hp := one_lt_p) (hq := one_lt_q.le) (hpq := hpq'.inv_add_inv_eq_one)]    · exact (iSup_le fun g ↦ iSup_le fun hg ↦ ineq g hg)    · exact (aemeasurable_integral_component hf)  · rw [← one_eq_p]    simp only [ENNReal.rpow_one, inv_one]    exact (lintegral_lintegral_swap hf).le