refactor(QuantumMechanics): SpaceDHilbertSpace API

Physlib/QuantumMechanics/DDimensions/Basic.lean

@@ -128,7 +128,7 @@ lemma potentialOperator_isSelfAdjoint (h_AESM : AEStronglyMeasurable Q.potential
   mulOperator_isSelfAdjoint_ofReal (by fun_prop) (by ext; simp)
 
 lemma potentialOperator_domain_ge (h_HTG : Q.potential.HasTemperateGrowth) :
-    schwartzSubmodule Q.d ≤ Q.potentialOperator.domain :=
+    SchwartzSubmodule Q.d ≤ Q.potentialOperator.domain :=
   mulOperator_domain_ge_of_hasTemperateGrowth (by fun_prop)
 
 /-!

Physlib/QuantumMechanics/DDimensions/Operators/Momentum.lean

@@ -85,20 +85,20 @@ open SchwartzSubmodule
 
 /-- The momentum operator as a LinearPMap with domain the Schwartz submodule. -/
 def momentumOperator : SpaceDHilbertSpace d →ₗ.[ℂ] SpaceDHilbertSpace d where
-  domain := schwartzSubmodule d
+  domain := SchwartzSubmodule d
   toFun := schwartzIncl.toLinearMap ∘ₗ (𝐩 i).toLinearMap ∘ₗ schwartzEquiv.symm.toLinearMap
 
 @[inherit_doc momentumOperator]
 notation "𝓟" => momentumOperator
 
-lemma momentumOperator_apply (ψ : schwartzSubmodule d) :
+lemma momentumOperator_apply (ψ : SchwartzSubmodule d) :
     𝓟 i ψ = schwartzEquiv (𝐩 i (schwartzEquiv.symm ψ)) := rfl
 
-lemma momentumOperator_apply_ae (ψ : schwartzSubmodule d) :
+lemma momentumOperator_apply_ae (ψ : SchwartzSubmodule d) :
     𝓟 i ψ =ᵐ[volume] 𝐩 i (schwartzEquiv.symm ψ) :=
   schwartzEquiv_coe_ae _
 
-lemma momentumOperator_range (ψ : schwartzSubmodule d) : 𝓟 i ψ ∈ schwartzSubmodule d := by
+lemma momentumOperator_range (ψ : SchwartzSubmodule d) : 𝓟 i ψ ∈ SchwartzSubmodule d := by
   simp [momentumOperator_apply]
 
 lemma momentumOperator_hasDenseDomain : (𝓟 i).HasDenseDomain := SchwartzSubmodule.dense d
@@ -144,12 +144,12 @@ def momentumSqOperator : SpaceDHilbertSpace d →ₗ.[ℂ] SpaceDHilbertSpace d
 lemma momentumSqOperator_eq :
     momentumSqOperator (d := d) = sum fun i ↦ (𝓟 i).comp (𝓟 i) (momentumOperator_range i) := rfl
 
-lemma momentumSqOperator_domain_eq : momentumSqOperator.domain = schwartzSubmodule d := by
+lemma momentumSqOperator_domain_eq : momentumSqOperator.domain = SchwartzSubmodule d := by
   rw [momentumSqOperator_eq, sum_domain]
   rcases eq_zero_or_pos d with rfl | hd
   · simp [SchwartzSubmodule.zero_eq_top]
   · letI := Fin.pos_iff_nonempty.mp hd
-    rw [← iInf_const (a := schwartzSubmodule d) (ι := Fin d)]
+    rw [← iInf_const (a := SchwartzSubmodule d) (ι := Fin d)]
     congr
 
 end

Physlib/QuantumMechanics/DDimensions/Operators/Multiplication.lean

@@ -52,7 +52,6 @@ noncomputable section
 
 open LinearPMap
 open MeasureTheory
-open AEEqFun
 open Filter
 open ComplexConjugate
 
@@ -68,26 +67,24 @@ def mulOperator (f : Space d → ℂ) : SpaceDHilbertSpace d →ₗ.[ℂ] SpaceD
     carrier := {ψ : SpaceDHilbertSpace d | MemHS (f • ψ.val.cast)}
     add_mem' := by
       intro ψ φ hψ hφ
-      refine memHS_of_ae _ (memHS_add hψ hφ) ?_
-      filter_upwards [coeFn_add ψ.val φ.val] with x h
+      refine (hψ.add hφ).ae_eq ?_
+      filter_upwards [coeFn_add ψ φ] with x h
       simp [mul_add, h]
-    zero_mem' := memHS_of_ae 0 zero_memHS (by filter_upwards; simp)
+    zero_mem' := MemHS.zero.ae_eq (by filter_upwards; simp)
     smul_mem' c ψ hψ := by
-      refine memHS_of_ae _ (memHS_const_smul (c := c) hψ) ?_
-      filter_upwards [coeFn_smul c ψ.val] with x h
-      change _ = (f • (c • ψ.val).cast) x
+      refine (hψ.const_smul c).ae_eq ?_
+      filter_upwards [coeFn_smul c ψ] with x h
       simp [h, mul_left_comm]
   }
   toFun := {
     toFun ψ := mk ψ.prop
     map_add' ψ φ := by
       rw [← mk_add, mk_eq_iff]
-      filter_upwards [coeFn_add ψ.1.val φ.1.val] with x h
+      filter_upwards [coeFn_add ψ.1 φ.1] with x h
       simp [h, mul_add]
     map_smul' c ψ := by
       rw [← mk_const_smul, mk_eq_iff]
-      filter_upwards [coeFn_smul c ψ.1.val] with x h
-      change (f • (c • ψ.1.val).cast) x = _
+      filter_upwards [coeFn_smul c ψ.1] with x h
       simp [h, mul_left_comm]
   }
 
