MeasureTheory.lintegral_lintegral_pow_swap_truncCompl

lemma lintegral_lintegral_pow_swap_truncCompl {q q₀ p₀ : ℝ}    [TopologicalSpace E₁] [ESeminormedAddMonoid E₁]    {j : Bool} {hμ : SigmaFinite (μ.restrict (fun x ↦ ‖f x‖ₑ).support)}    (hp₀ : 0 < p₀) (hp₀q₀ : p₀ ≤ q₀)    (hf : AEStronglyMeasurable f μ) (tc : ToneCouple) :    ∫⁻ (s : ℝ) in Ioi 0,        (∫⁻ (a : α) in (fun x ↦ ‖f x‖ₑ).support, ENNReal.ofReal (s ^ (q - q₀ - 1)) ^ (p₀⁻¹ * q₀)⁻¹ *        ‖trnc j f (tc.ton (ENNReal.ofReal s)) a‖ₑ ^ p₀ ∂μ) ^ (p₀⁻¹ * q₀) ≤    (∫⁻ a : α in (fun x ↦ ‖f x‖ₑ).support,      (∫⁻ (s : ℝ) in Ioi 0,        (ENNReal.ofReal (s ^ (q - q₀ - 1)) ^ (p₀⁻¹ * q₀)⁻¹ *        ‖trnc j f (tc.ton (ENNReal.ofReal s)) a‖ₑ ^ p₀) ^ (p₀⁻¹ * q₀)) ^ (p₀⁻¹ * q₀)⁻¹ ∂μ) ^ (p₀⁻¹ * q₀) := by  apply lintegral_lintegral_pow_swap_rpow  · apply le_of_mul_le_mul_left _ hp₀    field_simp    exact hp₀q₀  · unfold Function.uncurry    -- TODO: this is quite some effort, somehow the infrastructure may need to be better    apply AEMeasurable.mul    · fun_prop    · have : (fun a ↦ ‖trnc j f (tc.ton (ENNReal.ofReal a.1)) a.2‖ₑ ^ p₀) =          (fun a ↦ ‖trnc j f (tc.ton a.1) a.2‖ₑ ^ p₀ ) ∘          (Prod.map (fun a ↦ ENNReal.ofReal a) (fun a ↦ a)) := by rfl      rw [this]      apply AEMeasurable.comp_aemeasurable      · rw [← Measure.map_prod_map]        · simp only [Measure.map_id']          have : Measure.map (fun a ↦ ENNReal.ofReal a) (volume.restrict (Ioi 0)) = volume.restrict (Ioi 0) := by            simp [map_restrict_Ioi_eq_restrict_Ioi]          rw [this]          fun_prop        · fun_prop        · fun_prop      · fun_prop