MeasureTheory.estimate_trnc

lemma estimate_trnc {p₀ q₀ q : ℝ} {spf : ScaledPowerFunction} {j : Bool}    [TopologicalSpace E₁] [ESeminormedAddMonoid E₁]    (hp₀ : 0 < p₀) (hq₀ : 0 < q₀) (hp₀q₀ : p₀ ≤ q₀)    (hf : AEStronglyMeasurable f μ) (hf₂ : SigmaFinite (μ.restrict (fun x ↦ ‖f x‖ₑ).support))    (hpowers : if xor j (spf_to_tc spf).mon = true then q₀ < q else q < q₀)    (hpow_pos : 0 < q₀ + spf.σ⁻¹ * (q - q₀)) :    ∫⁻ s : ℝ in Ioi 0,    eLpNorm (trnc j f ((spf_to_tc spf).ton (ENNReal.ofReal s))) (ENNReal.ofReal p₀) μ ^ q₀ *    ENNReal.ofReal (s ^ (q - q₀ - 1)) ≤    (spf.d ^ (q - q₀)) * ENNReal.ofReal |q - q₀|⁻¹ *    (∫⁻ (a : α) in (fun x ↦ ‖f x‖ₑ).support,    ‖f a‖ₑ ^ (p₀ + spf.σ⁻¹ * (q - q₀) * (p₀ / q₀)) ∂μ) ^ (p₀⁻¹ * q₀) := by  have := spf.hd  unfold eLpNorm eLpNorm'  set tc := (spf_to_tc spf).toToneCouple  split_ifs with is_p₀pos is_p₀top  · have : p₀ ≤ 0 := ofReal_eq_zero.mp is_p₀pos    contrapose! this; exact hp₀  · contrapose! is_p₀top; exact coe_ne_top  · rw [toReal_ofReal hp₀.le]    calc    _ = ∫⁻ s : ℝ in Ioi 0, ENNReal.ofReal (s ^ (q - q₀ - 1)) *    ((∫⁻ (a : α), ↑‖trnc j f ((spf_to_tc spf).ton (ENNReal.ofReal s)) a‖ₑ ^ p₀ ∂μ) ^ (1 / p₀)) ^ q₀ := by      congr 1      ext x      rw [mul_comm]    _ = ∫⁻ (s : ℝ) in Ioi 0,        (ENNReal.ofReal (s ^ (q - q₀ - 1)) ^ (p₀⁻¹ * q₀)⁻¹) ^ (p₀⁻¹ * q₀) *        (∫⁻ (a : α) in (fun x ↦ ‖f x‖ₑ).support, ↑‖trnc j f (tc.ton (ENNReal.ofReal s)) a‖ₑ ^ p₀ ∂μ) ^ (p₀⁻¹ * q₀) := by      refine setLIntegral_congr_fun measurableSet_Ioi fun s hs ↦ ?_      rw [ENNReal.rpow_inv_rpow]      · rw [one_div, ← ENNReal.rpow_mul, restrict_to_support_trnc hp₀]      · positivity    _ = ∫⁻ (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₀) := by      refine setLIntegral_congr_fun measurableSet_Ioi fun s hs ↦ ?_      rw [lintegral_const_mul', ENNReal.mul_rpow_of_nonneg]      · positivity      · exact (ENNReal.rpow_lt_top_of_nonneg (by positivity) coe_ne_top).ne    _ ≤ (∫⁻ 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      -- This is a consequence of Minkowski's integral inequality      apply lintegral_lintegral_pow_swap_truncCompl hp₀ hp₀q₀ hf tc; assumption    _ = (∫⁻ a : α in (fun x ↦ ‖f x‖ₑ).support,        (∫⁻ (s : ℝ) in Ioi 0,        (ENNReal.ofReal (s ^ (q - q₀ - 1)) *        ↑‖trnc j f (tc.ton (ENNReal.ofReal s)) a‖ₑ ^ q₀)) ^ (p₀⁻¹ * q₀)⁻¹ ∂μ) ^ (p₀⁻¹ * q₀) := by      congr 1      apply lintegral_congr_support hf      intro x _      congr 1      refine setLIntegral_congr_fun measurableSet_Ioi fun s hs ↦ ?_      rw [ENNReal.mul_rpow_of_nonneg, ENNReal.rpow_inv_rpow, ← ENNReal.rpow_mul] <;> try positivity      congr      field_simp    _ = (∫⁻ a : α in (fun x ↦ ‖f x‖ₑ).support,        ((∫⁻ (s : ℝ) in res (xor j tc.mon) (tc.inv ‖f a‖ₑ),        (ENNReal.ofReal (s ^ (q - q₀ - 1)))) * ‖f a‖ₑ ^ q₀) ^ (p₀⁻¹ * q₀)⁻¹ ∂μ) ^ (p₀⁻¹ * q₀) := by      congr 1      apply lintegral_congr_support hf      intro x hfx      congr 1      apply lintegral_trunc_mul _ hq₀      measurability    _ = (∫⁻ a : α in (fun x ↦ ‖f x‖ₑ).support,        (((tc.inv ‖f a‖ₑ ^ (q - q₀ - 1 + 1) / ENNReal.ofReal |q - q₀ - 1 + 1|)) *        ‖f a‖ₑ ^ q₀) ^ (p₀⁻¹ * q₀)⁻¹ ∂μ) ^ (p₀⁻¹ * q₀) := by      congr 1      apply lintegral_congr_support hf      intro x hfx      congr 2      apply value_lintegral_res₀      split_ifs with h      · simp only [h, ↓reduceIte] at hpowers; linarith      · simp only [h, Bool.false_eq_true, ↓reduceIte] at hpowers; linarith    _ ≤ (∫⁻ a : α in (fun x ↦ ‖f x‖ₑ).support,        ((        (spf.d ^ (q - q₀ - 1 + 1) * ‖f a‖ₑ ^ (spf.σ⁻¹ * (q - q₀ - 1 + 1) + q₀) /        ENNReal.ofReal |q - q₀ - 1 + 1|))) ^ (p₀⁻¹ * q₀)⁻¹ ∂μ) ^ (p₀⁻¹ * q₀) := by      gcongr (?_) ^ (p₀⁻¹ * q₀)      apply setLIntegral_mono_ae      · fun_prop      · filter_upwards with x hfx        gcongr (?_) ^ (p₀⁻¹ * q₀)⁻¹        apply value_lintegral_res₂        · exact enorm_pos.mpr hfx        · simp only [sub_add_cancel]; linarith    _ = (∫⁻ a : α in (fun x ↦ ‖f x‖ₑ).support,        (((spf.d ^ (q - q₀)) ^ (p₀⁻¹ * q₀)⁻¹ *        (‖f a‖ₑ ^ ((spf.σ⁻¹ * (q - q₀) + q₀) * (p₀⁻¹ * q₀)⁻¹)) *    ENNReal.ofReal |q - q₀|⁻¹ ^ (p₀⁻¹ * q₀)⁻¹))  ∂μ) ^ (p₀⁻¹ * q₀) := by      congr 1      apply lintegral_congr_support hf      intro x _      rw [div_eq_mul_inv, sub_add_cancel, ENNReal.mul_rpow_of_nonneg,        ENNReal.mul_rpow_of_nonneg] <;> try positivity      rw [ENNReal.rpow_mul, ofReal_inv_of_pos]      have : q ≠ q₀ := by split_ifs at hpowers <;> order      exact abs_sub_pos.mpr this    _ = (spf.d ^ (q - q₀)) *        (∫⁻ (a : α) in (fun x ↦ ‖f x‖ₑ).support,        ‖f a‖ₑ ^ ((spf.σ⁻¹ * (q - q₀) + q₀) * (p₀⁻¹ * q₀)⁻¹) ∂μ) ^ (p₀⁻¹ * q₀) *        ENNReal.ofReal |q - q₀|⁻¹ := by      rw [lintegral_mul_const', lintegral_const_mul', ENNReal.mul_rpow_of_nonneg,          ENNReal.mul_rpow_of_nonneg, ENNReal.rpow_inv_rpow, ENNReal.rpow_inv_rpow] <;>          try positivity      · have := spf.hd.ne'        have := spf.hd'        refine rpow_ne_top_of_nonneg (by positivity) (by finiteness)      · finiteness    _ = (spf.d ^ (q - q₀)) *        (∫⁻ (a : α) in (fun x ↦ ‖f x‖ₑ).support,        ‖f a‖ₑ ^ (p₀ + spf.σ⁻¹ * (q - q₀) * (p₀ / q₀)) ∂μ) ^ (p₀⁻¹ * q₀) *        ENNReal.ofReal |q - q₀|⁻¹ := by      congr      ext x      congr      ring_nf      rw [inv_inv]      field_simp    _ = _ := by ring