Lemma6_1_3.eLpNorm_𝓜_le_eLpNorm_𝓜p_mul

lemma eLpNorm_𝓜_le_eLpNorm_𝓜p_mul (hf : Measurable f) (hfF : ∀ x, ‖f x‖ ≤ F.indicator 1 x)    {p p' : ℝ} (hpp : p.HolderConjugate p') :    eLpNorm (𝓜 𝔄 f) 2 ≤ (dens₂ 𝔄) ^ (p'⁻¹) * eLpNorm (𝓜p 𝔄 p f) 2 := by  have bf := bcs_of_measurable_of_le_indicator_f hf hfF  have p_pos : 0 < p := hpp.left_pos  have p'_pos : 0 < p' := hpp.right_pos  have inv_p_pos : 0 < p⁻¹ := by positivity  have inv_p'_pos : 0 < p'⁻¹ := by positivity  have : ENNReal.ofReal p ≠ 0 := ofReal_ne_zero_iff.mpr p_pos  have : ENNReal.ofReal p ≠ ⊤ := ofReal_ne_top  have : ENNReal.ofReal p' ≠ 0 := ofReal_ne_zero_iff.mpr p'_pos  have : ENNReal.ofReal p' ≠ ⊤ := ofReal_ne_top  have hp_coe : p.toNNReal.toReal = p := Real.coe_toNNReal _ (by positivity)  conv_lhs => rw [eq_indicator_one_mul_of_norm_le hfF]  refine eLpNorm_le_mul_eLpNorm_of_ae_le_mul'' _    measurable_maximalFunction.aestronglyMeasurable (ae_of_all _ <| fun x ↦ ?_)  simp only [enorm_eq_self, 𝓜, maximalFunction, ENNReal.rpow_one, inv_one]  apply iSup_le_iff.mpr <| fun 𝔭 ↦ iSup_le_iff.mpr <| fun h𝔭 ↦ ?_  apply indicator_le <| fun x hx ↦ ?_  rw [laverage_eq]  conv_lhs => enter [1, 2, x]; rw [Pi.mul_apply, enorm_mul, mul_comm]  set B := ball (𝔠 𝔭) (8 * ↑D ^ 𝔰 𝔭)  set dB := volume.restrict B  set mB := volume.restrict B univ  have mB_pos : 0 < mB := by    simp only [Measure.restrict_apply_univ B, mB]    exact measure_ball_pos _ _ (pos_of_mem_ball hx)  have mB_ne_top : mB ≠ ⊤ := by    simpa [Measure.restrict_apply_univ B, mB] using measure_ball_ne_top  have hmeas : AEMeasurable (fun x ↦ ‖(F.indicator 1 x : ℂ)‖ₑ) (volume.restrict B) :=    aemeasurable_const.indicator measurableSet_F |>.enorm  calc    _ ≤  eLpNorm (fun x ↦ ‖f x‖ₑ) (ENNReal.ofReal p) dB *          eLpNorm (fun x ↦ ‖(F.indicator 1 x : ℂ)‖ₑ) (ENNReal.ofReal p') dB / mB := by      gcongr      exact lintegral_mul_le_eLpNorm_mul_eLqNorm hpp.ennrealOfReal        bf.enorm.aestronglyMeasurable.aemeasurable.restrict hmeas    _ = (eLpNorm (fun x ↦ ‖(F.indicator 1 x : ℂ)‖ₑ) (ENNReal.ofReal p') dB / mB ^ (p'⁻¹))        * (eLpNorm (fun x ↦ ‖f x‖ₑ) (ENNReal.ofReal p) dB / mB ^ (p⁻¹)) := by      rw [mul_comm, div_eq_mul_inv]      have : mB⁻¹ = (mB ^ (p⁻¹))⁻¹ * (mB ^ (p'⁻¹))⁻¹ := by        rw [← ENNReal.mul_inv (Or.inl <| ne_of_gt <| ENNReal.rpow_pos mB_pos mB_ne_top)          (Or.inr <| ne_of_gt <| ENNReal.rpow_pos mB_pos mB_ne_top), ← ENNReal.rpow_add _ _          (ne_of_gt mB_pos) mB_ne_top, hpp.inv_add_inv_eq_one, ENNReal.rpow_one]      rw [this, div_eq_mul_inv, div_eq_mul_inv]      ring    _ ≤ _ := by      gcongr      · rw [eLpNorm_eq_lintegral_rpow_enorm_toReal (by assumption) (by assumption), toReal_ofReal <|          le_of_lt p'_pos, one_div, ← div_rpow_of_nonneg _ _ (le_of_lt inv_p'_pos), dens₂]        gcongr        refine le_trans ?_ <| le_iSup₂ 𝔭 h𝔭        refine le_trans ?_ <| le_iSup _ (8 * (D : ℝ) ^ 𝔰 𝔭)        refine le_trans (le_of_eq ?_) <| le_iSup _ (by gcongr; norm_num)        simp_rw [enorm_enorm]        congr        · rw [← lintegral_indicator_one <| measurableSet_F.inter measurableSet_ball,            inter_indicator_one]          conv_rhs => enter [2, x]; rw [Pi.mul_apply, ← indicator_mul_right]          rw [lintegral_indicator measurableSet_ball]          refine lintegral_congr (fun x ↦ ?_)          rw [Pi.one_apply, mul_one, enorm_indicator_eq_indicator_enorm, indicator, indicator]          split_ifs <;> simp [p'_pos]        · exact Measure.restrict_apply_univ B      · rw [eLpNorm_eq_lintegral_rpow_enorm_toReal (by assumption) (by assumption),          toReal_ofReal <| le_of_lt p_pos, 𝓜p, maximalFunction, one_div,          ← div_rpow_of_nonneg _ _ (le_of_lt inv_p_pos), ← laverage_eq, hp_coe]        refine le_trans (le_of_eq ?_) <| le_iSup₂ 𝔭 h𝔭        simp_rw [enorm_enorm]        rw [indicator_of_mem hx]