refactor(measure_theory/function/lp_space): generalize actions from normed_field to normed_ring (#19083)

eric-wieser · eric-wieser · commit e0736bb5b48b · 2023-05-26T16:13:43.000Z
The motivation is that this makes it easier to work with integrals in non-commutative rings.

This makes the proof of Hölder's inequality slightly more painful, as we can no longer use `simp_rw [norm_smul]` and have to make monotonicity arguments instead. `rel_congr` may be able to clean this up in mathlib3.

The results in the `normed_space` section (including Hölder's inequality) have been largely moved to the `monotonicity` section, where they hold more generally for arbitrary binary functions.
The results about scalar actions now follow as trivial special cases.

This also makes the `fails_quickly` linter reject the `complete_space (Lp_meas F 𝕜 m p μ)` instance.
Since Lean4 is around the corner and there are better debugging tools there, I think it's ok to just no-lint it.
diff --git a/src/measure_theory/function/conditional_expectation/basic.lean b/src/measure_theory/function/conditional_expectation/basic.lean
@@ -506,6 +506,10 @@ instance [hm : fact (m ≤ m0)] [complete_space F] [hp : fact (1 ≤ p)] :
   complete_space (Lp_meas_subgroup F m p μ) :=
 by { rw (Lp_meas_subgroup_to_Lp_trim_iso F p μ hm.elim).complete_space_iff, apply_instance, }
 
+-- For now just no-lint this; lean4's tree-based logging will make this easier to debug.
+-- One possible change might be to generalize `𝕜` from `is_R_or_C` to `normed_field`, as this
+-- result may well hold there.
+@[nolint fails_quickly]
 instance [hm : fact (m ≤ m0)] [complete_space F] [hp : fact (1 ≤ p)] :
   complete_space (Lp_meas F 𝕜 m p μ) :=
 by { rw (Lp_meas_subgroup_to_Lp_meas_iso F 𝕜 p μ).symm.complete_space_iff, apply_instance, }
@@ -1263,8 +1267,7 @@ lemma condexp_ind_smul_smul' [normed_space ℝ F] [smul_comm_class ℝ 𝕜 F] (
   (hμs : μ s ≠ ∞) (c : 𝕜) (x : F) :
   condexp_ind_smul hm hs hμs (c • x) = c • condexp_ind_smul hm hs hμs x :=
 by rw [condexp_ind_smul, condexp_ind_smul, to_span_singleton_smul',
-  (to_span_singleton ℝ x).smul_comp_LpL_apply c
-  ↑(condexp_L2 ℝ hm (indicator_const_Lp 2 hs hμs (1 : ℝ)))]
+  (to_span_singleton ℝ x).smul_comp_LpL c, smul_apply]
 
 lemma condexp_ind_smul_ae_eq_smul (hm : m ≤ m0) (hs : measurable_set s) (hμs : μ s ≠ ∞) (x : G) :
   condexp_ind_smul hm hs hμs x
diff --git a/src/measure_theory/function/continuous_map_dense.lean b/src/measure_theory/function/continuous_map_dense.lean
@@ -109,7 +109,7 @@ begin
   { refine function.support_subset_iff'.2 (λ x hx, _),
     simp only [hgv hx, pi.zero_apply, zero_smul] },
   have gc_mem : mem_ℒp (λ x, g x • c) p μ,
-  { apply mem_ℒp.smul_of_top_left (mem_ℒp_top_const _),
+  { refine mem_ℒp.smul_of_top_left (mem_ℒp_top_const _) _,
     refine ⟨g.continuous.ae_strongly_measurable, _⟩,
     have : snorm (v.indicator (λ x, (1 : ℝ))) p μ < ⊤,
     { refine (snorm_indicator_const_le _ _).trans_lt _,
diff --git a/src/measure_theory/function/lp_space.lean b/src/measure_theory/function/lp_space.lean
