chore(SchwartzSpace): clean up white space (#19336)

Definitions in term mode using `mkCLM` are indented by 6 spaces, but formulating things with `refine` drops it to a more reasonable 2 spaces. Absolutely no math change, just unindenting.

Author: sgouezel

Mathlib/Analysis/Distribution/SchwartzSpace.lean

@@ -764,53 +764,51 @@ variable [NormedAddCommGroup G] [NormedSpace ℝ G]
 /-- The map `f ↦ (x ↦ B (f x) (g x))` as a continuous `𝕜`-linear map on Schwartz space,
 where `B` is a continuous `𝕜`-linear map and `g` is a function of temperate growth. -/
 def bilinLeftCLM (B : E →L[ℝ] F →L[ℝ] G) {g : D → F} (hg : g.HasTemperateGrowth) :
-    𝓢(D, E) →L[ℝ] 𝓢(D, G) :=
+    𝓢(D, E) →L[ℝ] 𝓢(D, G) := by
   -- Todo (after port): generalize to `B : E →L[𝕜] F →L[𝕜] G` and `𝕜`-linear
-    mkCLM
-    (fun f x => B (f x) (g x))
+  refine mkCLM (fun f x => B (f x) (g x))
     (fun _ _ _ => by
       simp only [map_add, add_left_inj, Pi.add_apply, eq_self_iff_true,
         ContinuousLinearMap.add_apply])
     (fun _ _ _ => by
       simp only [smul_apply, map_smul, ContinuousLinearMap.coe_smul', Pi.smul_apply,
         RingHom.id_apply])
-    (fun f => (B.isBoundedBilinearMap.contDiff.restrict_scalars ℝ).comp (f.smooth'.prod hg.1))
-    (by
-      rintro ⟨k, n⟩
-      rcases hg.norm_iteratedFDeriv_le_uniform_aux n with ⟨l, C, hC, hgrowth⟩
-      use
-        Finset.Iic (l + k, n), ‖B‖ * ((n : ℝ) + (1 : ℝ)) * n.choose (n / 2) * (C * 2 ^ (l + k)),
-        by positivity
-      intro f x
-      have hxk : 0 ≤ ‖x‖ ^ k := by positivity
-      have hnorm_mul :=
-        ContinuousLinearMap.norm_iteratedFDeriv_le_of_bilinear B f.smooth' hg.1 x (n := n) le_top
-      refine le_trans (mul_le_mul_of_nonneg_left hnorm_mul hxk) ?_
-      move_mul [← ‖B‖]
-      simp_rw [mul_assoc ‖B‖]
-      gcongr _ * ?_
-      rw [Finset.mul_sum]
-      have : (∑ _x ∈ Finset.range (n + 1), (1 : ℝ)) = n + 1 := by simp
-      simp_rw [mul_assoc ((n : ℝ) + 1)]
-      rw [← this, Finset.sum_mul]
-      refine Finset.sum_le_sum fun i hi => ?_
-      simp only [one_mul]
-      move_mul [(Nat.choose n i : ℝ), (Nat.choose n (n / 2) : ℝ)]
-      gcongr ?_ * ?_
-      swap
-      · norm_cast
-        exact i.choose_le_middle n
-      specialize hgrowth (n - i) (by simp only [tsub_le_self]) x
-      refine le_trans (mul_le_mul_of_nonneg_left hgrowth (by positivity)) ?_
-      move_mul [C]
-      gcongr ?_ * C
-      rw [Finset.mem_range_succ_iff] at hi
-      change i ≤ (l + k, n).snd at hi
-      refine le_trans ?_ (one_add_le_sup_seminorm_apply le_rfl hi f x)
-      rw [pow_add]
-      move_mul [(1 + ‖x‖) ^ l]
-      gcongr
-      simp)
+    (fun f => (B.isBoundedBilinearMap.contDiff.restrict_scalars ℝ).comp (f.smooth'.prod hg.1)) ?_
+  rintro ⟨k, n⟩
+  rcases hg.norm_iteratedFDeriv_le_uniform_aux n with ⟨l, C, hC, hgrowth⟩
+  use
+    Finset.Iic (l + k, n), ‖B‖ * ((n : ℝ) + (1 : ℝ)) * n.choose (n / 2) * (C * 2 ^ (l + k)),
+    by positivity
+  intro f x
+  have hxk : 0 ≤ ‖x‖ ^ k := by positivity
+  have hnorm_mul :=
+    ContinuousLinearMap.norm_iteratedFDeriv_le_of_bilinear B f.smooth' hg.1 x (n := n) le_top
+  refine le_trans (mul_le_mul_of_nonneg_left hnorm_mul hxk) ?_
+  move_mul [← ‖B‖]
+  simp_rw [mul_assoc ‖B‖]
+  gcongr _ * ?_
+  rw [Finset.mul_sum]
+  have : (∑ _x ∈ Finset.range (n + 1), (1 : ℝ)) = n + 1 := by simp
+  simp_rw [mul_assoc ((n : ℝ) + 1)]
+  rw [← this, Finset.sum_mul]
+  refine Finset.sum_le_sum fun i hi => ?_
+  simp only [one_mul]
+  move_mul [(Nat.choose n i : ℝ), (Nat.choose n (n / 2) : ℝ)]
+  gcongr ?_ * ?_
+  swap
+  · norm_cast
+    exact i.choose_le_middle n
+  specialize hgrowth (n - i) (by simp only [tsub_le_self]) x
+  refine le_trans (mul_le_mul_of_nonneg_left hgrowth (by positivity)) ?_
+  move_mul [C]
+  gcongr ?_ * C
+  rw [Finset.mem_range_succ_iff] at hi
+  change i ≤ (l + k, n).snd at hi
+  refine le_trans ?_ (one_add_le_sup_seminorm_apply le_rfl hi f x)
+  rw [pow_add]
+  move_mul [(1 + ‖x‖) ^ l]
+  gcongr
+  simp
 
 end Multiplication
 
@@ -824,68 +822,67 @@ variable [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F]
 /-- Composition with a function on the right is a continuous linear map on Schwartz space
 provided that the function is temperate and growths polynomially near infinity. -/
 def compCLM {g : D → E} (hg : g.HasTemperateGrowth)
-    (hg_upper : ∃ (k : ℕ) (C : ℝ), ∀ x, ‖x‖ ≤ C * (1 + ‖g x‖) ^ k) : 𝓢(E, F) →L[𝕜] 𝓢(D, F) :=
-  mkCLM (fun f x => f (g x))
+    (hg_upper : ∃ (k : ℕ) (C : ℝ), ∀ x, ‖x‖ ≤ C * (1 + ‖g x‖) ^ k) : 𝓢(E, F) →L[𝕜] 𝓢(D, F) := by
+  refine mkCLM (fun f x => f (g x))
     (fun _ _ _ => by simp only [add_left_inj, Pi.add_apply, eq_self_iff_true]) (fun _ _ _ => rfl)
-    (fun f => f.smooth'.comp hg.1)
-    (by
-      rintro ⟨k, n⟩
-      rcases hg.norm_iteratedFDeriv_le_uniform_aux n with ⟨l, C, hC, hgrowth⟩
-      rcases hg_upper with ⟨kg, Cg, hg_upper'⟩
-      have hCg : 1 ≤ 1 + Cg := by
-        refine le_add_of_nonneg_right ?_
-        specialize hg_upper' 0
-        rw [norm_zero] at hg_upper'
-        exact nonneg_of_mul_nonneg_left hg_upper' (by positivity)
-      let k' := kg * (k + l * n)
-      use Finset.Iic (k', n), (1 + Cg) ^ (k + l * n) * ((C + 1) ^ n * n ! * 2 ^ k'), by positivity
-      intro f x
-      let seminorm_f := ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 _ _)) f
-      have hg_upper'' : (1 + ‖x‖) ^ (k + l * n) ≤ (1 + Cg) ^ (k + l * n) * (1 + ‖g x‖) ^ k' := by
-        rw [pow_mul, ← mul_pow]
-        gcongr
-        rw [add_mul]
-        refine add_le_add ?_ (hg_upper' x)
-        nth_rw 1 [← one_mul (1 : ℝ)]
-        gcongr
-        apply one_le_pow₀
-        simp only [le_add_iff_nonneg_right, norm_nonneg]
-      have hbound :
-        ∀ i, i ≤ n → ‖iteratedFDeriv ℝ i f (g x)‖ ≤ 2 ^ k' * seminorm_f / (1 + ‖g x‖) ^ k' := by
-        intro i hi
-        have hpos : 0 < (1 + ‖g x‖) ^ k' := by positivity
-        rw [le_div_iff₀' hpos]
-        change i ≤ (k', n).snd at hi
-        exact one_add_le_sup_seminorm_apply le_rfl hi _ _
-      have hgrowth' : ∀ N : ℕ, 1 ≤ N → N ≤ n →
-          ‖iteratedFDeriv ℝ N g x‖ ≤ ((C + 1) * (1 + ‖x‖) ^ l) ^ N := by
-        intro N hN₁ hN₂
-        refine (hgrowth N hN₂ x).trans ?_
-        rw [mul_pow]
-        have hN₁' := (lt_of_lt_of_le zero_lt_one hN₁).ne'
-        gcongr
-        · exact le_trans (by simp [hC]) (le_self_pow₀ (by simp [hC]) hN₁')
-        · refine le_self_pow₀ (one_le_pow₀ ?_) hN₁'
-          simp only [le_add_iff_nonneg_right, norm_nonneg]
-      have := norm_iteratedFDeriv_comp_le f.smooth' hg.1 le_top x hbound hgrowth'
-      have hxk : ‖x‖ ^ k ≤ (1 + ‖x‖) ^ k :=
-        pow_le_pow_left₀ (norm_nonneg _) (by simp only [zero_le_one, le_add_iff_nonneg_left]) _
-      refine le_trans (mul_le_mul hxk this (by positivity) (by positivity)) ?_
-      have rearrange :
-        (1 + ‖x‖) ^ k *
-            (n ! * (2 ^ k' * seminorm_f / (1 + ‖g x‖) ^ k') * ((C + 1) * (1 + ‖x‖) ^ l) ^ n) =
-          (1 + ‖x‖) ^ (k + l * n) / (1 + ‖g x‖) ^ k' *
-            ((C + 1) ^ n * n ! * 2 ^ k' * seminorm_f) := by
-        rw [mul_pow, pow_add, ← pow_mul]
-        ring
-      rw [rearrange]
-      have hgxk' : 0 < (1 + ‖g x‖) ^ k' := by positivity
-      rw [← div_le_iff₀ hgxk'] at hg_upper''
-      have hpos : (0 : ℝ) ≤ (C + 1) ^ n * n ! * 2 ^ k' * seminorm_f := by
-        have : 0 ≤ seminorm_f := apply_nonneg _ _
-        positivity
-      refine le_trans (mul_le_mul_of_nonneg_right hg_upper'' hpos) ?_
-      rw [← mul_assoc])
+    (fun f => f.smooth'.comp hg.1) ?_
+  rintro ⟨k, n⟩
+  rcases hg.norm_iteratedFDeriv_le_uniform_aux n with ⟨l, C, hC, hgrowth⟩
+  rcases hg_upper with ⟨kg, Cg, hg_upper'⟩
+  have hCg : 1 ≤ 1 + Cg := by
+    refine le_add_of_nonneg_right ?_
+    specialize hg_upper' 0
+    rw [norm_zero] at hg_upper'
+    exact nonneg_of_mul_nonneg_left hg_upper' (by positivity)
+  let k' := kg * (k + l * n)
+  use Finset.Iic (k', n), (1 + Cg) ^ (k + l * n) * ((C + 1) ^ n * n ! * 2 ^ k'), by positivity
+  intro f x
+  let seminorm_f := ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 _ _)) f
+  have hg_upper'' : (1 + ‖x‖) ^ (k + l * n) ≤ (1 + Cg) ^ (k + l * n) * (1 + ‖g x‖) ^ k' := by
+    rw [pow_mul, ← mul_pow]
+    gcongr
+    rw [add_mul]
+    refine add_le_add ?_ (hg_upper' x)
+    nth_rw 1 [← one_mul (1 : ℝ)]
+    gcongr
+    apply one_le_pow₀
+    simp only [le_add_iff_nonneg_right, norm_nonneg]
+  have hbound :
+    ∀ i, i ≤ n → ‖iteratedFDeriv ℝ i f (g x)‖ ≤ 2 ^ k' * seminorm_f / (1 + ‖g x‖) ^ k' := by
+    intro i hi
+    have hpos : 0 < (1 + ‖g x‖) ^ k' := by positivity
+    rw [le_div_iff₀' hpos]
+    change i ≤ (k', n).snd at hi
+    exact one_add_le_sup_seminorm_apply le_rfl hi _ _
+  have hgrowth' : ∀ N : ℕ, 1 ≤ N → N ≤ n →
+      ‖iteratedFDeriv ℝ N g x‖ ≤ ((C + 1) * (1 + ‖x‖) ^ l) ^ N := by
+    intro N hN₁ hN₂
+    refine (hgrowth N hN₂ x).trans ?_
+    rw [mul_pow]
+    have hN₁' := (lt_of_lt_of_le zero_lt_one hN₁).ne'
+    gcongr
+    · exact le_trans (by simp [hC]) (le_self_pow₀ (by simp [hC]) hN₁')
+    · refine le_self_pow₀ (one_le_pow₀ ?_) hN₁'
+      simp only [le_add_iff_nonneg_right, norm_nonneg]
+  have := norm_iteratedFDeriv_comp_le f.smooth' hg.1 le_top x hbound hgrowth'
+  have hxk : ‖x‖ ^ k ≤ (1 + ‖x‖) ^ k :=
+    pow_le_pow_left₀ (norm_nonneg _) (by simp only [zero_le_one, le_add_iff_nonneg_left]) _
+  refine le_trans (mul_le_mul hxk this (by positivity) (by positivity)) ?_
+  have rearrange :
+    (1 + ‖x‖) ^ k *
+        (n ! * (2 ^ k' * seminorm_f / (1 + ‖g x‖) ^ k') * ((C + 1) * (1 + ‖x‖) ^ l) ^ n) =
+      (1 + ‖x‖) ^ (k + l * n) / (1 + ‖g x‖) ^ k' *
+        ((C + 1) ^ n * n ! * 2 ^ k' * seminorm_f) := by
+    rw [mul_pow, pow_add, ← pow_mul]
+    ring
+  rw [rearrange]
+  have hgxk' : 0 < (1 + ‖g x‖) ^ k' := by positivity
+  rw [← div_le_iff₀ hgxk'] at hg_upper''
+  have hpos : (0 : ℝ) ≤ (C + 1) ^ n * n ! * 2 ^ k' * seminorm_f := by
+    have : 0 ≤ seminorm_f := apply_nonneg _ _
+    positivity
+  refine le_trans (mul_le_mul_of_nonneg_right hg_upper'' hpos) ?_
+  rw [← mul_assoc]
 
 @[simp] lemma compCLM_apply {g : D → E} (hg : g.HasTemperateGrowth)
     (hg_upper : ∃ (k : ℕ) (C : ℝ), ∀ x, ‖x‖ ≤ C * (1 + ‖g x‖) ^ k) (f : 𝓢(E, F)) :
@@ -1070,25 +1067,22 @@ lemma integrable (f : 𝓢(D, V)) : Integrable f μ :=
 
 variable (𝕜 μ) in
 /-- The integral as a continuous linear map from Schwartz space to the codomain. -/
-def integralCLM : 𝓢(D, V) →L[𝕜] V :=
-  mkCLMtoNormedSpace (∫ x, · x ∂μ)
-    (fun f g ↦ by
-      exact integral_add f.integrable g.integrable)
-    (integral_smul · ·)
-    (by
-      rcases hμ.exists_integrable with ⟨n, h⟩
-      let m := (n, 0)
-      use Finset.Iic m, 2 ^ n * ∫ x : D, (1 + ‖x‖) ^ (- (n : ℝ)) ∂μ
-      refine ⟨by positivity, fun f ↦ (norm_integral_le_integral_norm f).trans ?_⟩
-      have h' : ∀ x, ‖f x‖ ≤ (1 + ‖x‖) ^ (-(n : ℝ)) *
-          (2 ^ n * ((Finset.Iic m).sup (fun m' => SchwartzMap.seminorm 𝕜 m'.1 m'.2) f)) := by
-        intro x
-        rw [rpow_neg (by positivity), ← div_eq_inv_mul, le_div_iff₀' (by positivity), rpow_natCast]
-        simpa using one_add_le_sup_seminorm_apply (m := m) (k := n) (n := 0) le_rfl le_rfl f x
-      apply (integral_mono (by simpa using f.integrable_pow_mul μ 0) _ h').trans
-      · rw [integral_mul_right, ← mul_assoc, mul_comm (2 ^ n)]
-        rfl
-      apply h.mul_const)
+def integralCLM : 𝓢(D, V) →L[𝕜] V := by
+  refine mkCLMtoNormedSpace (∫ x, · x ∂μ)
+    (fun f g ↦ integral_add f.integrable g.integrable) (integral_smul · ·) ?_
+  rcases hμ.exists_integrable with ⟨n, h⟩
+  let m := (n, 0)
+  use Finset.Iic m, 2 ^ n * ∫ x : D, (1 + ‖x‖) ^ (- (n : ℝ)) ∂μ
+  refine ⟨by positivity, fun f ↦ (norm_integral_le_integral_norm f).trans ?_⟩
+  have h' : ∀ x, ‖f x‖ ≤ (1 + ‖x‖) ^ (-(n : ℝ)) *
+      (2 ^ n * ((Finset.Iic m).sup (fun m' => SchwartzMap.seminorm 𝕜 m'.1 m'.2) f)) := by
+    intro x
+    rw [rpow_neg (by positivity), ← div_eq_inv_mul, le_div_iff₀' (by positivity), rpow_natCast]
+    simpa using one_add_le_sup_seminorm_apply (m := m) (k := n) (n := 0) le_rfl le_rfl f x
+  apply (integral_mono (by simpa using f.integrable_pow_mul μ 0) _ h').trans
+  · rw [integral_mul_right, ← mul_assoc, mul_comm (2 ^ n)]
+    rfl
+  apply h.mul_const
 
 variable (𝕜) in
 @[simp]