@@ -99,7 +96,7 @@ lemma mem_mulOperator_domain_iff
   Iff.rfl
 
 lemma mulOperator_apply_ae {f : Space d → ℂ} (ψ : (𝓜 f).domain) : (𝓜 f) ψ =ᵐ[volume] f • ψ :=
-  coe_mk_ae ψ.prop
+  coeFn_mk ψ.prop
 
 /-!
 ## B. Domain
@@ -112,27 +109,27 @@ lemma mulOperator_hasDenseDomain {f : Space d → ℂ} (hf : AEStronglyMeasurabl
   obtain ⟨u, hu, hfu⟩ := AEStronglyMeasurable.aemeasurable hf
   let s : ℕ → Set (Space d) := fun n ↦ u ⁻¹' (Metric.closedBall 0 n)
   let φ : ℕ → SpaceDHilbertSpace d := fun n ↦
-    mk ((coe_hilbertSpace_memHS ψ).indicator (s := s n) (by measurability))
-  have hφ : ∀ n, φ n =ᵐ[volume] (s n).indicator ψ := fun n ↦ coe_mk_ae _
+    mk ((memHS_coe ψ).indicator (s := s n) (by measurability))
+  have hφ : ∀ n, φ n =ᵐ[volume] (s n).indicator ψ := fun n ↦ coeFn_mk _
   use φ
   constructor
   · intro n
     refine memHS_iff.mpr ⟨by measurability, by measurability, ?_⟩
-    refine HasFiniteIntegral.mono (memHS_iff.mp (coe_hilbertSpace_memHS (n • φ n))).2.2 ?_
-    filter_upwards [hfu, coeFn_smul n (φ n).val, hφ n] with x h₁ h₂ h₃
+    refine HasFiniteIntegral.mono (memHS_iff.mp <| memHS_coe (n • φ n)).2.2 ?_
+    filter_upwards [hfu, coeFn_smul n (φ n), hφ n] with x h₁ h₂ h₃
     by_cases hx : x ∈ s n
     · simp_rw [norm_pow, norm_norm, sq_le_sq, abs_norm]
       calc
         _ = ‖u x‖ * ‖φ n x‖ := by simp [h₁]
         _ ≤ n * ‖φ n x‖ := mul_le_mul_of_nonneg_right (by simp_all [s]) (norm_nonneg _)
-        _ = ‖(n • φ n) x‖ := by simp [h₂]
+        _ = ‖(n • φ n) x‖ := by simp [h₂, ← Nat.cast_smul_eq_nsmul ℂ]
     · simp [h₃, hx]
   · apply tendsto_sub_nhds_zero_iff.mp
     apply tendsto_zero_iff_tendsto_zero_lintegral_enorm_sq.mpr
     have h : ∀ n, ∫⁻ x, ‖(φ n - ψ) x‖ₑ ^ 2 = ∫⁻ x, ‖(s n)ᶜ.indicator ψ x‖ₑ ^ 2 := by
       intro n
       refine lintegral_congr_ae ?_
-      filter_upwards [coeFn_sub (φ n).val ψ.val, hφ n] with x h₁ h₂
+      filter_upwards [coeFn_sub (φ n) ψ, hφ n] with x h₁ h₂
       by_cases hx : x ∈ s n <;> simp [hx, h₁, h₂]
     simp_rw [h]
     rw [← MeasureTheory.lintegral_zero (α := Space d) (μ := volume)]
@@ -141,7 +138,7 @@ lemma mulOperator_hasDenseDomain {f : Space d → ℂ} (hf : AEStronglyMeasurabl
     · intro n
       filter_upwards with x
       by_cases hx : x ∈ s n <;> simp [hx]
-    · have : ∫⁻ x, ‖‖ψ x‖ ^ 2‖ₑ ≠ ⊤ := (memHS_iff.mp (coe_hilbertSpace_memHS ψ)).2.2.ne
+    · have : ∫⁻ x, ‖‖ψ x‖ ^ 2‖ₑ ≠ ⊤ := (memHS_iff.mp <| memHS_coe ψ).2.2.ne
       simp_all
     · filter_upwards with x
       rw [← zero_pow two_ne_zero, ← enorm_zero (E := ℂ)]
@@ -152,12 +149,12 @@ lemma mulOperator_hasDenseDomain {f : Space d → ℂ} (hf : AEStronglyMeasurabl
 
 open SchwartzMap SchwartzSubmodule in
 lemma mulOperator_domain_ge_of_hasTemperateGrowth
-    {f : Space d → ℂ} (hf : f.HasTemperateGrowth) : schwartzSubmodule d ≤ (𝓜 f).domain := by
+    {f : Space d → ℂ} (hf : f.HasTemperateGrowth) : SchwartzSubmodule d ≤ (𝓜 f).domain := by
   intro ψ hψ
   obtain ⟨g, hg⟩ := schwartzEquiv.surjective ⟨ψ, hψ⟩
   let w : 𝓢(Space d, ℂ) := smulLeftCLM ℂ f g
   let φ : SpaceDHilbertSpace d := schwartzEquiv w
-  refine memHS_of_ae φ (coe_hilbertSpace_memHS φ) ?_
+  refine (memHS_coe φ).ae_eq ?_
   filter_upwards [schwartzEquiv_coe_ae w, schwartzEquiv_coe_ae g] with x h₁ h₂
   simp [w, φ, h₁, ← h₂, hg, smulLeftCLM_apply_apply hf]
 
@@ -226,14 +223,14 @@ lemma mulOperator_adjoint_domain_le {f : Space d → ℂ} (hf : AEStronglyMeasur
     calc
       _ = ∫⁻ x, ‖‖(f • w n) x‖ ^ 2‖ₑ := by
         refine lintegral_congr_ae ?_
-        filter_upwards [coe_mk_ae (hw n)] with _ h
+        filter_upwards [coeFn_mk (hw n)] with _ h
         simp [φ, h]
       _ = ∫⁻ x in s n, ‖‖(f • w n) x‖ ^ 2‖ₑ :=
         (setLIntegral_eq_of_support_subset fun x hx ↦ by simp_all [w]).symm
     exact setLIntegral_congr_fun (hs_meas n) fun x hx ↦ by simp [w, hx, ← mul_assoc, ← pow_two]
   suffices ∀ n, ∫⁻ x in s n, ‖‖f x‖ ^ 2 * ‖ψ x‖ ^ 2‖ₑ ≤ ∫⁻ x, ‖‖ξ x‖ ^ 2‖ₑ by
     refine memHS_iff.mpr ⟨by measurability, by measurability, ?_⟩
-    refine lt_of_le_of_lt ?_ (memHS_iff.mp <| coe_hilbertSpace_memHS ξ).2.2
+    refine lt_of_le_of_lt ?_ (memHS_iff.mp <| memHS_coe ξ).2.2
     trans ⨆ n, ∫⁻ x in s n, ‖‖f x‖ ^ 2 * ‖ψ x‖ ^ 2‖ₑ
     · rw [← setLIntegral_univ, ← hs_univ,
         setLIntegral_iUnion_of_directed _ (directed_of_isDirected_le hs_mono)]
@@ -249,10 +246,10 @@ lemma mulOperator_adjoint_domain_le {f : Space d → ℂ} (hf : AEStronglyMeasur
           setLIntegral_eq_of_support_subset fun x hx ↦ by simp_all [w]
         _ = ∫⁻ x, ‖‖φ n x‖ ^ 2‖ₑ := by
           refine lintegral_congr_ae ?_
-          filter_upwards [coe_mk_ae (hw n)] with x h₁
+          filter_upwards [coeFn_mk (hw n)] with x h₁
           simp [φ, h₁]
-    · exact (memHS_iff.mp <| coe_hilbertSpace_memHS (φ n)).2.2.ne
-    · exact (memHS_iff.mp <| coe_hilbertSpace_memHS ξ).2.2.ne
+    · exact (memHS_iff.mp <| memHS_coe (φ n)).2.2.ne
+    · exact (memHS_iff.mp <| memHS_coe ξ).2.2.ne
     · suffices h : ∀ ψ : SpaceDHilbertSpace d, ‖ψ‖ ^ 2 = (∫⁻ x, ‖‖ψ x‖ ^ 2‖ₑ).toReal by
         simp only [← h, this]
       intro ψ
@@ -265,7 +262,7 @@ lemma mulOperator_adjoint_domain_le {f : Space d → ℂ} (hf : AEStronglyMeasur
     _ = ‖⟪ψ, 𝓜 f ⟨φ n, hφ n⟩⟫_ℂ‖ := by
       refine congrArg norm ?_
       refine integral_congr_ae ?_
-      filter_upwards [coe_mk_ae (hw n), mulOperator_apply_ae ⟨φ n, hφ n⟩] with x h₁ h₂
+      filter_upwards [coeFn_mk (hw n), mulOperator_apply_ae ⟨φ n, hφ n⟩] with x h₁ h₂
       by_cases hx : x ∈ s n
       · simp only [φ, h₁, h₂, inner_self_eq_norm_sq_to_K, coe_algebraMap, RCLike.inner_apply,
           Pi.smul_apply', smul_eq_mul]
@@ -322,7 +319,7 @@ lemma mulOperator_compRestricted_le (f g : Space d → ℂ) : 𝓜 f ∘ᵣ 𝓜
   constructor
   · intro ψ hψ
     obtain ⟨hψ, hgψ⟩ := mem_compRestricted_domain_iff.mp hψ
-    refine memHS_of_ae _ (mem_mulOperator_domain_iff.mp hgψ) ?_
+    refine (mem_mulOperator_domain_iff.mp hgψ).ae_eq ?_
     filter_upwards [mulOperator_apply_ae ⟨ψ, hψ⟩]
     simp_all [mul_assoc]
   · intro ψ φ hψφ
@@ -338,7 +335,7 @@ lemma mulOperator_compRestricted_eq (f : Space d → ℂ) {g : Space d → ℂ}
   refine eq_of_le_of_domain_eq hle ?_
   refine eq_of_le_of_ge hle.1 fun ψ hψ ↦ ?_
   refine mem_compRestricted_domain_iff.mpr ⟨h ▸ Submodule.mem_top, ?_⟩
-  refine memHS_of_ae _ (mem_mulOperator_domain_iff.mp hψ) ?_
+  refine (mem_mulOperator_domain_iff.mp hψ).ae_eq ?_
   filter_upwards [mulOperator_apply_ae ⟨ψ, h ▸ Submodule.mem_top⟩]
   simp_all [mul_assoc]
 

Physlib/QuantumMechanics/DDimensions/Operators/Position.lean

@@ -180,7 +180,7 @@ lemma radiusPowLM_apply_stronglyMeasurable {d : ℕ} (s : ℝ) (ψ : 𝓢(Space
 
 /-- `x ↦ ‖x‖ˢψ(x)` is square-integrable provided `s` is not too negative. -/
 lemma radiusPowLM_apply_memHS {d : ℕ} (s : ℝ) (ψ : 𝓢(Space d, ℂ)) (a : ℕ)
-    (hψ : ψ ∈ polyBddSchwartzMap d a) (h : 0 < d + 2 * (a + s)) :
+    (hψ : ψ ∈ PolyBddSchwartzMap d a) (h : 0 < d + 2 * (a + s)) :
     MemHS (𝐫 s ψ) := by
   rcases Nat.eq_zero_or_pos d with (rfl | hd)
   · simp only [MemHS, MemLp.of_discrete]
@@ -403,20 +403,20 @@ private lemma add_floor_toNat_pos_aux (d : ℕ) (s : ℝ) :
   linarith
 
 lemma radiusPowLM_apply_polyBddSchwartz_memHS {d : ℕ} {s : ℝ}
-    (ψ : polyBddSchwartzSubmodule d ⌊1 - d / 2 - s⌋.toNat) :
+    (ψ : PolyBddSchwartzSubmodule d ⌊1 - d / 2 - s⌋.toNat) :
     MemHS (𝐫[d] s (polyBddSchwartzEquiv.symm ψ)) :=
   let f := polyBddSchwartzEquiv.symm ψ
   radiusPowLM_apply_memHS s f.1 ⌊1 - d / 2 - s⌋.toNat f.2 (add_floor_toNat_pos_aux d s)
 
 lemma radiusPowOperator_domain_ge {d : ℕ} (s : ℝ) :
-    polyBddSchwartzSubmodule d ⌊1 - d / 2 - s⌋.toNat ≤ (radiusPowOperator s).domain := by
+    PolyBddSchwartzSubmodule d ⌊1 - d / 2 - s⌋.toNat ≤ (radiusPowOperator s).domain := by
   intro ψ hψ
   let f := polyBddSchwartzEquiv.symm ⟨ψ, hψ⟩
   apply mem_mulOperator_domain_iff.mpr
-  refine memHS_of_ae (𝐫 s f.1) ?_ ?_
-  · exact radiusPowLM_apply_memHS s f.1 _ f.2 (add_floor_toNat_pos_aux d s)
+  refine MemHS.ae_eq (f := 𝐫 s f.1) ?_ ?_
   · filter_upwards [polyBddSchwartzEquiv_coe_ae f]
     simp_all [f]
+  · exact radiusPowLM_apply_memHS s f.1 _ f.2 (add_floor_toNat_pos_aux d s)
 
 end
 end QuantumMechanics