feat(LpSpace/DomAct): add a lemma + @[to_additive] (#14488)

Author: urkud

Mathlib/MeasureTheory/Function/LpSpace/DomAct/Basic.lean

@@ -50,6 +50,14 @@ theorem smul_Lp_const [IsFiniteMeasure μ] (c : Mᵈᵐᵃ) (a : E) :
     c • Lp.const p μ a = Lp.const p μ a :=
   rfl
 
+@[to_additive]
+theorem mk_smul_indicatorConstLp (c : M)
+    {s : Set α} (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (b : E) :
+    mk c • indicatorConstLp p hs hμs b =
+      indicatorConstLp p (hs.preimage <| measurable_const_smul c)
+        (by rwa [SMulInvariantMeasure.measure_preimage_smul c hs]) b :=
+  rfl
+
 instance [SMul N α] [SMulCommClass M N α] [SMulInvariantMeasure N α μ] [MeasurableSMul N α] :
     SMulCommClass Mᵈᵐᵃ Nᵈᵐᵃ (Lp E p μ) :=
   Subtype.val_injective.smulCommClass (fun _ _ ↦ rfl) fun _ _ ↦ rfl
@@ -105,6 +113,7 @@ theorem edist_smul_Lp (c : Mᵈᵐᵃ) (f g : Lp E p μ) : edist (c • f) (c 
 
 variable [Fact (1 ≤ p)]
 
+@[to_additive]
 instance : IsometricSMul Mᵈᵐᵃ (Lp E p μ) := ⟨edist_smul_Lp⟩
 
 end SMul