Lean/Mathlib: Lᵖ bound by duality without knowing F ∈ Lᵖ (truncated norming function)

To get ∫⁻‖F‖ₑ^p ≤ K^(p-1)∫⁻‖f‖ₑ^p from ∫ F g = ∫ f (S g) and an L^q bound for S, test against g_N = indicator A_N (F·|F|^(p-2)) with A_N = spanningSets μ N ∩ {|F| ≤ N}. Then g_N is bounded on a finite-measure set, so it is in every Lʳ: use memLp_indicator_iff_restrict + MemLp.of_bound, with have : IsFiniteMeasure (μ.restrict s) := isFiniteMeasure_restrict.2 hμs. The pointwise facts are |x·|x|^(p-2)| = |x|^(p-1) and x·(x|x|^(p-2)) = |x|^p. They hold also at x = 0 because Real.zero_rpow gives 0^r = 0 for r ≠ 0, so no Real.sign is needed. Chain: X_N ≤ ‖∫F g_N‖ₑ (Real.ofReal_le_enorm after ofReal_integral_eq_lintegral_ofReal), then enorm_integral_le_lintegral_enorm, then ENNReal.lintegral_mul_le_Lp_mul_Lq. Divide by X_N^(1/q) < ∞ with ENNReal.mul_le_mul_iff_left. Finish with lintegral_iSup on the indicators. hpq.div_conj_eq_sub_one turns K^(p/q) into K^(p-1).