diff --git a/Physlib/QuantumMechanics/DDimensions/Basic.lean b/Physlib/QuantumMechanics/DDimensions/Basic.lean index b1fbd1ff2..3c7f22b3a 100644 --- a/Physlib/QuantumMechanics/DDimensions/Basic.lean +++ b/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) /-! diff --git a/Physlib/QuantumMechanics/DDimensions/Operators/Momentum.lean b/Physlib/QuantumMechanics/DDimensions/Operators/Momentum.lean index e1b95f4c4..cd6fadb33 100644 --- a/Physlib/QuantumMechanics/DDimensions/Operators/Momentum.lean +++ b/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 diff --git a/Physlib/QuantumMechanics/DDimensions/Operators/Multiplication.lean b/Physlib/QuantumMechanics/DDimensions/Operators/Multiplication.lean index 090a9a5ab..67daf3b36 100644 --- a/Physlib/QuantumMechanics/DDimensions/Operators/Multiplication.lean +++ b/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] diff --git a/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean b/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean index e6d2308c2..faf088297 100644 --- a/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean +++ b/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 diff --git a/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean b/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean index 409906016..775b83bee 100644 --- a/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean +++ b/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean @@ -10,155 +10,162 @@ public import Mathlib.MeasureTheory.Function.L2Space public import Physlib.SpaceAndTime.Space.Module /-! -# Hilbert space for quantum mechanics on Space d +# Hilbert spaces for quantum mechanics on `Space d` + +## i. Overview + +## ii. Key results + +## iii. Table of contents + +- A. Definition +- B. Dual space +- C. Membership +- D. Construction of elements +- E. Coersions +- F. Misc. + +## iv. References -/ @[expose] public section +noncomputable section + namespace QuantumMechanics -noncomputable section +open Function InnerProductSpace MeasureTheory Measure Set + +/-! +## A. Definition +-/ /-- The Hilbert space for single-particle quantum mechanics on `Space d` is defined to be `L²(Space d, ℂ)`, the space of almost-everywhere equal equivalence classes of square-integrable functions from `Space d` to `ℂ`. -/ -abbrev SpaceDHilbertSpace (d : ℕ) := MeasureTheory.Lp (α := Space d) ℂ 2 +abbrev SpaceDHilbertSpace (d : ℕ) := Lp (α := Space d) ℂ 2 volume namespace SpaceDHilbertSpace -open MeasureTheory -open InnerProductSpace -/-- The anti-linear map from the Hilbert space to its dual. -/ -def toBra {d : ℕ} : SpaceDHilbertSpace d →ₛₗ[starRingEnd ℂ] (StrongDual ℂ (SpaceDHilbertSpace d)) := +variable {d : ℕ} {f g : Space d → ℂ} (ψ φ : SpaceDHilbertSpace d) + +variable {ψ φ} in +lemma ext_iff : ψ = φ ↔ ψ =ᵐ[volume] φ := Lp.ext_iff + +/-! +## B. Dual space +-/ + +/-- The anti-linear equivalence between `SpaceDHilbertSpace d` and its dual. + + This is the map that takes a ket to its corresponding bra and _vice versa_. -/ +def toBra : SpaceDHilbertSpace d ≃ₛₗ[starRingEnd ℂ] StrongDual ℂ (SpaceDHilbertSpace d) := toDual ℂ (SpaceDHilbertSpace d) @[simp] -lemma toBra_apply (f g : SpaceDHilbertSpace d) : toBra f g = ⟪f, g⟫_ℂ := rfl - -/-- The anti-linear map `toBra` taking a ket to its corresponding bra is surjective. -/ -lemma toBra_surjective : Function.Surjective (toBra (d := d)) := - (toDual ℂ (SpaceDHilbertSpace d)).surjective +lemma toBra_apply_apply : toBra ψ φ = ⟪ψ, φ⟫_ℂ := rfl -/-- The anti-linear map `toBra` taking a ket to its corresponding bra is injective. -/ -lemma toBra_injective : Function.Injective (toBra (d := d)) := by - intro f g h - simpa [toBra] using h +@[simp] +lemma toBra_symm_apply (f : StrongDual ℂ (SpaceDHilbertSpace d)) : ⟪toBra.symm f, ψ⟫_ℂ = f ψ := + toDual_symm_apply /-! -## Member of the Hilbert space as a property +## C. Membership -/ /-- The proposition `MemHS f` for a function `f : Space d → ℂ` is defined to be true if the function `f` can be lifted to the Hilbert space. -/ -def MemHS (f : Space d → ℂ) : Prop := MemLp f 2 - -lemma aeStronglyMeasurable_of_memHS {f : Space d → ℂ} (h : MemHS f) : AEStronglyMeasurable f := - MemLp.aestronglyMeasurable h - -/-- A function `f` satisfies `MemHS f` if and only if it is almost everywhere - strongly measurable and square integrable. -/ -lemma memHS_iff {f : Space d → ℂ} : MemHS f ↔ - AEStronglyMeasurable f ∧ Integrable (fun x ↦ ‖f x‖ ^ 2) := by - rw [MemHS, MemLp, and_congr_right] - intro h - rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top - (NeZero.ne' 2).symm ENNReal.top_ne_ofNat.symm] - simp only [ENNReal.toReal_ofNat, ENNReal.rpow_ofNat] - have h' : AEStronglyMeasurable (fun x ↦ ‖f x‖ ^ 2) := - AEStronglyMeasurable.pow (AEStronglyMeasurable.norm h) 2 - simp [Integrable, h', HasFiniteIntegral] +def MemHS (f : Space d → ℂ) : Prop := MemLp f 2 volume -@[simp] -lemma zero_memHS : MemHS (d := d) 0 := by - rw [memHS_iff] - simp only [Pi.ofNat_apply, norm_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, - integrable_fun_zero, and_true] - fun_prop +lemma memHS_coe : MemHS ψ := Lp.memLp ψ + +/-- A function `f` satisfies `MemHS f` if and only if it is a.e. strongly measurable + and square integrable. -/ +lemma memHS_iff : MemHS f ↔ AEStronglyMeasurable f ∧ Integrable (fun x ↦ ‖f x‖ ^ 2) := + and_congr_right fun h ↦ (and_iff_right h).symm.trans (memLp_two_iff_integrable_sq_norm h) + +lemma mem_iff {f : Space d →ₘ[volume] ℂ} : f ∈ SpaceDHilbertSpace d ↔ MemHS f := Lp.mem_Lp_iff_memLp @[simp] -lemma zero_fun_memHS : MemHS (fun _ : Space d ↦ (0 : ℂ)) := zero_memHS +lemma MemHS.zero : MemHS (0 : Space d → ℂ) := MemLp.zero + +lemma MemHS.neg (hf : MemHS f) : MemHS (-f) := MemLp.neg hf -lemma memHS_add {f g : Space d → ℂ} (hf : MemHS f) (hg : MemHS g) : MemHS (f + g) := - MemLp.add hf hg +lemma MemHS.add (hf : MemHS f) (hg : MemHS g) : MemHS (f + g) := MemLp.add hf hg -lemma memHS_const_smul {f : Space d → ℂ} {c : ℂ} (hf : MemHS f) : MemHS (c • f) := - MemLp.const_smul hf c +lemma MemHS.sub (hf : MemHS f) (hg : MemHS g) : MemHS (f - g) := MemLp.sub hf hg -lemma memHS_of_ae {g : Space d → ℂ} (f : Space d → ℂ) (hf : MemHS f) (hfg : f =ᵐ[volume] g) : - MemHS g := MemLp.ae_eq hfg hf +lemma MemHS.const_smul (c : ℂ) (hf : MemHS f) : MemHS (c • f) := MemLp.const_smul hf c + +lemma MemHS.ae_eq (hfg : f =ᵐ[volume] g) (hf : MemHS f) : MemHS g := MemLp.ae_eq hfg hf /-! -## Construction of elements of the Hilbert space +## D. Construction of elements -/ -lemma aeEqFun_mk_mem_iff (f : Space d → ℂ) (hf : AEStronglyMeasurable f volume) : - AEEqFun.mk f hf ∈ SpaceDHilbertSpace d ↔ MemHS f := by - rw [Lp.mem_Lp_iff_memLp] - exact memLp_congr_ae (AEEqFun.coeFn_mk f hf) +section + +variable (hf : MemHS f) (hg : MemHS g) /-- Given a function `f : Space d → ℂ` such that `MemHS f` is true via `hf`, - `SpaceDHilbertSpace.mk f` is the element of the Hilbert space defined by `f`. -/ -def mk {f : Space d → ℂ} (hf : MemHS f) : SpaceDHilbertSpace d := - ⟨AEEqFun.mk f hf.1, (aeEqFun_mk_mem_iff f hf.1).mpr hf⟩ + `mk hf` is the element of the Hilbert space defined by `f`. -/ +def mk : SpaceDHilbertSpace d := + ⟨AEEqFun.mk f hf.1, mem_iff.mpr <| hf.ae_eq (AEEqFun.coeFn_mk f hf.1).symm⟩ + +@[simp] +lemma mk_neg : mk hf.neg = -mk hf := rfl + +@[simp] +lemma mk_add : mk (hf.add hg) = mk hf + mk hg := rfl -lemma coe_hilbertSpace_memHS (f : SpaceDHilbertSpace d) : MemHS (f : Space d → ℂ) := by - rw [← aeEqFun_mk_mem_iff f (Lp.aestronglyMeasurable f)] - have hf : f = AEEqFun.mk f (Lp.aestronglyMeasurable f) := (AEEqFun.mk_coeFn _).symm - exact hf ▸ f.2 +@[simp] +lemma mk_sub : mk (hf.sub hg) = mk hf - mk hg := rfl + +@[simp] +lemma mk_const_smul (c : ℂ) : mk (hf.const_smul c) = c • mk hf := rfl -lemma mk_surjective (f : SpaceDHilbertSpace d) : - ∃ (g : Space d → ℂ) (hg : MemHS g), mk hg = f := by - use f, coe_hilbertSpace_memHS f - simp [mk] +lemma coeFn_mk : mk hf =ᵐ[volume] f := AEEqFun.coeFn_mk f hf.1 -lemma coe_mk_ae {f : Space d → ℂ} (hf : MemHS f) : (mk hf) =ᵐ[volume] f := - AEEqFun.coeFn_mk f hf.1 +lemma mk_eq_iff : mk hf = mk hg ↔ f =ᵐ[volume] g := by simp [mk] -lemma inner_mk_mk {f g : Space d → ℂ} (hf : MemHS f) (hg : MemHS g) : - ⟪mk hf, mk hg⟫_ℂ = ∫ x : Space d, starRingEnd ℂ (f x) * g x := by +lemma mk_surjective : ∃ (f : Space d → ℂ) (hf : MemHS f), mk hf = ψ := + ⟨ψ, memHS_coe ψ, by simp [mk]⟩ + +lemma inner_mk_mk : ⟪mk hf, mk hg⟫_ℂ = ∫ x, starRingEnd ℂ (f x) * g x := by apply integral_congr_ae - filter_upwards [coe_mk_ae hf, coe_mk_ae hg] with x hf hg - simp [hf, hg, mul_comm] + filter_upwards [coeFn_mk hf, coeFn_mk hg] + simp_all [mul_comm] -@[simp] -lemma eLpNorm_mk {f : Space d → ℂ} {hf : MemHS f} : eLpNorm (mk hf) 2 = eLpNorm f 2 := - eLpNorm_congr_ae (coe_mk_ae hf) - -lemma mem_iff {f : Space d → ℂ} (hf : AEStronglyMeasurable f volume) : - AEEqFun.mk f hf ∈ SpaceDHilbertSpace d ↔ Integrable (fun x ↦ ‖f x‖ ^ 2) := by - rw [Lp.mem_Lp_iff_memLp, MemLp, eLpNorm_aeeqFun] - have h1 := AEEqFun.aestronglyMeasurable (AEEqFun.mk f hf) - have h2 : AEStronglyMeasurable (fun x ↦ norm (f x) ^ 2) := - AEStronglyMeasurable.pow (continuous_norm.comp_aestronglyMeasurable hf) 2 - simp only [h1] - simp only [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top (NeZero.ne' 2).symm - (ENNReal.top_ne_ofNat).symm, ENNReal.toReal_ofNat, ENNReal.rpow_ofNat] - simp [h2, Integrable, HasFiniteIntegral] +end -@[simp] -lemma mk_add {f g : Space d → ℂ} {hf : MemHS f} {hg : MemHS g} : - mk (memHS_add hf hg) = mk hf + mk hg := rfl +/-! +## E. Coersions +-/ -@[simp] -lemma mk_const_smul {f : Space d → ℂ} {c : ℂ} {hf : MemHS f} : - mk (memHS_const_smul (c := c) hf) = c • mk hf := rfl +section + +variable (c : ℂ) (ψ φ : SpaceDHilbertSpace d) + +lemma coeFn_neg : ⇑(-ψ) =ᵐ[volume] -ψ := Lp.coeFn_neg _ -lemma mk_eq_iff {f g : Space d → ℂ} {hf : MemHS f} {hg : MemHS g} : - mk hf = mk hg ↔ f =ᵐ[volume] g := by simp [mk] +lemma coeFn_add : ⇑(ψ.val + φ.val) =ᵐ[volume] ψ + φ := Lp.coeFn_add _ _ -lemma ext_iff {f g : SpaceDHilbertSpace d} : - f = g ↔ (f : Space d → ℂ) =ᵐ[volume] (g : Space d → ℂ) := Lp.ext_iff +lemma coeFn_sub : ⇑(ψ.val - φ.val) =ᵐ[volume] ψ - φ := Lp.coeFn_sub _ _ + +lemma coeFn_smul : ⇑(c • ψ) =ᵐ[volume] c • ψ := Lp.coeFn_smul _ _ + +end /-! -## Limits +## F. Misc. -/ open Filter lemma tendsto_zero_iff_tendsto_zero_lintegral_enorm_sq - {d : ℕ} {α : Type*} {l : Filter α} {ψ : α → SpaceDHilbertSpace d} : - Tendsto ψ l (nhds 0) ↔ Tendsto (fun a ↦ ∫⁻ x : Space d, ‖ψ a x‖ₑ ^ 2) l (nhds 0) := by + {α : Type*} {l : Filter α} {ψ : α → SpaceDHilbertSpace d} : + Tendsto ψ l (nhds 0) ↔ Tendsto (fun a ↦ ∫⁻ x, ‖ψ a x‖ₑ ^ 2) l (nhds 0) := by trans Tendsto (fun a ↦ (∫⁻ x, ‖ψ a x‖ₑ ^ 2) ^ (2⁻¹ : ℝ)) l (nhds 0) · simp [tendsto_iff_edist_tendsto_0, edist_zero_right, Lp.enorm_def, eLpNorm, eLpNorm'] constructor <;> intro h @@ -168,5 +175,5 @@ lemma tendsto_zero_iff_tendsto_zero_lintegral_enorm_sq simp_all end SpaceDHilbertSpace -end end QuantumMechanics +end diff --git a/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/PolyBddSchwartzSubmodule.lean b/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/PolyBddSchwartzSubmodule.lean index c2644baa3..6ac8e891a 100644 --- a/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/PolyBddSchwartzSubmodule.lean +++ b/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/PolyBddSchwartzSubmodule.lean @@ -16,12 +16,12 @@ public import Mathlib.Analysis.Calculus.BumpFunction.InnerProduct In this module we define polynomially-bounded Schwartz submodules of `SpaceDHilbertSpace`. -For each `a : ℕ∞`, `polyBddSchwartzSubmodule d a` is the submodule corresponding to Schwartz +For each `a : ℕ∞`, `PolyBddSchwartzSubmodule d a` is the submodule corresponding to Schwartz maps `f` satisfying the polynomial growth bounds `‖x‖ ^ (-k) * ‖f x‖ ≤ Cₖ` for all `(k : ℕ) ≤ a`. In particular, for `a = ⊤` such a bound holds for all natural numbers. These serve as a natural domain for singular unbounded operators. For example, the `1/r` Coulomb -potential operator maps `polyBddSchwartzSubmodule d ⊤` to itself. In the same way that multiplying +potential operator maps `PolyBddSchwartzSubmodule d ⊤` to itself. In the same way that multiplying a Schwartz map by any polynomial in the coordinates results in a square-integrable function, polynomially-bounded Schwartz maps may be multiplied by Laurent polynomials and remain square-integrable (the precise condition depends on `d`, `a` and the negative degree of @@ -36,7 +36,7 @@ their being dense in `SpaceDHilbertSpace 0 ≅ ℂ`). ## ii. Key results -- `polyBddSchwartzSubmodule d (a : ℕ∞)`: Restriction of `schwartzSubmodule d` to those Schwartz maps +- `PolyBddSchwartzSubmodule d (a : ℕ∞)`: Restriction of `SchwartzSubmodule d` to those Schwartz maps which are bounded by powers of `‖x‖`. - `PolyBddSchwartzSubmodule.dense d a`: These submodules are dense in `SpaceDHilbertSpace`. @@ -68,7 +68,7 @@ open SchwartzSubmodule -/ /-- A function is a bounded Schwartz map if it is both Schwartz and bounded by powers of `‖x‖`. -/ -def polyBddSchwartzMap (d : ℕ) (a : ℕ∞) : Submodule ℂ 𝓢(Space d, ℂ) where +def PolyBddSchwartzMap (d : ℕ) (a : ℕ∞) : Submodule ℂ 𝓢(Space d, ℂ) where carrier := {f : 𝓢(Space d, ℂ) | ∀ k : ℕ, k ≤ a → ∃ C : ℝ, 0 < C ∧ ∀ x : Space d, ‖x‖ ^ (-k : ℤ) * ‖f x‖ ≤ C} add_mem' := by @@ -87,13 +87,13 @@ def polyBddSchwartzMap (d : ℕ) (a : ℕ∞) : Submodule ℂ 𝓢(Space d, ℂ) rw [smul_apply, norm_smul, mul_rotate', mul_comm ‖f x‖] exact le_trans (mul_le_mul_of_nonneg_left (hC x) (norm_nonneg c)) (by linarith) -/-- The continuous linear map `schwartzIncl` with domain restricted to `polyBddSchwartzMap d a`. -/ -def polyBddSchwartzIncl {d : ℕ} {a : ℕ∞} : polyBddSchwartzMap d a →L[ℂ] SpaceDHilbertSpace d := - ⟨schwartzIncl.domRestrict (polyBddSchwartzMap d a), +/-- The continuous linear map `schwartzIncl` with domain restricted to `PolyBddSchwartzMap d a`. -/ +def polyBddSchwartzIncl {d : ℕ} {a : ℕ∞} : PolyBddSchwartzMap d a →L[ℂ] SpaceDHilbertSpace d := + ⟨schwartzIncl.domRestrict (PolyBddSchwartzMap d a), schwartzIncl.continuous_domRestrict schwartzIncl.continuous _⟩ /-- The submodule of `SpaceDHilbertSpace d` corresponding to bounded Schwartz maps. -/ -abbrev polyBddSchwartzSubmodule (d : ℕ) (a : ℕ∞) : Submodule ℂ (SpaceDHilbertSpace d) := +abbrev PolyBddSchwartzSubmodule (d : ℕ) (a : ℕ∞) : Submodule ℂ (SpaceDHilbertSpace d) := (polyBddSchwartzIncl (a := a)).range lemma polyBddSchwartzIncl_injective (d : ℕ) (a : ℕ∞) : @@ -103,7 +103,7 @@ lemma polyBddSchwartzIncl_injective (d : ℕ) (a : ℕ∞) : /-- The linear equivalence between polynomially-bounded Schwartz maps and the corresponding submodule of the Hilbert space. -/ def polyBddSchwartzEquiv {d : ℕ} {a : ℕ∞} : - polyBddSchwartzMap d a ≃ₗ[ℂ] polyBddSchwartzSubmodule d a := + PolyBddSchwartzMap d a ≃ₗ[ℂ] PolyBddSchwartzSubmodule d a := LinearEquiv.ofInjective polyBddSchwartzIncl.toLinearMap (polyBddSchwartzIncl_injective d a) namespace PolyBddSchwartzSubmodule @@ -112,18 +112,18 @@ namespace PolyBddSchwartzSubmodule ## B. Coercions -/ -instance {d : ℕ} {a : ℕ∞} : CoeOut (polyBddSchwartzMap d a) 𝓢(Space d, ℂ) := ⟨fun f ↦ f.val⟩ +instance {d : ℕ} {a : ℕ∞} : CoeOut (PolyBddSchwartzMap d a) 𝓢(Space d, ℂ) := ⟨fun f ↦ f.val⟩ -instance {d : ℕ} {a : ℕ∞} : CoeFun (polyBddSchwartzMap d a) (fun _ ↦ Space d → ℂ) := +instance {d : ℕ} {a : ℕ∞} : CoeFun (PolyBddSchwartzMap d a) (fun _ ↦ Space d → ℂ) := ⟨fun f ↦ ⇑f.val⟩ @[simp] -lemma toFun_eq_coe {d : ℕ} {a : ℕ∞} (f : polyBddSchwartzMap d a) (x : Space d) : +lemma toFun_eq_coe {d : ℕ} {a : ℕ∞} (f : PolyBddSchwartzMap d a) (x : Space d) : f.val.toFun x = f.val x := rfl lemma polyBddSchwartzEquiv_symm_apply_coe {d : ℕ} {a : ℕ∞} - {ψ : schwartzSubmodule d} (hψ : ↑ψ ∈ polyBddSchwartzSubmodule d a) : + {ψ : SchwartzSubmodule d} (hψ : ↑ψ ∈ PolyBddSchwartzSubmodule d a) : (polyBddSchwartzEquiv.symm ⟨ψ, hψ⟩).val = schwartzEquiv.symm ψ := by apply schwartzEquiv.injective apply SetLike.coe_eq_coe.mp @@ -132,32 +132,32 @@ lemma polyBddSchwartzEquiv_symm_apply_coe {d : ℕ} {a : ℕ∞} rw [← hg, LinearEquiv.symm_apply_apply, LinearEquiv.apply_symm_apply, ← hg'] rfl -lemma polyBddSchwartzEquiv_coe_ae {d : ℕ} {a : ℕ∞} (f : polyBddSchwartzMap d a) : +lemma polyBddSchwartzEquiv_coe_ae {d : ℕ} {a : ℕ∞} (f : PolyBddSchwartzMap d a) : polyBddSchwartzEquiv f =ᵐ[volume] f.val := schwartzEquiv_coe_ae f.val /-! ### C. (In)equalities -/ -lemma polyBddSchwartzMap_zero_eq_top (d : ℕ) : polyBddSchwartzMap d 0 = ⊤ := by +lemma PolyBddSchwartzMap_zero_eq_top (d : ℕ) : PolyBddSchwartzMap d 0 = ⊤ := by ext f have := f.decay 0 0 - simp_all [polyBddSchwartzMap] + simp_all [PolyBddSchwartzMap] -lemma polyBddSchwartzMap_antitone (d : ℕ) {a b : ℕ∞} (h : a ≤ b) : - polyBddSchwartzMap d b ≤ polyBddSchwartzMap d a := fun _ hx k hk ↦ hx k (hk.trans h) +lemma PolyBddSchwartzMap_antitone (d : ℕ) {a b : ℕ∞} (h : a ≤ b) : + PolyBddSchwartzMap d b ≤ PolyBddSchwartzMap d a := fun _ hx k hk ↦ hx k (hk.trans h) -lemma of_zero_eq (d : ℕ) : polyBddSchwartzSubmodule d 0 = schwartzSubmodule d := by - simp [polyBddSchwartzSubmodule, polyBddSchwartzIncl, polyBddSchwartzMap_zero_eq_top] +lemma of_zero_eq (d : ℕ) : PolyBddSchwartzSubmodule d 0 = SchwartzSubmodule d := by + simp [PolyBddSchwartzSubmodule, polyBddSchwartzIncl, PolyBddSchwartzMap_zero_eq_top] -lemma le_schwartzSubmodule (d : ℕ) (a : ℕ∞) : polyBddSchwartzSubmodule d a ≤ schwartzSubmodule d := +lemma le_SchwartzSubmodule (d : ℕ) (a : ℕ∞) : PolyBddSchwartzSubmodule d a ≤ SchwartzSubmodule d := LinearMap.range_domRestrict_le_range _ _ lemma antitone (d : ℕ) {a b : ℕ∞} (h : a ≤ b) : - polyBddSchwartzSubmodule d b ≤ polyBddSchwartzSubmodule d a := by - simp only [polyBddSchwartzSubmodule, polyBddSchwartzIncl, + PolyBddSchwartzSubmodule d b ≤ PolyBddSchwartzSubmodule d a := by + simp only [PolyBddSchwartzSubmodule, polyBddSchwartzIncl, ContinuousLinearMap.toLinearMap_domRestrict, LinearMap.range_domRestrict] - exact Submodule.map_mono (polyBddSchwartzMap_antitone d h) + exact Submodule.map_mono (PolyBddSchwartzMap_antitone d h) /-! ### D. Density @@ -176,28 +176,28 @@ private lemma enorm_bump_mul_le_enorm {𝕜 E : Type*} [RCLike 𝕜] [NormedAddC exact abs_le_abs_of_nonneg f.nonneg f.le_one private lemma dense_zero_top : - Dense (polyBddSchwartzSubmodule 0 ⊤ : Set (SpaceDHilbertSpace 0)) := by - suffices polyBddSchwartzMap 0 ⊤ = ⊤ by - simp [polyBddSchwartzSubmodule, polyBddSchwartzIncl, this] + Dense (PolyBddSchwartzSubmodule 0 ⊤ : Set (SpaceDHilbertSpace 0)) := by + suffices PolyBddSchwartzMap 0 ⊤ = ⊤ by + simp [PolyBddSchwartzSubmodule, polyBddSchwartzIncl, this] refine Submodule.eq_top_iff'.mpr (fun f k hk ↦ ?_) refine ⟨1 + ‖f 0‖, by positivity, fun x ↦ ?_⟩ simp only [Space.point_dim_zero_eq, norm_zero, zpow_neg, zpow_natCast] rcases k with _ | k <;> simp [add_nonneg] -lemma dense_top (d : ℕ) : Dense (polyBddSchwartzSubmodule d ⊤ : Set (SpaceDHilbertSpace d)) := by +lemma dense_top (d : ℕ) : Dense (PolyBddSchwartzSubmodule d ⊤ : Set (SpaceDHilbertSpace d)) := by rcases eq_zero_or_pos d with (rfl | hd) - · -- `d = 0`: Every function `Space 0 ≅ {0} → ℂ` is in `polyBddSchwartzSubmodule 0 ⊤`. + · -- `d = 0`: Every function `Space 0 ≅ {0} → ℂ` is in `PolyBddSchwartzSubmodule 0 ⊤`. exact dense_zero_top - · -- `d > 0`: Construct a sequence in `polyBddSchwartzSubmodule d ⊤` which tends to `ξ` + · -- `d > 0`: Construct a sequence in `PolyBddSchwartzSubmodule d ⊤` which tends to `ξ` intro ξ apply mem_closure_iff_seq_limit.mpr - -- `ψₙ = [fₙ]` is a sequence in `schwartzSubmodule` which tends to `ξ` + -- `ψₙ = [fₙ]` is a sequence in `SchwartzSubmodule` which tends to `ξ` obtain ⟨ψ, hψ, hψξ⟩ := mem_closure_iff_seq_limit.mp (SchwartzSubmodule.dense d ξ) let f (n : ℕ) : 𝓢(Space d, ℂ) := schwartzEquiv.symm ⟨ψ n, hψ n⟩ -- `bₙ` is a sequence of bump functions with shrinking domain let b (n : ℕ) : ContDiffBump (0 : Space d) := ⟨(n + 1)⁻¹, 2 * (n + 1 : ℝ)⁻¹, by positivity, lt_two_mul_self Nat.inv_pos_of_nat⟩ - -- `φₙ = [bₙfₙ]` is a sequence in `schwartzSubmodule` which tends to `0` + -- `φₙ = [bₙfₙ]` is a sequence in `SchwartzSubmodule` which tends to `0` let g (n : ℕ) : 𝓢(Space d, ℂ) := smulLeftCLM ℂ (b n) (f n) let φ (n : ℕ) : SpaceDHilbertSpace d := schwartzIncl (g n) have hg (n : ℕ) (x : Space d) : g n x = b n x * f n x := by @@ -233,15 +233,15 @@ lemma dense_top (d : ℕ) : Dense (polyBddSchwartzSubmodule d ⊤ : Set (SpaceDH refine mk (f := s n) ⟨?_, ?_⟩ · exact (continuous_ofReal.comp (b n).continuous).aestronglyMeasurable.mul ξ.val.aestronglyMeasurable - · refine lt_of_le_of_lt ?_ (coe_hilbertSpace_memHS ξ).2 + · refine lt_of_le_of_lt ?_ (memHS_coe ξ).2 exact eLpNorm_mono_enorm (enorm_bump_mul_le_enorm (b n) ξ) have hψ_ae (n : ℕ) : ψ n =ᵐ[volume] f n := (schwartzEquiv_symm_coe_ae ⟨ψ n, hψ n⟩).symm have hφ_ae (n : ℕ) : φ n =ᵐ[volume] g n := schwartzEquiv_coe_ae (g n) - have hσ_ae (n : ℕ) : σ n =ᵐ[volume] s n := coe_mk_ae _ + have hσ_ae (n : ℕ) : σ n =ᵐ[volume] s n := coeFn_mk _ have hφσ_ae (n : ℕ) : (φ - σ) n =ᵐ[volume] g n - s n := - (AEEqFun.coeFn_sub (φ n).val (σ n).val).trans <| (hφ_ae n).sub (hσ_ae n) + (coeFn_sub (φ n) (σ n)).trans <| (hφ_ae n).sub (hσ_ae n) have hψξ_ae (n : ℕ) : ψ n - ξ =ᵐ[volume] f n - ξ := - (AEEqFun.coeFn_sub (ψ n).val ξ.val).trans <| (hψ_ae n).sub EventuallyEq.rfl + (coeFn_sub (ψ n) ξ).trans <| (hψ_ae n).sub EventuallyEq.rfl refine tendsto_of_sub_tendsto_zero (f := σ) 0 ?_ ?_ · -- `σ = bₙξ → 0` since the norms are bounded by the integral of `‖ξ‖²` (independent of `n`!) -- on a domain which tends to zero @@ -284,7 +284,7 @@ lemma dense_top (d : ℕ) : Dense (polyBddSchwartzSubmodule d ⊤ : Set (SpaceDH simp_rw [h, h', Pi.sub_apply, hg, s, ← mul_sub] exact ENNReal.pow_le_pow_left <| enorm_bump_mul_le_enorm (b n) (fun x ↦ f n x - ξ x) x -lemma dense (d : ℕ) (a : ℕ∞) : Dense (polyBddSchwartzSubmodule d a : Set (SpaceDHilbertSpace d)) := +lemma dense (d : ℕ) (a : ℕ∞) : Dense (PolyBddSchwartzSubmodule d a : Set (SpaceDHilbertSpace d)) := (dense_top d).mono (antitone d le_top) end PolyBddSchwartzSubmodule diff --git a/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/SchwartzSubmodule.lean b/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/SchwartzSubmodule.lean index abf1229aa..b8ae0a8c2 100644 --- a/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/SchwartzSubmodule.lean +++ b/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/SchwartzSubmodule.lean @@ -17,7 +17,7 @@ In this module we define the Schwartz submodule of `SpaceDHilbertSpace`. ## ii. Key results -- `schwartzSubmodule d`: Submodule of `SpaceDHilbertSpace d` consisting of the L² equivalence +- `SchwartzSubmodule d`: Submodule of `SpaceDHilbertSpace d` consisting of the L² equivalence classes of Schwartz maps `𝓢(Space d, ℂ)`. ## iii. Table of contents @@ -51,22 +51,22 @@ variable {d : ℕ} def schwartzIncl : 𝓢(Space d, ℂ) →L[ℂ] SpaceDHilbertSpace d := toLpCLM ℂ (E := Space d) ℂ 2 /-- The submodule of `SpaceDHilbertSpace d` corresponding to Schwartz maps. -/ -abbrev schwartzSubmodule (d : ℕ) := (schwartzIncl (d := d)).range +abbrev SchwartzSubmodule (d : ℕ) := (schwartzIncl (d := d)).range /-- The linear equivalence between the Schwartz maps `𝓢(Space d, ℂ)` and the Schwartz submodule of `SpaceDHilbertSpace d`. -/ -def schwartzEquiv : 𝓢(Space d, ℂ) ≃ₗ[ℂ] schwartzSubmodule d := +def schwartzEquiv : 𝓢(Space d, ℂ) ≃ₗ[ℂ] SchwartzSubmodule d := LinearEquiv.ofInjective schwartzIncl.toLinearMap (injective_toLp (E := Space d) 2) namespace SchwartzSubmodule -variable (f g : 𝓢(Space d, ℂ)) (ψ : schwartzSubmodule d) +variable (f g : 𝓢(Space d, ℂ)) (ψ : SchwartzSubmodule d) /-! ## B. Coercions -/ -instance : CoeFun (schwartzSubmodule d) fun _ ↦ Space d → ℂ := ⟨fun ψ ↦ ψ.val⟩ +instance : CoeFun (SchwartzSubmodule d) fun _ ↦ Space d → ℂ := ⟨fun ψ ↦ ψ.val⟩ lemma schwartzEquiv_apply_coe : ↑(schwartzEquiv f) = schwartzIncl f := by simp [schwartzEquiv] @@ -84,7 +84,7 @@ lemma schwartzEquiv_ae_eq (h : schwartzEquiv f =ᵐ[volume] schwartzEquiv g) : f -/ @[simp] -lemma zero_eq_top : schwartzSubmodule 0 = ⊤ := by +lemma zero_eq_top : SchwartzSubmodule 0 = ⊤ := by ext ψ simp only [LinearMap.mem_range, ContinuousLinearMap.coe_coe, Submodule.mem_top, iff_true] let g : 𝓢(Space 0, ℂ) := { @@ -104,7 +104,7 @@ lemma zero_eq_top : schwartzSubmodule 0 = ⊤ := by rw [← schwartzEquiv_apply_coe, hg, Space.point_dim_zero_eq x] rfl -lemma dense (d : ℕ) : Dense (schwartzSubmodule d : Set (SpaceDHilbertSpace d)) := +lemma dense (d : ℕ) : Dense (SchwartzSubmodule d : Set (SpaceDHilbertSpace d)) := denseRange_toLpCLM ENNReal.top_ne_ofNat.symm lemma schwartzEquiv_inner :