Merge pull request #351 from HEPLean/JTS/QuantumMechanics

refactor: Multigoal proof

PhysLean/PerturbationTheory/Koszul/KoszulSign.lean

@@ -73,17 +73,15 @@ lemma koszulSign_erase_boson {𝓕 : Type} (q : 𝓕 → FieldStatistic) (le : 
     simp only [List.length_cons, Fin.zero_eta, List.get_eq_getElem, Fin.val_zero,
       List.getElem_cons_zero, Fin.isValue, List.eraseIdx_zero, List.tail_cons, koszulSign]
     intro h
-    rw [koszulSignInsert_boson]
+    rw [koszulSignInsert_boson _ _ _ h]
     simp only [one_mul]
-    exact h
   | φ :: φs, ⟨n + 1, h⟩ => by
     simp only [List.length_cons, List.get_eq_getElem, List.getElem_cons_succ, Fin.isValue,
       List.eraseIdx_cons_succ]
     intro h'
-    rw [koszulSign, koszulSign, koszulSign_erase_boson q le φs ⟨n, Nat.succ_lt_succ_iff.mp h⟩]
+    rw [koszulSign, koszulSign, koszulSign_erase_boson q le φs ⟨n, Nat.succ_lt_succ_iff.mp h⟩ h']
     congr 1
     rw [koszulSignInsert_erase_boson q le φ φs ⟨n, Nat.succ_lt_succ_iff.mp h⟩ h']
-    exact h'
 
 lemma koszulSign_insertIdx [IsTotal 𝓕 le] [IsTrans 𝓕 le] (φ : 𝓕) :
     (φs : List 𝓕) → (n : ℕ) → (hn : n ≤ φs.length) →
@@ -101,7 +99,7 @@ lemma koszulSign_insertIdx [IsTotal 𝓕 le] [IsTrans 𝓕 le] (φ : 𝓕) :
     simp only [List.insertIdx_zero, List.insertionSort, List.length_cons, Fin.zero_eta]
     rw [koszulSign]
     trans koszulSign q le (φ1 :: φs) * koszulSignInsert q le φ (φ1 :: φs)
-    ring
+    · ring
     simp only [insertionSortEquiv, List.length_cons, Nat.succ_eq_add_one, List.insertionSort,
       orderedInsertEquiv, OrderIso.toEquiv_symm, Fin.symm_castOrderIso,
       PhysLean.Fin.equivCons_trans,
@@ -123,7 +121,7 @@ lemma koszulSign_insertIdx [IsTotal 𝓕 le] [IsTrans 𝓕 le] (φ : 𝓕) :
     conv_lhs =>
       rw [List.insertIdx_succ_cons]
       rw [koszulSign]
-    rw [koszulSign_insertIdx]
+    rw [koszulSign_insertIdx _ _ _ (Nat.le_of_lt_succ h)]
     conv_rhs =>
       rhs
       simp only [List.insertIdx_succ_cons]
@@ -154,7 +152,7 @@ lemma koszulSign_insertIdx [IsTotal 𝓕 le] [IsTrans 𝓕 le] (φ : 𝓕) :
       ⟨n, hnsL⟩
     let nro : Fin (rs.length + 1) :=
       ⟨↑(orderedInsertPos le rs φ1), orderedInsertPos_lt_length le rs φ1⟩
-    rw [koszulSignInsert_insertIdx, koszulSignInsert_cons]
+    rw [koszulSignInsert_insertIdx _ _ _ _ _ _ (Nat.le_of_lt_succ h), koszulSignInsert_cons]
     trans koszulSignInsert q le φ1 φs * (koszulSignCons q le φ1 φ *
       𝓢(q φ, ofList q (rs.take ni)))
     · simp only [rs, ni]
@@ -189,13 +187,11 @@ lemma koszulSign_insertIdx [IsTotal 𝓕 le] [IsTrans 𝓕 le] (φ : 𝓕) :
       rw [exchangeSign_symm]
     · simp only [hn, ↓reduceIte, Fin.val_succ]
       rw [ofList_take_insertIdx_le, map_mul, ← mul_assoc]
-      congr 1
-      rw [exchangeSign_mul_self, koszulSignCons]
-      simp only [hc2 hn, ↓reduceIte]
-      exact Nat.le_of_not_lt hn
-      exact Nat.le_of_lt_succ (orderedInsertPos_lt_length le rs φ1)
-    · exact Nat.le_of_lt_succ h
-    · exact Nat.le_of_lt_succ h
+      · congr 1
+        rw [exchangeSign_mul_self, koszulSignCons]
+        simp only [hc2 hn, ↓reduceIte]
+      · exact Nat.le_of_not_lt hn
+      · exact Nat.le_of_lt_succ (orderedInsertPos_lt_length le rs φ1)
 
 lemma insertIdx_eraseIdx {I : Type} : (n : ℕ) → (r : List I) → (hn : n < r.length) →
     List.insertIdx n (r.get ⟨n, hn⟩) (r.eraseIdx n) = r
@@ -292,7 +288,7 @@ lemma koszulSign_eq_rel_eq_stat_append {ψ φ : 𝓕} [IsTrans 𝓕 le]
   simp only [koszulSign, ← mul_assoc]
   trans 1 * koszulSign q le φs
   swap
-  simp only [one_mul]
+  · simp only [one_mul]
   congr
   simp only [koszulSignInsert, ite_mul, neg_mul]
   simp_all only [and_self, ite_true]
@@ -311,13 +307,9 @@ lemma koszulSign_eq_rel_eq_stat {ψ φ : 𝓕} [IsTrans 𝓕 le]
     simp only [mul_eq_mul_right_iff]
     left
     trans koszulSignInsert q le φ'' (φ :: ψ :: (φs' ++ φs))
-    apply koszulSignInsert_eq_perm
-    refine List.Perm.symm (List.perm_cons_append_cons φ ?_)
-    exact List.Perm.symm List.perm_middle
-    rw [koszulSignInsert_eq_remove_same_stat_append q le]
-    exact h1
-    exact h2
-    exact hq
+    · apply koszulSignInsert_eq_perm
+      exact (List.perm_cons_append_cons φ List.perm_middle.symm).symm
+    · rw [koszulSignInsert_eq_remove_same_stat_append q le h1 h2 hq]
 
 lemma koszulSign_of_sorted : (φs : List 𝓕)
     → (hs : List.Sorted le φs) → koszulSign q le φs = 1
@@ -348,9 +340,9 @@ lemma koszulSign_of_append_eq_insertionSort_left [IsTotal 𝓕 le] [IsTrans 𝓕
         List.insertIdx (List.insertionSort le φs).length φ (List.insertionSort le φs ++ φs') := by
       rw [insertIdx_length_fst_append]
     rw [h1, h2]
-    rw [koszulSign_insertIdx]
+    rw [koszulSign_insertIdx _ _ _ _ _ (by simp)]
     simp only [instCommGroup.eq_1, List.take_left', List.length_insertionSort]
-    rw [koszulSign_insertIdx]
+    rw [koszulSign_insertIdx _ _ _ _ _ (by simp)]
     simp only [mul_assoc, instCommGroup.eq_1, List.length_insertionSort, List.take_left',
       ofList_insertionSort, mul_eq_mul_left_iff]
     left
@@ -376,8 +368,6 @@ lemma koszulSign_of_append_eq_insertionSort_left [IsTotal 𝓕 le] [IsTrans 𝓕
       rw [insertIdx_length_fst_append]
       symm
       apply insertionSort_insertionSort_append
-    · simp
-    · simp
 
 lemma koszulSign_of_append_eq_insertionSort [IsTotal 𝓕 le] [IsTrans 𝓕 le] : (φs'' φs φs' : List 𝓕) →
     koszulSign q le (φs'' ++ φs ++ φs') =
@@ -419,8 +409,8 @@ lemma koszulSign_perm_eq_append [IsTrans 𝓕 le] (φ : 𝓕) (φs φs' φs2 : L
   · intro x y l h
     simp_all only [List.mem_cons, forall_eq_or_imp, List.cons_append]
     apply Wick.koszulSign_swap_eq_rel_cons
-    exact IsTrans.trans y φ x h.1.2 h.2.1.1
-    exact IsTrans.trans x φ y h.2.1.2 h.1.1
+    · exact IsTrans.trans y φ x h.1.2 h.2.1.1
+    · exact IsTrans.trans x φ y h.2.1.2 h.1.1
   · intro l1 l2 l3 h1 h2 ih1 ih2 h
     simp_all only [and_self, implies_true, nonempty_prop, forall_const, motive]
     refine (ih2 ?_)

PhysLean/PerturbationTheory/Koszul/KoszulSignInsert.lean

@@ -92,8 +92,8 @@ lemma koszulSignInsert_eq_filter (φ : 𝓕) : (φs : List 𝓕) →
       simp only [Fin.isValue, h, ↓reduceIte]
       rw [koszulSignInsert_eq_filter]
       congr
-      simp only [decide_not]
-      simp
+      · simp only [decide_not]
+      · simp
 
 lemma koszulSignInsert_eq_cons [IsTotal 𝓕 le] (φ : 𝓕) (φs : List 𝓕) :
     koszulSignInsert q le φ φs = koszulSignInsert q le φ (φ :: φs) := by
@@ -131,10 +131,10 @@ lemma koszulSignInsert_eq_grade (φ : 𝓕) (φs : List 𝓕) :
           simpa [ofList] using ih
       · simp [hr1]
     · rw [List.filter_cons_of_neg]
-      simp only [decide_not, Fin.isValue]
-      rw [koszulSignInsert_eq_filter] at ih
-      simpa [ofList] using ih
-      simpa using hr1
+      · simp only [decide_not, Fin.isValue]
+        rw [koszulSignInsert_eq_filter] at ih
+        simpa [ofList] using ih
+      · simpa using hr1
 
 lemma koszulSignInsert_eq_perm (φs φs' : List 𝓕) (φ : 𝓕) (h : φs.Perm φs') :
     koszulSignInsert q le φ φs = koszulSignInsert q le φ φs' := by

PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Basic.lean

@@ -78,14 +78,14 @@ variable (Q : HarmonicOscillator)
 @[simp]
 lemma m_mul_ω_div_two_ℏ_pos : 0 < Q.m * Q.ω / (2 * Q.ℏ) := by
   apply div_pos
-  exact mul_pos Q.hm Q.hω
-  exact mul_pos (by norm_num) Q.hℏ
+  · exact mul_pos Q.hm Q.hω
+  · exact mul_pos (by norm_num) Q.hℏ
 
 @[simp]
 lemma m_mul_ω_div_ℏ_pos : 0 < Q.m * Q.ω / Q.ℏ := by
   apply div_pos
-  exact mul_pos Q.hm Q.hω
-  exact Q.hℏ
+  · exact mul_pos Q.hm Q.hω
+  · exact Q.hℏ
 
 lemma m_ne_zero : Q.m ≠ 0 := by
   have h1 := Q.hm

PhysLean/QuantumMechanics/OneDimension/HarmonicOscillator/Completeness.lean

@@ -52,11 +52,11 @@ lemma mul_eigenfunction_integrable (f : ℝ → ℂ) (hf : MemHS f) :
     funext x
     simp
 
-lemma mul_physHermiteFun_integrable (f : ℝ → ℂ) (hf : MemHS f) (n : ℕ) :
-    MeasureTheory.Integrable (fun x => (physHermiteFun n (√(Q.m * Q.ω / Q.ℏ) * x)) *
+lemma mul_physHermite_integrable (f : ℝ → ℂ) (hf : MemHS f) (n : ℕ) :
+    MeasureTheory.Integrable (fun x => (physHermite n (√(Q.m * Q.ω / Q.ℏ) * x)) *
       (f x * ↑(Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ))))) := by
   have h2 : (1 / ↑√(2 ^ n * ↑n !) * ↑√√(Q.m * Q.ω / (Real.pi * Q.ℏ)) : ℂ) • (fun (x : ℝ) =>
-      (physHermiteFun n (√(Q.m * Q.ω / Q.ℏ) * x) *
+      (physHermite n (√(Q.m * Q.ω / Q.ℏ) * x) *
       (f x * Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ))))) = fun x =>
       Q.eigenfunction n x * f x := by
     funext x
@@ -67,7 +67,7 @@ lemma mul_physHermiteFun_integrable (f : ℝ → ℂ) (hf : MemHS f) (n : ℕ) :
   have h1 := Q.mul_eigenfunction_integrable f hf (n := n)
   rw [← h2] at h1
   rw [IsUnit.integrable_smul_iff] at h1
-  exact h1
+  · exact h1
   simp only [ofNat_nonneg, pow_nonneg, Real.sqrt_mul, Complex.ofReal_mul, one_div, mul_inv_rev,
     isUnit_iff_ne_zero, ne_eq, _root_.mul_eq_zero, inv_eq_zero, Complex.ofReal_eq_zero, cast_nonneg,
     Real.sqrt_eq_zero, cast_eq_zero, pow_eq_zero_iff', OfNat.ofNat_ne_zero, false_and, or_false,
@@ -80,14 +80,14 @@ lemma mul_physHermiteFun_integrable (f : ℝ → ℂ) (hf : MemHS f) (n : ℕ) :
     · apply mul_pos Real.pi_pos Q.hℏ
 
 lemma mul_polynomial_integrable (f : ℝ → ℂ) (hf : MemHS f) (P : Polynomial ℤ) :
-    MeasureTheory.Integrable (fun x => ((fun x => P.aeval x) (√(Q.m * Q.ω / Q.ℏ) * x)) *
+    MeasureTheory.Integrable (fun x => (P (√(Q.m * Q.ω / Q.ℏ) * x)) *
       (f x * Real.exp (- Q.m * Q.ω * x^2 / (2 * Q.ℏ)))) volume := by
-  have h1 := polynomial_mem_physHermiteFun_span P
+  have h1 := polynomial_mem_physHermite_span P
   rw [Finsupp.mem_span_range_iff_exists_finsupp] at h1
   obtain ⟨a, ha⟩ := h1
-  have h2 : (fun x => ↑((fun x => P.aeval x) (√(Q.m * Q.ω / Q.ℏ) * x)) *
+  have h2 : (fun x => ↑(P (√(Q.m * Q.ω / Q.ℏ) * x)) *
     (f x * ↑(Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ)))))
-    = (fun x => ∑ r ∈ a.support, a r * (physHermiteFun r (√(Q.m * Q.ω / Q.ℏ) * x)) *
+    = (fun x => ∑ r ∈ a.support, a r * (physHermite r (√(Q.m * Q.ω / Q.ℏ) * x)) *
     (f x * Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ)))) := by
     funext x
     rw [← ha]
@@ -100,9 +100,9 @@ lemma mul_polynomial_integrable (f : ℝ → ℂ) (hf : MemHS f) (P : Polynomial
   intro i hi
   simp only [mul_assoc]
   have hf' : (fun a_1 =>
-    ↑(a i) * (↑(physHermiteFun i (√(Q.m * Q.ω / Q.ℏ) * a_1)) *
+    ↑(a i) * (↑(physHermite i (√(Q.m * Q.ω / Q.ℏ) * a_1)) *
     (f a_1 * ↑(Real.exp (- Q.m * (Q.ω * a_1 ^ 2) / (2 * Q.ℏ))))))
-    = fun x => (a i) • ((physHermiteFun i (√(Q.m * Q.ω / Q.ℏ) * x)) *
+    = fun x => (a i) • ((physHermite i (√(Q.m * Q.ω / Q.ℏ) * x)) *
       (f x * ↑(Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ))))) := by
     funext x
     simp only [neg_mul, Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg,
@@ -112,7 +112,7 @@ lemma mul_polynomial_integrable (f : ℝ → ℂ) (hf : MemHS f) (P : Polynomial
     simp_all
   rw [hf']
   apply MeasureTheory.Integrable.smul
-  exact Q.mul_physHermiteFun_integrable f hf i
+  exact Q.mul_physHermite_integrable f hf i
 
 lemma mul_power_integrable (f : ℝ → ℂ) (hf : MemHS f) (r : ℕ) :
     MeasureTheory.Integrable (fun x => x ^ r *
@@ -130,8 +130,9 @@ lemma mul_power_integrable (f : ℝ → ℂ) (hf : MemHS f) (r : ℕ) :
         Complex.ofReal_pow, Complex.ofReal_ofNat, Pi.smul_apply, smul_eq_mul]
       ring
     rw [h2] at h1
-    rw [IsUnit.integrable_smul_iff] at h1
-    simpa using h1
+    suffices h2 : IsUnit (↑(√(Q.m * Q.ω / Q.ℏ) ^ r : ℂ)) by
+      rw [IsUnit.integrable_smul_iff h2] at h1
+      simpa using h1
     simp only [isUnit_iff_ne_zero, ne_eq, pow_eq_zero_iff', Complex.ofReal_eq_zero, not_and,
       Decidable.not_not]
     have h1 : √(Q.m * Q.ω / Q.ℏ) ≠ 0 := by
@@ -142,7 +143,7 @@ lemma mul_power_integrable (f : ℝ → ℂ) (hf : MemHS f) (r : ℕ) :
     simp [h1]
   · simp only [ne_eq, Decidable.not_not] at hr
     subst hr
-    simpa using Q.mul_physHermiteFun_integrable f hf 0
+    simpa using Q.mul_physHermite_integrable f hf 0
 
 /-!
 
@@ -164,16 +165,16 @@ local notation "hm" => Q.hm
 local notation "hℏ" => Q.hℏ
 local notation "hω" => Q.hω
 
-lemma orthogonal_physHermiteFun_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
+lemma orthogonal_physHermite_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
     (hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n), HilbertSpace.mk hf⟫_ℂ = 0)
     (n : ℕ) :
-    ∫ (x : ℝ), (physHermiteFun n (√(Q.m * Q.ω / Q.ℏ) * x)) *
+    ∫ (x : ℝ), (physHermite n (√(Q.m * Q.ω / Q.ℏ) * x)) *
     (f x * ↑(Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ))))
     = 0 := by
   have h1 := Q.orthogonal_eigenfunction_of_mem_orthogonal f hf hOrth n
   have h2 : (fun (x : ℝ) =>
           (1 / ↑√(2 ^ n * ↑n !) * ↑√√(Q.m * Q.ω / (Real.pi * Q.ℏ)) : ℂ) *
-            (physHermiteFun n (√(Q.m * Q.ω / Q.ℏ) * x) * f x *
+            (physHermite n (√(Q.m * Q.ω / Q.ℏ) * x) * f x *
             Real.exp (- Q.m * Q.ω * x ^ 2 / (2 * Q.ℏ))))
     = fun x => Q.eigenfunction n x * f x := by
     funext x
@@ -207,14 +208,14 @@ lemma orthogonal_physHermiteFun_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS
 lemma orthogonal_polynomial_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
     (hOrth : ∀ n : ℕ, ⟪HilbertSpace.mk (Q.eigenfunction_memHS n), HilbertSpace.mk hf⟫_ℂ = 0)
     (P : Polynomial ℤ) :
-    ∫ x : ℝ, ((fun x => P.aeval x) (√(m * ω / ℏ) * x)) *
+    ∫ x : ℝ, (P (√(m * ω / ℏ) * x)) *
       (f x * Real.exp (- m * ω * x^2 / (2 * ℏ))) = 0 := by
-  have h1 := polynomial_mem_physHermiteFun_span P
+  have h1 := polynomial_mem_physHermite_span P
   rw [Finsupp.mem_span_range_iff_exists_finsupp] at h1
   obtain ⟨a, ha⟩ := h1
-  have h2 : (fun x => ↑((fun x => P.aeval x) (√(m * ω / ℏ) * x)) *
+  have h2 : (fun x => ↑(P (√(m * ω / ℏ) * x)) *
     (f x * ↑(Real.exp (-m * ω * x ^ 2 / (2 * ℏ)))))
-    = (fun x => ∑ r ∈ a.support, a r * (physHermiteFun r (√(m * ω / ℏ) * x)) *
+    = (fun x => ∑ r ∈ a.support, a r * (physHermite r (√(m * ω / ℏ) * x)) *
     (f x * Real.exp (-m * ω * x ^ 2 / (2 * ℏ)))) := by
     funext x
     rw [← ha]
@@ -231,7 +232,7 @@ lemma orthogonal_polynomial_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
     rw [integral_mul_left]
     simp only [_root_.mul_eq_zero, Complex.ofReal_eq_zero]
     right
-    rw [← Q.orthogonal_physHermiteFun_of_mem_orthogonal f hf hOrth x]
+    rw [← Q.orthogonal_physHermite_of_mem_orthogonal f hf hOrth x]
     congr
     funext x
     simp only [neg_mul, Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg,
@@ -243,9 +244,9 @@ lemma orthogonal_polynomial_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
     ring
   · /- Integrablility -/
     intro i hi
-    have hf' : (fun x => ↑(a i) * ↑(physHermiteFun i (√(m * ω / ℏ) * x)) *
+    have hf' : (fun x => ↑(a i) * ↑(physHermite i (√(m * ω / ℏ) * x)) *
         (f x * ↑(Real.exp (-m * ω * x ^ 2 / (2 * ℏ)))))
-        = a i • (fun x => (physHermiteFun i (√(m * ω / ℏ) * x)) *
+        = a i • (fun x => (physHermite i (√(m * ω / ℏ) * x)) *
         (f x * ↑(Real.exp (-m * ω * x ^ 2 / (2 * ℏ))))) := by
       funext x
       simp only [neg_mul, Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg,
@@ -254,7 +255,7 @@ lemma orthogonal_polynomial_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
       ring
     rw [hf']
     apply Integrable.smul
-    exact Q.mul_physHermiteFun_integrable f hf i
+    exact Q.mul_physHermite_integrable f hf i
 
 /-- If `f` is a function `ℝ → ℂ` satisfying `MemHS f` such that it is orthogonal
   to all `eigenfunction n` then it is orthogonal to
@@ -296,7 +297,7 @@ lemma orthogonal_power_of_mem_orthogonal (f : ℝ → ℂ) (hf : MemHS f)
     subst hr
     simp only [pow_zero, neg_mul, Complex.ofReal_exp, Complex.ofReal_div, Complex.ofReal_neg,
       Complex.ofReal_mul, Complex.ofReal_pow, Complex.ofReal_ofNat, one_mul]
-    rw [← Q.orthogonal_physHermiteFun_of_mem_orthogonal f hf hOrth 0]
+    rw [← Q.orthogonal_physHermite_of_mem_orthogonal f hf hOrth 0]
     congr
     funext x
     simp