one_third_in_jain_sequence

formal source

 121  omega
 122
 123/-- The ν = 1/3 Laughlin state is in the Jain sequence (m=1, p=1, plus). -/
 124theorem one_third_in_jain_sequence :
 125    jain_fraction 1 1 true = 1/3 := by
 126  unfold jain_fraction
 127  norm_num
 128
 129/-- The ν = 2/5 state is in the Jain sequence (m=1, p=2, plus). -/
 130theorem two_fifth_in_jain_sequence :
 131    jain_fraction 2 1 true = 2/5 := by
 132  unfold jain_fraction
 133  norm_num
 134
 135/-! ## Laughlin Quasi-particle Charge -/
 136
 137/-- At filling ν = 1/q, quasi-particles carry fractional charge e/q. -/
 138def laughlin_quasi_charge (q : ℕ) : ℚ := 1 / q
 139
 140/-- At ν = 1/3: quasi-particle charge = e/3. -/
 141theorem laughlin_charge_one_third :
 142    laughlin_quasi_charge 3 = 1/3 := by
 143  simp [laughlin_quasi_charge]
 144
 145/-- Quasi-particle charge is smaller for larger q. -/
 146theorem quasi_charge_decreasing (q₁ q₂ : ℕ) (h1 : 0 < q₁) (h2 : 0 < q₂) (h : q₁ < q₂) :
 147    laughlin_quasi_charge q₂ < laughlin_quasi_charge q₁ := by
 148  unfold laughlin_quasi_charge
 149  have hq1 : (0 : ℚ) < q₁ := by exact_mod_cast h1
 150  have hq2 : (0 : ℚ) < q₂ := by exact_mod_cast h2
 151  have hlt : (q₁ : ℚ) < q₂ := by exact_mod_cast h
 152  exact div_lt_div_of_pos_left one_pos hq1 hlt
 153
 154/-! ## Exchange Statistics in FQHE -/