Imports
The tight binding chain
i. Overview
The tight binding chain corresponds to an electron in motion
in a 1d solid with the assumption the electron can sit only on the atoms of the solid.
The solid is assumed to consist of N sites with a separation of a between them
Mathematically, the tight binding chain corresponds to a
QM problem located on a lattice with only self and nearest neighbour interactions,
with periodic boundary conditions.
ii. Key results
TightBindingChain : The physical parameters making up the tight binding chain.
localizedState : The orthonormal basis of localized states.
hamiltonian : The Hamiltonian of the tight binding chain.
BrillouinZone : The Brillouin zone of the tight binding chain.
QuantaWaveNumber : The quantized wavenumbers of the energy eigenstates.
energyEigenstate : The energy eigenstates of the tight binding chain.
energyEigenvalue : The energy eigenvalues of the tight binding chain.
hamiltonian_energyEigenstate : The Hamiltonian acting on an energy eigenstate
gives the corresponding energy eigenvalue times the energy eigenstate.
iii. Table of contents
A. The setup
B. The localized states
B.1. The orthonormal basis of localized states
B.2. Notation for localized states
B.3. Orthonormality of the localized states
C. The operator |m⟩⟨n|
C.1. Definition of the operator |m⟩⟨n|
C.2. Notation for the operator |m⟩⟨n|
C.3. The operator |m⟩⟨n| applied to a localized state
D. The Hamiltonian of the tight binding chain
D.1. Hermiticity of the Hamiltonian
D.2. Hamiltonian applied to a localized state
D.3. Mean energy of a localized state
E. The Brillouin zone and quantized wavenumbers
E.1. The Brillouin zone
E.2. The quantized wavenumbers of the energy eigenstates
E.3. Wavenumbers lie in the Brillouin zone
E.4. Expotentials related to the quantized wavenumbers
F. The energy eigenstates and eigenvalues
F.1. The energy eigenstates
F.2. Orthonormality of the energy eigenstates
F.3. The energy eigenvalues
F.4. The time-independent Schrodinger equation
iv. References
@[ expose ] public section
A. The setup
The physical parameters making up the tight binding chain.
The number of sites, or atoms, in the chain
The distance between the sites
The energy associate with a particle sitting at a fixed site.
structure TightBindingChain where N : Nat
[ N_ne_zero : NeZero N ] a : ℝ
a_pos : 0 < a E0 : ℝ t : ℝ
A.2. The Hilbert space
The Hilbert space of a TightBindingchain is the N-dimensional finite dimensional
Hilbert space.
B. The localized states
Localized states correspond to the electron being located on a specific site in the chain.
B.1. The orthonormal basis of localized states
B.2. Notation for localized states
The inner product of two localized states.
B.3. Orthonormality of the localized states
The localized states are normalized.
lemma localizedState_orthonormal_eq_ite ( m n : Fin T . N ) :
⟨ m | n ⟩ = if m = n then 1 else 0 := orthonormal_iff_ite . mp T . localizedState_orthonormal _ _
C. The operator |m⟩⟨n|
C.1. Definition of the operator |m⟩⟨n|
C.2. Notation for the operator |m⟩⟨n|
C.3. The operator |m⟩⟨n| applied to a localized state
lemma localizedComp_apply_localizedState ( m n p : Fin T . N ) :
| m ⟩⟨ n | | p ⟩ = if n = p then | m ⟩ else 0 := by T : TightBindingChain m : Fin T . N n : Fin T . N p : Fin T . N ⊢ | m ⟩⟨ n | ( localizedState p ) = if n = p then localizedState m else 0
rw [ localizedComp , T : TightBindingChain m : Fin T . N n : Fin T . N p : Fin T . N ⊢ { toFun := fun ψ => ⟪ localizedState n , ψ ⟫_ ℂ • localizedState m , map_add' := ⋯ , map_smul' := ⋯ } ( localizedState p ) =
if n = p then localizedState m else 0 All goals completed! 🐙 LinearMap.coe_mk , T : TightBindingChain m : Fin T . N n : Fin T . N p : Fin T . N ⊢ { toFun := fun ψ => ⟪ localizedState n , ψ ⟫_ ℂ • localizedState m , map_add' := ⋯ } ( localizedState p ) =
if n = p then localizedState m else 0 All goals completed! 🐙 AddHom.coe_mk , T : TightBindingChain m : Fin T . N n : Fin T . N p : Fin T . N ⊢ ⟪ localizedState n , localizedState p ⟫_ ℂ • localizedState m = if n = p then localizedState m else 0 All goals completed! 🐙
T . localizedState_orthonormal_eq_ite n p , T : TightBindingChain m : Fin T . N n : Fin T . N p : Fin T . N ⊢ ( if n = p then 1 else 0 ) • localizedState m = if n = p then localizedState m else 0 All goals completed! 🐙 ite_smul , T : TightBindingChain m : Fin T . N n : Fin T . N p : Fin T . N ⊢ ( if n = p then 1 • localizedState m else 0 • localizedState m ) = if n = p then localizedState m else 0 All goals completed! 🐙 one_smul , T : TightBindingChain m : Fin T . N n : Fin T . N p : Fin T . N ⊢ ( if n = p then localizedState m else 0 • localizedState m ) = if n = p then localizedState m else 0 All goals completed! 🐙 zero_smul T : TightBindingChain m : Fin T . N n : Fin T . N p : Fin T . N ⊢ ( if n = p then localizedState m else 0 ) = if n = p then localizedState m else 0 All goals completed! 🐙 ] All goals completed! 🐙
The adjoint of localizedComp |m⟩⟨n| is |n⟩⟨m|.
lemma localizedComp_adjoint ( m n : Fin T . N ) ( ψ φ : T . HilbertSpace ) :
⟪ | m ⟩⟨ n | ψ , φ ⟫_ ℂ = ⟪ ψ , | n ⟩⟨ m | φ ⟫_ ℂ := by T : TightBindingChain m : Fin T . N n : Fin T . N ψ : T . HilbertSpace φ : T . HilbertSpace ⊢ ⟪ | m ⟩⟨ n | ψ , φ ⟫_ ℂ = ⟪ ψ , | n ⟩⟨ m | φ ⟫_ ℂ
simp only [ localizedComp , LinearMap.coe_mk , AddHom.coe_mk , inner_smul_left , inner_smul_right ,
inner_conj_symm ] T : TightBindingChain m : Fin T . N n : Fin T . N ψ : T . HilbertSpace φ : T . HilbertSpace ⊢ ⟪ ψ , localizedState n ⟫_ ℂ * ⟪ localizedState m , φ ⟫_ ℂ = ⟪ localizedState m , φ ⟫_ ℂ * ⟪ ψ , localizedState n ⟫_ ℂ
ring All goals completed! 🐙
D. The Hamiltonian of the tight binding chain
D.1. Hermiticity of the Hamiltonian
The hamiltonian of the tight binding chain is hermitian.
lemma hamiltonian_hermitian ( ψ φ : T . HilbertSpace ) :
⟪ T . hamiltonian ψ , φ ⟫_ ℂ = ⟪ ψ , T . hamiltonian φ ⟫_ ℂ := by T : TightBindingChain ψ : T . HilbertSpace φ : T . HilbertSpace ⊢ ⟪ T . hamiltonian ψ , φ ⟫_ ℂ = ⟪ ψ , T . hamiltonian φ ⟫_ ℂ
simp only [ hamiltonian , LinearMap.sub_apply , LinearMap.smul_apply , LinearMap.coe_sum ,
Finset.sum_apply , LinearMap.add_apply , inner_sub_left , inner_sub_right ] T : TightBindingChain ψ : T . HilbertSpace φ : T . HilbertSpace ⊢ ⟪ T . E0 • ∑ c , | c ⟩⟨ c | ψ , φ ⟫_ ℂ - ⟪ T . t • ∑ x , ( | x ⟩⟨ x + 1 | ψ + | x + 1 ⟩⟨ x | ψ ) , φ ⟫_ ℂ =
⟪ ψ , T . E0 • ∑ c , | c ⟩⟨ c | φ ⟫_ ℂ - ⟪ ψ , T . t • ∑ x , ( | x ⟩⟨ x + 1 | φ + | x + 1 ⟩⟨ x | φ ) ⟫_ ℂ
congr 1 e_a T : TightBindingChain ψ : T . HilbertSpace φ : T . HilbertSpace ⊢ ⟪ T . E0 • ∑ c , | c ⟩⟨ c | ψ , φ ⟫_ ℂ = ⟪ ψ , T . E0 • ∑ c , | c ⟩⟨ c | φ ⟫_ ℂ e_a T : TightBindingChain ψ : T . HilbertSpace φ : T . HilbertSpace ⊢ ⟪ T . t • ∑ x , ( | x ⟩⟨ x + 1 | ψ + | x + 1 ⟩⟨ x | ψ ) , φ ⟫_ ℂ = ⟪ ψ , T . t • ∑ x , ( | x ⟩⟨ x + 1 | φ + | x + 1 ⟩⟨ x | φ ) ⟫_ ℂ
· e_a T : TightBindingChain ψ : T . HilbertSpace φ : T . HilbertSpace ⊢ ⟪ T . E0 • ∑ c , | c ⟩⟨ c | ψ , φ ⟫_ ℂ = ⟪ ψ , T . E0 • ∑ c , | c ⟩⟨ c | φ ⟫_ ℂ
simp only [ Finset.smul_sum , sum_inner , inner_sum , inner_smul_left_eq_smul ,
inner_smul_right_eq_smul , localizedComp_adjoint ] All goals completed! 🐙
· e_a T : TightBindingChain ψ : T . HilbertSpace φ : T . HilbertSpace ⊢ ⟪ T . t • ∑ x , ( | x ⟩⟨ x + 1 | ψ + | x + 1 ⟩⟨ x | ψ ) , φ ⟫_ ℂ = ⟪ ψ , T . t • ∑ x , ( | x ⟩⟨ x + 1 | φ + | x + 1 ⟩⟨ x | φ ) ⟫_ ℂ
simp only [ Finset.smul_sum , smul_add , sum_inner , inner_sum , inner_add_left , inner_add_right ,
inner_smul_left_eq_smul , inner_smul_right_eq_smul , localizedComp_adjoint ] e_a T : TightBindingChain ψ : T . HilbertSpace φ : T . HilbertSpace ⊢ ∑ x , ( T . t • ⟪ ψ , | x + 1 ⟩⟨ x | φ ⟫_ ℂ + T . t • ⟪ ψ , | x ⟩⟨ x + 1 | φ ⟫_ ℂ ) =
∑ x , ( T . t • ⟪ ψ , | x ⟩⟨ x + 1 | φ ⟫_ ℂ + T . t • ⟪ ψ , | x + 1 ⟩⟨ x | φ ⟫_ ℂ )
exact Finset.sum_congr rfl fun n _ => by T : TightBindingChain ψ : T . HilbertSpace φ : T . HilbertSpace n : Fin T . N x✝ : n ∈ Finset.univ ⊢ T . t • ⟪ ψ , | n + 1 ⟩⟨ n | φ ⟫_ ℂ + T . t • ⟪ ψ , | n ⟩⟨ n + 1 | φ ⟫_ ℂ = T . t • ⟪ ψ , | n ⟩⟨ n + 1 | φ ⟫_ ℂ + T . t • ⟪ ψ , | n + 1 ⟩⟨ n | φ ⟫_ ℂ ring All goals completed! 🐙
D.2. Hamiltonian applied to a localized state
The Hamiltonian applied to the localized state |n⟩ gives
T.E0 • |n⟩ - T.t • (|n + 1⟩ + |n - 1⟩).
lemma hamiltonian_apply_localizedState ( n : Fin T . N ) :
T . hamiltonian | n ⟩ = ( T . E0 : ℂ ) • | n ⟩ - ( T . t : ℂ ) • ( | n + 1 ⟩ + | n - 1 ⟩ ) := by T : TightBindingChain n : Fin T . N ⊢ T . hamiltonian ( localizedState n ) = ↑ T . E0 • localizedState n - ↑ T . t • ( localizedState ( n + 1 ) + localizedState ( n - 1 ) )
simp only [ hamiltonian , LinearMap.sub_apply , LinearMap.smul_apply , LinearMap.coe_sum ,
Finset.sum_apply , LinearMap.add_apply , smul_add , Finset.sum_add_distrib ,
localizedComp_apply_localizedState , ← eq_sub_iff_add_eq , Finset.sum_ite_eq' , Finset.mem_univ ,
if_true ] T : TightBindingChain n : Fin T . N ⊢ T . E0 • localizedState n - ( T . t • localizedState ( n - 1 ) + T . t • localizedState ( n + 1 ) ) =
↑ T . E0 • localizedState n - ( ↑ T . t • localizedState ( n + 1 ) + ↑ T . t • localizedState ( n - 1 ) )
module All goals completed! 🐙
D.3. Mean energy of a localized state
The energy of a localized state in the tight binding chain is E0.
This lemma assumes that there is more then one site in the chain otherwise the
result is not true.
lemma energy_localizedState ( n : Fin T . N ) ( htn : 1 < T . N ) : ⟪ | n ⟩ , T . hamiltonian | n ⟩ ⟫_ ℂ = T . E0 := by T : TightBindingChain n : Fin T . N htn : 1 < T . N ⊢ ⟪ localizedState n , T . hamiltonian ( localizedState n ) ⟫_ ℂ = ↑ T . E0
rw [ hamiltonian_apply_localizedState T : TightBindingChain n : Fin T . N htn : 1 < T . N ⊢ ⟪ localizedState n , ↑ T . E0 • localizedState n - ↑ T . t • ( localizedState ( n + 1 ) + localizedState ( n - 1 ) ) ⟫_ ℂ = ↑ T . E0 T : TightBindingChain n : Fin T . N htn : 1 < T . N ⊢ ⟪ localizedState n , ↑ T . E0 • localizedState n - ↑ T . t • ( localizedState ( n + 1 ) + localizedState ( n - 1 ) ) ⟫_ ℂ = ↑ T . E0 ] T : TightBindingChain n : Fin T . N htn : 1 < T . N ⊢ ⟪ localizedState n , ↑ T . E0 • localizedState n - ↑ T . t • ( localizedState ( n + 1 ) + localizedState ( n - 1 ) ) ⟫_ ℂ = ↑ T . E0
simp only [ smul_add , inner_sub_right , inner_add_right , inner_smul_right ,
localizedState_orthonormal_eq_ite , ↓ reduceIte , mul_one , left_eq_add , eq_sub_iff_add_eq ,
add_eq_left , Fin.one_eq_zero_iff , mul_ite , mul_zero , sub_eq_self ] T : TightBindingChain n : Fin T . N htn : 1 < T . N ⊢ ( ( if T . N = 1 then ↑ T . t else 0 ) + if T . N = 1 then ↑ T . t else 0 ) = 0
simp [ show T . N ≠ 1 from by omega ] All goals completed! 🐙
E. The Brillouin zone and quantized wavenumbers
E.1. The Brillouin zone
The Brillouin zone of the tight binding model is [-π/a, π/a).
This is the set in which wave functions are uniquely defined.
def BrillouinZone : Set ℝ := Set.Ico ( - Real.pi / T . a ) ( Real.pi / T . a )
E.2. The quantized wavenumbers of the energy eigenstates
The wavenumbers associated with the energy eigenstates.
This corresponds to the set 2 π / (a N) * (n - ⌊N/2⌋) for n : Fin T.N.
It is defined as such so it sits in the Brillouin zone.
def QuantaWaveNumber : Set ℝ := { x | ( ∃ n : Fin T . N ,
2 * Real.pi / ( T . a * T . N ) * ( ( n : ℝ ) - ( T . N / 2 : ℕ ) ) = x ) }
E.3. Wavenumbers lie in the Brillouin zone
The quantized wavenumbers form a subset of the BrillouinZone.
lemma quantaWaveNumber_exp_N ( n : ℕ ) ( k : T . QuantaWaveNumber ) :
Complex.exp ( Complex.I * k * n * T . N * T . a ) = 1 := by T : TightBindingChain n : ℕ k : ↑ T . QuantaWaveNumber ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ n * ↑ T . N * ↑ T . a ) = 1
refine Complex.exp_eq_one_iff . mpr ? _ T : TightBindingChain n : ℕ k : ↑ T . QuantaWaveNumber ⊢ ∃ n_1 , Complex.I * ↑ ↑ k * ↑ n * ↑ T . N * ↑ T . a = ↑ n_1 * ( 2 * ↑ Real.pi * Complex.I )
obtain ⟨ _ , m , rfl ⟩ := k T : TightBindingChain n : ℕ m : Fin T . N ⊢ ∃ n_1 ,
Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ m - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . N * ↑ T . a =
↑ n_1 * ( 2 * ↑ Real.pi * Complex.I )
use ( ( m : Int ) - ( T . N / 2 : ℕ ) ) * ( n : ℤ ) h T : TightBindingChain n : ℕ m : Fin T . N ⊢ Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ m - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . N * ↑ T . a =
↑ ( ( ↑ ↑ m - ↑ ( T . N / 2 ) ) * ↑ n ) * ( 2 * ↑ Real.pi * Complex.I )
have hpp : ( T . N : ℂ ) ≠ 0 := by T : TightBindingChain n : ℕ k : ↑ T . QuantaWaveNumber ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ n * ↑ T . N * ↑ T . a ) = 1 h T : TightBindingChain n : ℕ m : Fin T . N hpp : ↑ T . N ≠ 0 ⊢ Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ m - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . N * ↑ T . a =
↑ ( ( ↑ ↑ m - ↑ ( T . N / 2 ) ) * ↑ n ) * ( 2 * ↑ Real.pi * Complex.I ) simp [ Ne.symm ( NeZero.ne' T . N ) ] h T : TightBindingChain n : ℕ m : Fin T . N hpp : ↑ T . N ≠ 0 ⊢ Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ m - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . N * ↑ T . a =
↑ ( ( ↑ ↑ m - ↑ ( T . N / 2 ) ) * ↑ n ) * ( 2 * ↑ Real.pi * Complex.I ) h T : TightBindingChain n : ℕ m : Fin T . N hpp : ↑ T . N ≠ 0 ⊢ Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ m - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . N * ↑ T . a =
↑ ( ( ↑ ↑ m - ↑ ( T . N / 2 ) ) * ↑ n ) * ( 2 * ↑ Real.pi * Complex.I )
have hT' : ( T . a : ℂ ) ≠ 0 := Complex.ne_zero_of_re_pos T . a_pos h T : TightBindingChain n : ℕ m : Fin T . N hpp : ↑ T . N ≠ 0 hT' : ↑ T . a ≠ 0 ⊢ Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ m - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . N * ↑ T . a =
↑ ( ( ↑ ↑ m - ↑ ( T . N / 2 ) ) * ↑ n ) * ( 2 * ↑ Real.pi * Complex.I )
simp only [ Complex.ofReal_mul , Complex.ofReal_div , Complex.ofReal_ofNat , Complex.ofReal_natCast ,
Complex.ofReal_sub , Int.cast_mul , Int.cast_sub , Int.cast_natCast ] h T : TightBindingChain n : ℕ m : Fin T . N hpp : ↑ T . N ≠ 0 hT' : ↑ T . a ≠ 0 ⊢ Complex.I * ( 2 * ↑ Real.pi / ( ↑ T . a * ↑ T . N ) * ( ↑ ↑ m - ↑ ( T . N / 2 ) ) ) * ↑ n * ↑ T . N * ↑ T . a =
( ↑ ↑ m - ↑ ( T . N / 2 ) ) * ↑ n * ( 2 * ↑ Real.pi * Complex.I )
field_simp All goals completed! 🐙
lemma quantaWaveNumber_exp_sub_one ( n : Fin T . N ) ( k : T . QuantaWaveNumber ) :
Complex.exp ( Complex.I * k * ( n - 1 ) . val * T . a ) =
Complex.exp ( Complex.I * k * n * T . a ) * Complex.exp ( - Complex.I * k * T . a ) := by T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a )
rw [ Fin.val_sub T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - ↑ 1 + ↑ n ) % T . N ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a ) T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - ↑ 1 + ↑ n ) % T . N ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a ) ] T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - ↑ 1 + ↑ n ) % T . N ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a )
trans Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( ( T . N - 1 + n ) / T . N ) * T . N + ( n - 1 ) . val ) * ↑ T . a ) T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - ↑ 1 + ↑ n ) % T . N ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) ) * ↑ T . a ) T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a )
· T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - ↑ 1 + ↑ n ) % T . N ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) ) * ↑ T . a ) simp only [ Nat.cast_add , Nat.cast_mul ] T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - ↑ 1 + ↑ n ) % T . N ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ( ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N + ↑ ↑ ( n - 1 ) ) * ↑ T . a )
have h0 : ( Complex.I * ↑ ↑ k * ( ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N + ( n - 1 ) . val ) * ↑ T . a )
= Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N * ↑ T . a +
Complex.I * ↑ ↑ k * ( ( n - 1 ) . val * ↑ T . a ) := by T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a ) T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber h0 : Complex.I * ↑ ↑ k * ( ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N + ↑ ↑ ( n - 1 ) ) * ↑ T . a =
Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N * ↑ T . a + Complex.I * ↑ ↑ k * ( ↑ ↑ ( n - 1 ) * ↑ T . a ) ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - ↑ 1 + ↑ n ) % T . N ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ( ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N + ↑ ↑ ( n - 1 ) ) * ↑ T . a ) ring T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber h0 : Complex.I * ↑ ↑ k * ( ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N + ↑ ↑ ( n - 1 ) ) * ↑ T . a =
Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N * ↑ T . a + Complex.I * ↑ ↑ k * ( ↑ ↑ ( n - 1 ) * ↑ T . a ) ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - ↑ 1 + ↑ n ) % T . N ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ( ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N + ↑ ↑ ( n - 1 ) ) * ↑ T . a ) T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber h0 : Complex.I * ↑ ↑ k * ( ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N + ↑ ↑ ( n - 1 ) ) * ↑ T . a =
Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N * ↑ T . a + Complex.I * ↑ ↑ k * ( ↑ ↑ ( n - 1 ) * ↑ T . a ) ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - ↑ 1 + ↑ n ) % T . N ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ( ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N + ↑ ↑ ( n - 1 ) ) * ↑ T . a )
rw [ h0 , T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber h0 : Complex.I * ↑ ↑ k * ( ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N + ↑ ↑ ( n - 1 ) ) * ↑ T . a =
Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N * ↑ T . a + Complex.I * ↑ ↑ k * ( ↑ ↑ ( n - 1 ) * ↑ T . a ) ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - ↑ 1 + ↑ n ) % T . N ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N * ↑ T . a + Complex.I * ↑ ↑ k * ( ↑ ↑ ( n - 1 ) * ↑ T . a ) ) T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber h0 : Complex.I * ↑ ↑ k * ( ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N + ↑ ↑ ( n - 1 ) ) * ↑ T . a =
Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N * ↑ T . a + Complex.I * ↑ ↑ k * ( ↑ ↑ ( n - 1 ) * ↑ T . a ) ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - ↑ 1 + ↑ n ) % T . N ) * ↑ T . a ) = 1 * Complex.exp ( Complex.I * ↑ ↑ k * ( ↑ ↑ ( n - 1 ) * ↑ T . a ) ) Complex.exp_add , T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber h0 : Complex.I * ↑ ↑ k * ( ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N + ↑ ↑ ( n - 1 ) ) * ↑ T . a =
Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N * ↑ T . a + Complex.I * ↑ ↑ k * ( ↑ ↑ ( n - 1 ) * ↑ T . a ) ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - ↑ 1 + ↑ n ) % T . N ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N * ↑ T . a ) *
Complex.exp ( Complex.I * ↑ ↑ k * ( ↑ ↑ ( n - 1 ) * ↑ T . a ) ) T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber h0 : Complex.I * ↑ ↑ k * ( ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N + ↑ ↑ ( n - 1 ) ) * ↑ T . a =
Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N * ↑ T . a + Complex.I * ↑ ↑ k * ( ↑ ↑ ( n - 1 ) * ↑ T . a ) ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - ↑ 1 + ↑ n ) % T . N ) * ↑ T . a ) = 1 * Complex.exp ( Complex.I * ↑ ↑ k * ( ↑ ↑ ( n - 1 ) * ↑ T . a ) ) quantaWaveNumber_exp_N T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber h0 : Complex.I * ↑ ↑ k * ( ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N + ↑ ↑ ( n - 1 ) ) * ↑ T . a =
Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N * ↑ T . a + Complex.I * ↑ ↑ k * ( ↑ ↑ ( n - 1 ) * ↑ T . a ) ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - ↑ 1 + ↑ n ) % T . N ) * ↑ T . a ) = 1 * Complex.exp ( Complex.I * ↑ ↑ k * ( ↑ ↑ ( n - 1 ) * ↑ T . a ) ) T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber h0 : Complex.I * ↑ ↑ k * ( ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N + ↑ ↑ ( n - 1 ) ) * ↑ T . a =
Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N * ↑ T . a + Complex.I * ↑ ↑ k * ( ↑ ↑ ( n - 1 ) * ↑ T . a ) ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - ↑ 1 + ↑ n ) % T . N ) * ↑ T . a ) = 1 * Complex.exp ( Complex.I * ↑ ↑ k * ( ↑ ↑ ( n - 1 ) * ↑ T . a ) ) ] T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber h0 : Complex.I * ↑ ↑ k * ( ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N + ↑ ↑ ( n - 1 ) ) * ↑ T . a =
Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N * ↑ T . a + Complex.I * ↑ ↑ k * ( ↑ ↑ ( n - 1 ) * ↑ T . a ) ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - ↑ 1 + ↑ n ) % T . N ) * ↑ T . a ) = 1 * Complex.exp ( Complex.I * ↑ ↑ k * ( ↑ ↑ ( n - 1 ) * ↑ T . a ) )
simp only [ Fin.val_one' , one_mul ] T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber h0 : Complex.I * ↑ ↑ k * ( ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N + ↑ ↑ ( n - 1 ) ) * ↑ T . a =
Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N * ↑ T . a + Complex.I * ↑ ↑ k * ( ↑ ↑ ( n - 1 ) * ↑ T . a ) ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 % T . N + ↑ n ) % T . N ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ( ↑ ↑ ( n - 1 ) * ↑ T . a ) )
congr 1 T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber h0 : Complex.I * ↑ ↑ k * ( ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N + ↑ ↑ ( n - 1 ) ) * ↑ T . a =
Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N * ↑ T . a + Complex.I * ↑ ↑ k * ( ↑ ↑ ( n - 1 ) * ↑ T . a ) ⊢ Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 % T . N + ↑ n ) % T . N ) * ↑ T . a = Complex.I * ↑ ↑ k * ( ↑ ↑ ( n - 1 ) * ↑ T . a )
simp only [ mul_assoc , mul_eq_mul_left_iff , mul_eq_mul_right_iff , Nat.cast_inj ,
Complex.ofReal_eq_zero , Complex.I_ne_zero , or_false ] T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber h0 : Complex.I * ↑ ↑ k * ( ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N + ↑ ↑ ( n - 1 ) ) * ↑ T . a =
Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N ) * ↑ T . N * ↑ T . a + Complex.I * ↑ ↑ k * ( ↑ ↑ ( n - 1 ) * ↑ T . a ) ⊢ ( ( T . N - 1 % T . N + ↑ n ) % T . N = ↑ ( n - 1 ) ∨ T . a = 0 ) ∨ ↑ k = 0
aesop All goals completed! 🐙
· T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a ) have hx : ( ( ( T . N - 1 + n ) / T . N ) * T . N + ( n - 1 ) . val ) =
( T . N - 1 + n ) := by T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a ) T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a )
conv_rhs => rw [ ← Nat.div_add_mod' ( a := T . N - 1 + n ) ( b := T . N ) ] T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber | ( T . N - 1 + ↑ n ) / T . N * T . N + ( T . N - 1 + ↑ n ) % T . N T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a )
congr e_a T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber ⊢ ↑ ( n - 1 ) = ( T . N - 1 + ↑ n ) % T . N T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a )
by_cases hn : T . N = 1 pos T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hn : T . N = 1 ⊢ ↑ ( n - 1 ) = ( T . N - 1 + ↑ n ) % T . N neg T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hn : ¬ T . N = 1 ⊢ ↑ ( n - 1 ) = ( T . N - 1 + ↑ n ) % T . N T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a )
· pos T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hn : T . N = 1 ⊢ ↑ ( n - 1 ) = ( T . N - 1 + ↑ n ) % T . N T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a ) simp only [ hn , tsub_self , zero_add ] pos T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hn : T . N = 1 ⊢ ↑ ( n - 1 ) = ↑ n % 1 T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a )
have h0 : n = 0 := by T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a ) pos T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hn : T . N = 1 h0 : n = 0 ⊢ ↑ ( n - 1 ) = ↑ n % 1 T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a ) omega pos T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hn : T . N = 1 h0 : n = 0 ⊢ ↑ ( n - 1 ) = ↑ n % 1 T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a ) pos T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hn : T . N = 1 h0 : n = 0 ⊢ ↑ ( n - 1 ) = ↑ n % 1 T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a )
subst h0 pos T : TightBindingChain k : ↑ T . QuantaWaveNumber hn : T . N = 1 ⊢ ↑ ( 0 - 1 ) = ↑ 0 % 1 T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a )
simpa using hn All goals completed! 🐙 T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a )
· neg T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hn : ¬ T . N = 1 ⊢ ↑ ( n - 1 ) = ( T . N - 1 + ↑ n ) % T . N T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a ) rw [ @ Fin.val_sub neg T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hn : ¬ T . N = 1 ⊢ ( T . N - ↑ 1 + ↑ n ) % T . N = ( T . N - 1 + ↑ n ) % T . N neg T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hn : ¬ T . N = 1 ⊢ ( T . N - ↑ 1 + ↑ n ) % T . N = ( T . N - 1 + ↑ n ) % T . N T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a ) ] neg T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hn : ¬ T . N = 1 ⊢ ( T . N - ↑ 1 + ↑ n ) % T . N = ( T . N - 1 + ↑ n ) % T . N T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a )
congr neg.e_a.e_a.e_a T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hn : ¬ T . N = 1 ⊢ ↑ 1 = 1 T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a )
simp [ Nat.one_mod_eq_one . mpr hn ] T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a ) T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a )
rw [ hx T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( T . N - 1 + ↑ n ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a ) T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( T . N - 1 + ↑ n ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a ) ] T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( T . N - 1 + ↑ n ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a )
have hl : ( Complex.I * ↑ ↑ k * ↑ ( T . N - 1 + ↑ n ) * ↑ T . a ) =
Complex.I * ↑ ↑ k * n * ↑ T . a + Complex.I * ↑ ↑ k * ↑ ( T . N - 1 ) * ↑ T . a := by T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a ) T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n hl : Complex.I * ↑ ↑ k * ↑ ( T . N - 1 + ↑ n ) * ↑ T . a = Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a + Complex.I * ↑ ↑ k * ↑ ( T . N - 1 ) * ↑ T . a ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( T . N - 1 + ↑ n ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a )
simp only [ Nat.cast_add ] T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n ⊢ Complex.I * ↑ ↑ k * ( ↑ ( T . N - 1 ) + ↑ ↑ n ) * ↑ T . a = Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a + Complex.I * ↑ ↑ k * ↑ ( T . N - 1 ) * ↑ T . a T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n hl : Complex.I * ↑ ↑ k * ↑ ( T . N - 1 + ↑ n ) * ↑ T . a = Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a + Complex.I * ↑ ↑ k * ↑ ( T . N - 1 ) * ↑ T . a ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( T . N - 1 + ↑ n ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a )
ring T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n hl : Complex.I * ↑ ↑ k * ↑ ( T . N - 1 + ↑ n ) * ↑ T . a = Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a + Complex.I * ↑ ↑ k * ↑ ( T . N - 1 ) * ↑ T . a ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( T . N - 1 + ↑ n ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a ) T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n hl : Complex.I * ↑ ↑ k * ↑ ( T . N - 1 + ↑ n ) * ↑ T . a = Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a + Complex.I * ↑ ↑ k * ↑ ( T . N - 1 ) * ↑ T . a ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( T . N - 1 + ↑ n ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a )
rw [ hl , T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n hl : Complex.I * ↑ ↑ k * ↑ ( T . N - 1 + ↑ n ) * ↑ T . a = Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a + Complex.I * ↑ ↑ k * ↑ ( T . N - 1 ) * ↑ T . a ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a + Complex.I * ↑ ↑ k * ↑ ( T . N - 1 ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a ) T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n hl : Complex.I * ↑ ↑ k * ↑ ( T . N - 1 + ↑ n ) * ↑ T . a = Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a + Complex.I * ↑ ↑ k * ↑ ( T . N - 1 ) * ↑ T . a ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( T . N - 1 ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a ) Complex.exp_add T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n hl : Complex.I * ↑ ↑ k * ↑ ( T . N - 1 + ↑ n ) * ↑ T . a = Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a + Complex.I * ↑ ↑ k * ↑ ( T . N - 1 ) * ↑ T . a ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( T . N - 1 ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a ) T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n hl : Complex.I * ↑ ↑ k * ↑ ( T . N - 1 + ↑ n ) * ↑ T . a = Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a + Complex.I * ↑ ↑ k * ↑ ( T . N - 1 ) * ↑ T . a ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( T . N - 1 ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a ) ] T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n hl : Complex.I * ↑ ↑ k * ↑ ( T . N - 1 + ↑ n ) * ↑ T . a = Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a + Complex.I * ↑ ↑ k * ↑ ( T . N - 1 ) * ↑ T . a ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( T . N - 1 ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a )
congr 1 e_a T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n hl : Complex.I * ↑ ↑ k * ↑ ( T . N - 1 + ↑ n ) * ↑ T . a = Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a + Complex.I * ↑ ↑ k * ↑ ( T . N - 1 ) * ↑ T . a ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ( T . N - 1 ) * ↑ T . a ) = Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a )
rw [ Nat.cast_pred ( Nat.pos_of_neZero T . N ) e_a T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n hl : Complex.I * ↑ ↑ k * ↑ ( T . N - 1 + ↑ n ) * ↑ T . a = Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a + Complex.I * ↑ ↑ k * ↑ ( T . N - 1 ) * ↑ T . a ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ( ↑ T . N - 1 ) * ↑ T . a ) = Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a ) e_a T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n hl : Complex.I * ↑ ↑ k * ↑ ( T . N - 1 + ↑ n ) * ↑ T . a = Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a + Complex.I * ↑ ↑ k * ↑ ( T . N - 1 ) * ↑ T . a ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ( ↑ T . N - 1 ) * ↑ T . a ) = Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a ) ] e_a T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n hl : Complex.I * ↑ ↑ k * ↑ ( T . N - 1 + ↑ n ) * ↑ T . a = Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a + Complex.I * ↑ ↑ k * ↑ ( T . N - 1 ) * ↑ T . a ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ( ↑ T . N - 1 ) * ↑ T . a ) = Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a )
have hl : ( Complex.I * ↑ ↑ k * ( ↑ T . N - 1 ) * ↑ T . a ) =
Complex.I * ↑ ↑ k * ( 1 : ℕ ) * ↑ T . N * ↑ T . a + ( - Complex.I * ↑ ↑ k * ↑ T . a ) := by T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a ) e_a T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n hl✝ : Complex.I * ↑ ↑ k * ↑ ( T . N - 1 + ↑ n ) * ↑ T . a = Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a + Complex.I * ↑ ↑ k * ↑ ( T . N - 1 ) * ↑ T . a hl : Complex.I * ↑ ↑ k * ( ↑ T . N - 1 ) * ↑ T . a = Complex.I * ↑ ↑ k * ↑ 1 * ↑ T . N * ↑ T . a + - Complex.I * ↑ ↑ k * ↑ T . a ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ( ↑ T . N - 1 ) * ↑ T . a ) = Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a ) ring e_a T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n hl✝ : Complex.I * ↑ ↑ k * ↑ ( T . N - 1 + ↑ n ) * ↑ T . a = Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a + Complex.I * ↑ ↑ k * ↑ ( T . N - 1 ) * ↑ T . a hl : Complex.I * ↑ ↑ k * ( ↑ T . N - 1 ) * ↑ T . a = Complex.I * ↑ ↑ k * ↑ 1 * ↑ T . N * ↑ T . a + - Complex.I * ↑ ↑ k * ↑ T . a ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ( ↑ T . N - 1 ) * ↑ T . a ) = Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a ) e_a T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n hl✝ : Complex.I * ↑ ↑ k * ↑ ( T . N - 1 + ↑ n ) * ↑ T . a = Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a + Complex.I * ↑ ↑ k * ↑ ( T . N - 1 ) * ↑ T . a hl : Complex.I * ↑ ↑ k * ( ↑ T . N - 1 ) * ↑ T . a = Complex.I * ↑ ↑ k * ↑ 1 * ↑ T . N * ↑ T . a + - Complex.I * ↑ ↑ k * ↑ T . a ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ( ↑ T . N - 1 ) * ↑ T . a ) = Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a )
rw [ hl , e_a T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n hl✝ : Complex.I * ↑ ↑ k * ↑ ( T . N - 1 + ↑ n ) * ↑ T . a = Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a + Complex.I * ↑ ↑ k * ↑ ( T . N - 1 ) * ↑ T . a hl : Complex.I * ↑ ↑ k * ( ↑ T . N - 1 ) * ↑ T . a = Complex.I * ↑ ↑ k * ↑ 1 * ↑ T . N * ↑ T . a + - Complex.I * ↑ ↑ k * ↑ T . a ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ 1 * ↑ T . N * ↑ T . a + - Complex.I * ↑ ↑ k * ↑ T . a ) = Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a ) All goals completed! 🐙 Complex.exp_add , e_a T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n hl✝ : Complex.I * ↑ ↑ k * ↑ ( T . N - 1 + ↑ n ) * ↑ T . a = Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a + Complex.I * ↑ ↑ k * ↑ ( T . N - 1 ) * ↑ T . a hl : Complex.I * ↑ ↑ k * ( ↑ T . N - 1 ) * ↑ T . a = Complex.I * ↑ ↑ k * ↑ 1 * ↑ T . N * ↑ T . a + - Complex.I * ↑ ↑ k * ↑ T . a ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ 1 * ↑ T . N * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a ) =
Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a ) All goals completed! 🐙 quantaWaveNumber_exp_N , e_a T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n hl✝ : Complex.I * ↑ ↑ k * ↑ ( T . N - 1 + ↑ n ) * ↑ T . a = Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a + Complex.I * ↑ ↑ k * ↑ ( T . N - 1 ) * ↑ T . a hl : Complex.I * ↑ ↑ k * ( ↑ T . N - 1 ) * ↑ T . a = Complex.I * ↑ ↑ k * ↑ 1 * ↑ T . N * ↑ T . a + - Complex.I * ↑ ↑ k * ↑ T . a ⊢ 1 * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a ) = Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a ) All goals completed! 🐙 neg_mul , e_a T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n hl✝ : Complex.I * ↑ ↑ k * ↑ ( T . N - 1 + ↑ n ) * ↑ T . a = Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a + Complex.I * ↑ ↑ k * ↑ ( T . N - 1 ) * ↑ T . a hl : Complex.I * ↑ ↑ k * ( ↑ T . N - 1 ) * ↑ T . a = Complex.I * ↑ ↑ k * ↑ 1 * ↑ T . N * ↑ T . a + - Complex.I * ↑ ↑ k * ↑ T . a ⊢ 1 * Complex.exp ( - ( Complex.I * ↑ ↑ k ) * ↑ T . a ) = Complex.exp ( - ( Complex.I * ↑ ↑ k ) * ↑ T . a ) All goals completed! 🐙 one_mul e_a T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber hx : ( T . N - 1 + ↑ n ) / T . N * T . N + ↑ ( n - 1 ) = T . N - 1 + ↑ n hl✝ : Complex.I * ↑ ↑ k * ↑ ( T . N - 1 + ↑ n ) * ↑ T . a = Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a + Complex.I * ↑ ↑ k * ↑ ( T . N - 1 ) * ↑ T . a hl : Complex.I * ↑ ↑ k * ( ↑ T . N - 1 ) * ↑ T . a = Complex.I * ↑ ↑ k * ↑ 1 * ↑ T . N * ↑ T . a + - Complex.I * ↑ ↑ k * ↑ T . a ⊢ Complex.exp ( - ( Complex.I * ↑ ↑ k ) * ↑ T . a ) = Complex.exp ( - ( Complex.I * ↑ ↑ k ) * ↑ T . a ) All goals completed! 🐙 ] All goals completed! 🐙 lemma quantaWaveNumber_exp_add_one ( n : Fin T . N ) ( k : T . QuantaWaveNumber ) :
Complex.exp ( Complex.I * k * ( n + 1 ) . val * T . a ) =
Complex.exp ( Complex.I * k * n * T . a ) * Complex.exp ( Complex.I * k * T . a ) := by T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) =
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( Complex.I * ↑ ↑ k * ↑ T . a )
conv_rhs =>
rw [ show n = ( n + 1 ) - 1 from ( add_sub_cancel_right n 1 ) . symm ,
quantaWaveNumber_exp_sub_one , mul_assoc , ← Complex.exp_add ] T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber | Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a + Complex.I * ↑ ↑ k * ↑ T . a )
simp T : TightBindingChain n : Fin T . N k : ↑ T . QuantaWaveNumber | Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a )
F. The energy eigenstates and eigenvalues
F.1. The energy eigenstates
F.2. Orthonormality of the energy eigenstates
The energy eigenstates of the tight binding chain are orthogonal.
This is a fundamental quantum mechanical result: eigenstates of a Hermitian operator
(the Hamiltonian) with distinct eigenvalues are orthogonal. Here we prove it directly
using the periodic boundary conditions which quantize the wavenumbers.
The key physical insight is that different wavenumbers k₁ ≠ k₂ give rise to different
N-th roots of unity exp(i(k₂-k₁)a), and the sum of all N-th roots of unity equals zero.
lemma energyEigenstate_orthogonal :
Pairwise fun k1 k2 => ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0 := by T : TightBindingChain ⊢ Pairwise fun k1 k2 => ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0
intro k1 k2 hne T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0
set ω := Complex.exp ( Complex.I * ( k2 - k1 ) * T . a ) with hω_def T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0
have hterm ( n : ℕ ) : ( starRingEnd ℂ ) ( Complex.exp ( Complex.I * k1 * n * T . a ) ) *
Complex.exp ( Complex.I * k2 * n * T . a ) = ω ^ n := by T : TightBindingChain ⊢ Pairwise fun k1 k2 => ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0 T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0
rw [ ← Complex.exp_conj , T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) n : ℕ ⊢ Complex.exp ( ( starRingEnd ℂ ) ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) n : ℕ ⊢ Complex.exp ( ( starRingEnd ℂ ) ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) + Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) =
Complex.exp ( ↑ n * ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) ) T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0 ← Complex.exp_add , T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) n : ℕ ⊢ Complex.exp ( ( starRingEnd ℂ ) ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) + Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) n : ℕ ⊢ Complex.exp ( ( starRingEnd ℂ ) ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) + Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) =
Complex.exp ( ↑ n * ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) ) T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0 hω_def , T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) n : ℕ ⊢ Complex.exp ( ( starRingEnd ℂ ) ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) + Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) =
Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) ^ n T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) n : ℕ ⊢ Complex.exp ( ( starRingEnd ℂ ) ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) + Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) =
Complex.exp ( ↑ n * ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) ) T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0 ← Complex.exp_nat_mul T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) n : ℕ ⊢ Complex.exp ( ( starRingEnd ℂ ) ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) + Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) =
Complex.exp ( ↑ n * ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) ) T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) n : ℕ ⊢ Complex.exp ( ( starRingEnd ℂ ) ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) + Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) =
Complex.exp ( ↑ n * ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) ) T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0 ] T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) n : ℕ ⊢ Complex.exp ( ( starRingEnd ℂ ) ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) + Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) =
Complex.exp ( ↑ n * ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) ) T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0
simp only [ map_mul , Complex.conj_I , Complex.conj_ofReal , Complex.conj_natCast ] T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) n : ℕ ⊢ Complex.exp ( - Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a + Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) =
Complex.exp ( ↑ n * ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) ) T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0
ring_nf T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0 T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0
have hω_pow : ω ^ T . N = 1 := by T : TightBindingChain ⊢ Pairwise fun k1 k2 => ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0 T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0
rw [ hω_def , T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n ⊢ Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) ^ T . N = 1 T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0 ← Complex.exp_nat_mul , T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n ⊢ Complex.exp ( ↑ T . N * ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) ) = 1 T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0 show ( T . N : ℂ ) * ( Complex.I * ( k2 - k1 ) * T . a ) =
Complex.I * k2 * ( 1 : ℕ ) * T . N * T . a - Complex.I * k1 * ( 1 : ℕ ) * T . N * T . a by T : TightBindingChain ⊢ Pairwise fun k1 k2 => ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0 T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0
push_cast T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n ⊢ ↑ T . N * ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) = Complex.I * ↑ ↑ k2 * 1 * ↑ T . N * ↑ T . a - Complex.I * ↑ ↑ k1 * 1 * ↑ T . N * ↑ T . a T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0 ; ring All goals completed! 🐙 T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0 ,
Complex.exp_sub , T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n ⊢ Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ 1 * ↑ T . N * ↑ T . a ) / Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ 1 * ↑ T . N * ↑ T . a ) = 1 T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0 T . quantaWaveNumber_exp_N 1 k2 , T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n ⊢ 1 / Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ 1 * ↑ T . N * ↑ T . a ) = 1 T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0 T . quantaWaveNumber_exp_N 1 k1 , T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n ⊢ 1 / 1 = 1 T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0 div_one T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n ⊢ 1 = 1 T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0 ] T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0 T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0
have hω_ne_one : ω ≠ 1 := fun hω_eq_one => hne <| by T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_eq_one : ω = 1 ⊢ k1 = k2 T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0
obtain ⟨ _ , ⟨ n1 , rfl ⟩ ⟩ := k1 T : TightBindingChain k2 : ↑ T . QuantaWaveNumber n1 : Fin T . N hne : ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) ) *
Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) =
ω ^ n hω_pow : ω ^ T . N = 1 hω_eq_one : ω = 1 ⊢ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ = k2 T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0
obtain ⟨ _ , ⟨ n2 , rfl ⟩ ⟩ := k2 T : TightBindingChain n1 : Fin T . N n2 : Fin T . N hne : ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ≠ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ω : ℂ :=
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hω_def : ω =
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) ) *
Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) =
ω ^ n hω_pow : ω ^ T . N = 1 hω_eq_one : ω = 1 ⊢ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ = ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0
obtain ⟨ m , hm ⟩ := Complex.exp_eq_one_iff . mp ( hω_def ▸ hω_eq_one ) T : TightBindingChain n1 : Fin T . N n2 : Fin T . N hne : ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ≠ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ω : ℂ :=
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hω_def : ω =
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) ) *
Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) =
ω ^ n hω_pow : ω ^ T . N = 1 hω_eq_one : ω = 1 m : ℤ hm : Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a =
↑ m * ( 2 * ↑ Real.pi * Complex.I ) ⊢ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ = ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0
have ha : ( T . a : ℂ ) ≠ 0 := Complex.ne_zero_of_re_pos T . a_pos T : TightBindingChain n1 : Fin T . N n2 : Fin T . N hne : ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ≠ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ω : ℂ :=
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hω_def : ω =
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) ) *
Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) =
ω ^ n hω_pow : ω ^ T . N = 1 hω_eq_one : ω = 1 m : ℤ hm : Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a =
↑ m * ( 2 * ↑ Real.pi * Complex.I ) ha : ↑ T . a ≠ 0 ⊢ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ = ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0
have hN : ( T . N : ℂ ) ≠ 0 := Nat.cast_ne_zero . mpr ( NeZero.ne T . N ) T : TightBindingChain n1 : Fin T . N n2 : Fin T . N hne : ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ≠ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ω : ℂ :=
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hω_def : ω =
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) ) *
Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) =
ω ^ n hω_pow : ω ^ T . N = 1 hω_eq_one : ω = 1 m : ℤ hm : Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a =
↑ m * ( 2 * ↑ Real.pi * Complex.I ) ha : ↑ T . a ≠ 0 hN : ↑ T . N ≠ 0 ⊢ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ = ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0
push_cast at hm T : TightBindingChain n1 : Fin T . N n2 : Fin T . N hne : ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ≠ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ω : ℂ :=
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hω_def : ω =
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) ) *
Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) =
ω ^ n hω_pow : ω ^ T . N = 1 hω_eq_one : ω = 1 m : ℤ ha : ↑ T . a ≠ 0 hN : ↑ T . N ≠ 0 hm : Complex.I * ( 2 * ↑ Real.pi / ( ↑ T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) - 2 * ↑ Real.pi / ( ↑ T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) ) *
↑ T . a =
↑ m * ( 2 * ↑ Real.pi * Complex.I ) ⊢ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ = ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0
field_simp at hm T : TightBindingChain n1 : Fin T . N n2 : Fin T . N hne : ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ≠ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ω : ℂ :=
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hω_def : ω =
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) ) *
Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) =
ω ^ n hω_pow : ω ^ T . N = 1 hω_eq_one : ω = 1 m : ℤ ha : ↑ T . a ≠ 0 hN : ↑ T . N ≠ 0 hm : ↑ ↑ n2 - ↑ ( T . N / 2 ) - ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) = ↑ T . N * ↑ m ⊢ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ = ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0
have hm_int : ( T . N : ℤ ) ∣ ( n2 : ℤ ) - n1 := ⟨ m , by T : TightBindingChain n1 : Fin T . N n2 : Fin T . N hne : ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ≠ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ω : ℂ :=
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hω_def : ω =
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) ) *
Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) =
ω ^ n hω_pow : ω ^ T . N = 1 hω_eq_one : ω = 1 m : ℤ ha : ↑ T . a ≠ 0 hN : ↑ T . N ≠ 0 hm : ↑ ↑ n2 - ↑ ( T . N / 2 ) - ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) = ↑ T . N * ↑ m ⊢ ↑ ↑ n2 - ↑ ↑ n1 = ↑ T . N * m T : TightBindingChain n1 : Fin T . N n2 : Fin T . N hne : ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ≠ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ω : ℂ :=
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hω_def : ω =
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) ) *
Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) =
ω ^ n hω_pow : ω ^ T . N = 1 hω_eq_one : ω = 1 m : ℤ ha : ↑ T . a ≠ 0 hN : ↑ T . N ≠ 0 hm : ↑ ↑ n2 - ↑ ( T . N / 2 ) - ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) = ↑ T . N * ↑ m hm_int : ↑ T . N ∣ ↑ ↑ n2 - ↑ ↑ n1 ⊢ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ = ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0
have : ( n2 : ℂ ) - n1 = ( T . N : ℂ ) * m := by ring_nf at hm ⊢ T : TightBindingChain n1 : Fin T . N n2 : Fin T . N hne : ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ≠ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ω : ℂ :=
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hω_def : ω =
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) ) *
Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) =
ω ^ n hω_pow : ω ^ T . N = 1 hω_eq_one : ω = 1 m : ℤ ha : ↑ T . a ≠ 0 hN : ↑ T . N ≠ 0 hm : ↑ ↑ n2 - ↑ ↑ n1 = ↑ T . N * ↑ m ⊢ ↑ ↑ n2 - ↑ ↑ n1 = ↑ T . N * ↑ m T : TightBindingChain n1 : Fin T . N n2 : Fin T . N hne : ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ≠ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ω : ℂ :=
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hω_def : ω =
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) ) *
Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) =
ω ^ n hω_pow : ω ^ T . N = 1 hω_eq_one : ω = 1 m : ℤ ha : ↑ T . a ≠ 0 hN : ↑ T . N ≠ 0 hm : ↑ ↑ n2 - ↑ ( T . N / 2 ) - ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) = ↑ T . N * ↑ m this : ↑ ↑ n2 - ↑ ↑ n1 = ↑ T . N * ↑ m ⊢ ↑ ↑ n2 - ↑ ↑ n1 = ↑ T . N * m T : TightBindingChain n1 : Fin T . N n2 : Fin T . N hne : ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ≠ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ω : ℂ :=
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hω_def : ω =
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) ) *
Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) =
ω ^ n hω_pow : ω ^ T . N = 1 hω_eq_one : ω = 1 m : ℤ ha : ↑ T . a ≠ 0 hN : ↑ T . N ≠ 0 hm : ↑ ↑ n2 - ↑ ( T . N / 2 ) - ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) = ↑ T . N * ↑ m hm_int : ↑ T . N ∣ ↑ ↑ n2 - ↑ ↑ n1 ⊢ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ = ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0 ; exact hm T : TightBindingChain n1 : Fin T . N n2 : Fin T . N hne : ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ≠ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ω : ℂ :=
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hω_def : ω =
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) ) *
Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) =
ω ^ n hω_pow : ω ^ T . N = 1 hω_eq_one : ω = 1 m : ℤ ha : ↑ T . a ≠ 0 hN : ↑ T . N ≠ 0 hm : ↑ ↑ n2 - ↑ ( T . N / 2 ) - ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) = ↑ T . N * ↑ m this : ↑ ↑ n2 - ↑ ↑ n1 = ↑ T . N * ↑ m ⊢ ↑ ↑ n2 - ↑ ↑ n1 = ↑ T . N * m T : TightBindingChain n1 : Fin T . N n2 : Fin T . N hne : ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ≠ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ω : ℂ :=
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hω_def : ω =
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) ) *
Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) =
ω ^ n hω_pow : ω ^ T . N = 1 hω_eq_one : ω = 1 m : ℤ ha : ↑ T . a ≠ 0 hN : ↑ T . N ≠ 0 hm : ↑ ↑ n2 - ↑ ( T . N / 2 ) - ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) = ↑ T . N * ↑ m hm_int : ↑ T . N ∣ ↑ ↑ n2 - ↑ ↑ n1 ⊢ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ = ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0 T : TightBindingChain n1 : Fin T . N n2 : Fin T . N hne : ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ≠ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ω : ℂ :=
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hω_def : ω =
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) ) *
Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) =
ω ^ n hω_pow : ω ^ T . N = 1 hω_eq_one : ω = 1 m : ℤ ha : ↑ T . a ≠ 0 hN : ↑ T . N ≠ 0 hm : ↑ ↑ n2 - ↑ ( T . N / 2 ) - ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) = ↑ T . N * ↑ m this : ↑ ↑ n2 - ↑ ↑ n1 = ↑ T . N * ↑ m ⊢ ↑ ↑ n2 - ↑ ↑ n1 = ↑ T . N * m T : TightBindingChain n1 : Fin T . N n2 : Fin T . N hne : ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ≠ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ω : ℂ :=
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hω_def : ω =
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) ) *
Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) =
ω ^ n hω_pow : ω ^ T . N = 1 hω_eq_one : ω = 1 m : ℤ ha : ↑ T . a ≠ 0 hN : ↑ T . N ≠ 0 hm : ↑ ↑ n2 - ↑ ( T . N / 2 ) - ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) = ↑ T . N * ↑ m hm_int : ↑ T . N ∣ ↑ ↑ n2 - ↑ ↑ n1 ⊢ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ = ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0
exact_mod_cast this All goals completed! 🐙 T : TightBindingChain n1 : Fin T . N n2 : Fin T . N hne : ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ≠ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ω : ℂ :=
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hω_def : ω =
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) ) *
Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) =
ω ^ n hω_pow : ω ^ T . N = 1 hω_eq_one : ω = 1 m : ℤ ha : ↑ T . a ≠ 0 hN : ↑ T . N ≠ 0 hm : ↑ ↑ n2 - ↑ ( T . N / 2 ) - ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) = ↑ T . N * ↑ m hm_int : ↑ T . N ∣ ↑ ↑ n2 - ↑ ↑ n1 ⊢ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ = ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0 ⟩ T : TightBindingChain n1 : Fin T . N n2 : Fin T . N hne : ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ≠ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ω : ℂ :=
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hω_def : ω =
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) ) *
Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) =
ω ^ n hω_pow : ω ^ T . N = 1 hω_eq_one : ω = 1 m : ℤ ha : ↑ T . a ≠ 0 hN : ↑ T . N ≠ 0 hm : ↑ ↑ n2 - ↑ ( T . N / 2 ) - ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) = ↑ T . N * ↑ m hm_int : ↑ T . N ∣ ↑ ↑ n2 - ↑ ↑ n1 ⊢ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ = ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0
have := Int.eq_zero_of_abs_lt_dvd hm_int
( abs_lt . mpr ⟨ by T : TightBindingChain n1 : Fin T . N n2 : Fin T . N hne : ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ≠ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ω : ℂ :=
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hω_def : ω =
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) ) *
Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) =
ω ^ n hω_pow : ω ^ T . N = 1 hω_eq_one : ω = 1 m : ℤ ha : ↑ T . a ≠ 0 hN : ↑ T . N ≠ 0 hm : ↑ ↑ n2 - ↑ ( T . N / 2 ) - ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) = ↑ T . N * ↑ m hm_int : ↑ T . N ∣ ↑ ↑ n2 - ↑ ↑ n1 ⊢ - ↑ T . N < ↑ ↑ n2 - ↑ ↑ n1 T : TightBindingChain n1 : Fin T . N n2 : Fin T . N hne : ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ≠ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ω : ℂ :=
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hω_def : ω =
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) ) *
Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) =
ω ^ n hω_pow : ω ^ T . N = 1 hω_eq_one : ω = 1 m : ℤ ha : ↑ T . a ≠ 0 hN : ↑ T . N ≠ 0 hm : ↑ ↑ n2 - ↑ ( T . N / 2 ) - ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) = ↑ T . N * ↑ m hm_int : ↑ T . N ∣ ↑ ↑ n2 - ↑ ↑ n1 this : ↑ ↑ n2 - ↑ ↑ n1 = 0 ⊢ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ = ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0 have := n1 . isLt T : TightBindingChain n1 : Fin T . N n2 : Fin T . N hne : ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ≠ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ω : ℂ :=
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hω_def : ω =
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) ) *
Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) =
ω ^ n hω_pow : ω ^ T . N = 1 hω_eq_one : ω = 1 m : ℤ ha : ↑ T . a ≠ 0 hN : ↑ T . N ≠ 0 hm : ↑ ↑ n2 - ↑ ( T . N / 2 ) - ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) = ↑ T . N * ↑ m hm_int : ↑ T . N ∣ ↑ ↑ n2 - ↑ ↑ n1 this : ↑ n1 < T . N ⊢ - ↑ T . N < ↑ ↑ n2 - ↑ ↑ n1 T : TightBindingChain n1 : Fin T . N n2 : Fin T . N hne : ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ≠ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ω : ℂ :=
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hω_def : ω =
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) ) *
Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) =
ω ^ n hω_pow : ω ^ T . N = 1 hω_eq_one : ω = 1 m : ℤ ha : ↑ T . a ≠ 0 hN : ↑ T . N ≠ 0 hm : ↑ ↑ n2 - ↑ ( T . N / 2 ) - ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) = ↑ T . N * ↑ m hm_int : ↑ T . N ∣ ↑ ↑ n2 - ↑ ↑ n1 this : ↑ ↑ n2 - ↑ ↑ n1 = 0 ⊢ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ = ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0 ; omega All goals completed! 🐙 T : TightBindingChain n1 : Fin T . N n2 : Fin T . N hne : ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ≠ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ω : ℂ :=
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hω_def : ω =
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) ) *
Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) =
ω ^ n hω_pow : ω ^ T . N = 1 hω_eq_one : ω = 1 m : ℤ ha : ↑ T . a ≠ 0 hN : ↑ T . N ≠ 0 hm : ↑ ↑ n2 - ↑ ( T . N / 2 ) - ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) = ↑ T . N * ↑ m hm_int : ↑ T . N ∣ ↑ ↑ n2 - ↑ ↑ n1 this : ↑ ↑ n2 - ↑ ↑ n1 = 0 ⊢ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ = ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0 , by T : TightBindingChain n1 : Fin T . N n2 : Fin T . N hne : ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ≠ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ω : ℂ :=
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hω_def : ω =
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) ) *
Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) =
ω ^ n hω_pow : ω ^ T . N = 1 hω_eq_one : ω = 1 m : ℤ ha : ↑ T . a ≠ 0 hN : ↑ T . N ≠ 0 hm : ↑ ↑ n2 - ↑ ( T . N / 2 ) - ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) = ↑ T . N * ↑ m hm_int : ↑ T . N ∣ ↑ ↑ n2 - ↑ ↑ n1 ⊢ ↑ ↑ n2 - ↑ ↑ n1 < ↑ T . N T : TightBindingChain n1 : Fin T . N n2 : Fin T . N hne : ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ≠ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ω : ℂ :=
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hω_def : ω =
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) ) *
Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) =
ω ^ n hω_pow : ω ^ T . N = 1 hω_eq_one : ω = 1 m : ℤ ha : ↑ T . a ≠ 0 hN : ↑ T . N ≠ 0 hm : ↑ ↑ n2 - ↑ ( T . N / 2 ) - ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) = ↑ T . N * ↑ m hm_int : ↑ T . N ∣ ↑ ↑ n2 - ↑ ↑ n1 this : ↑ ↑ n2 - ↑ ↑ n1 = 0 ⊢ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ = ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0 have := n2 . isLt T : TightBindingChain n1 : Fin T . N n2 : Fin T . N hne : ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ≠ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ω : ℂ :=
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hω_def : ω =
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) ) *
Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) =
ω ^ n hω_pow : ω ^ T . N = 1 hω_eq_one : ω = 1 m : ℤ ha : ↑ T . a ≠ 0 hN : ↑ T . N ≠ 0 hm : ↑ ↑ n2 - ↑ ( T . N / 2 ) - ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) = ↑ T . N * ↑ m hm_int : ↑ T . N ∣ ↑ ↑ n2 - ↑ ↑ n1 this : ↑ n2 < T . N ⊢ ↑ ↑ n2 - ↑ ↑ n1 < ↑ T . N T : TightBindingChain n1 : Fin T . N n2 : Fin T . N hne : ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ≠ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ω : ℂ :=
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hω_def : ω =
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) ) *
Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) =
ω ^ n hω_pow : ω ^ T . N = 1 hω_eq_one : ω = 1 m : ℤ ha : ↑ T . a ≠ 0 hN : ↑ T . N ≠ 0 hm : ↑ ↑ n2 - ↑ ( T . N / 2 ) - ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) = ↑ T . N * ↑ m hm_int : ↑ T . N ∣ ↑ ↑ n2 - ↑ ↑ n1 this : ↑ ↑ n2 - ↑ ↑ n1 = 0 ⊢ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ = ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0 ; omega All goals completed! 🐙 T : TightBindingChain n1 : Fin T . N n2 : Fin T . N hne : ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ≠ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ω : ℂ :=
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hω_def : ω =
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) ) *
Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) =
ω ^ n hω_pow : ω ^ T . N = 1 hω_eq_one : ω = 1 m : ℤ ha : ↑ T . a ≠ 0 hN : ↑ T . N ≠ 0 hm : ↑ ↑ n2 - ↑ ( T . N / 2 ) - ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) = ↑ T . N * ↑ m hm_int : ↑ T . N ∣ ↑ ↑ n2 - ↑ ↑ n1 this : ↑ ↑ n2 - ↑ ↑ n1 = 0 ⊢ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ = ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0 ⟩ ) T : TightBindingChain n1 : Fin T . N n2 : Fin T . N hne : ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ≠ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ω : ℂ :=
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hω_def : ω =
Complex.exp
( Complex.I *
( ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ -
↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ ) *
↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) ) *
Complex.exp ( Complex.I * ↑ ↑ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ * ↑ n * ↑ T . a ) =
ω ^ n hω_pow : ω ^ T . N = 1 hω_eq_one : ω = 1 m : ℤ ha : ↑ T . a ≠ 0 hN : ↑ T . N ≠ 0 hm : ↑ ↑ n2 - ↑ ( T . N / 2 ) - ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) = ↑ T . N * ↑ m hm_int : ↑ T . N ∣ ↑ ↑ n2 - ↑ ↑ n1 this : ↑ ↑ n2 - ↑ ↑ n1 = 0 ⊢ ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n1 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ = ⟨ 2 * Real.pi / ( T . a * ↑ T . N ) * ( ↑ ↑ n2 - ↑ ( T . N / 2 ) ) , ⋯ ⟩ T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0
simp only [ show n1 . val = n2 . val by omega ] T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0 T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ ⟪ T . energyEigenstate k1 , T . energyEigenstate k2 ⟫_ ℂ = 0
simp only [ energyEigenstate , sum_inner ] T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ ∑ i ,
⟪ Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ ↑ i * ↑ T . a ) • localizedState i ,
∑ n , Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ ↑ n * ↑ T . a ) • localizedState n ⟫_ ℂ =
0
simp_rw [ T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ ∑ i ,
⟪ Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ ↑ i * ↑ T . a ) • localizedState i ,
∑ n , Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ ↑ n * ↑ T . a ) • localizedState n ⟫_ ℂ =
0 inner_sum , T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ ∑ x ,
∑ i ,
⟪ Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ ↑ x * ↑ T . a ) • localizedState x ,
Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ ↑ i * ↑ T . a ) • localizedState i ⟫_ ℂ =
0 inner_smul_left , T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ ∑ x ,
∑ x_1 ,
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ ↑ x * ↑ T . a ) ) *
⟪ localizedState x , Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ ↑ x_1 * ↑ T . a ) • localizedState x_1 ⟫_ ℂ =
0 inner_smul_right , T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ ∑ x ,
∑ x_1 ,
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ ↑ x * ↑ T . a ) ) *
( Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ ↑ x_1 * ↑ T . a ) * ⟪ localizedState x , localizedState x_1 ⟫_ ℂ ) =
0 localizedState_orthonormal_eq_ite T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ ∑ x ,
∑ x_1 ,
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ ↑ x * ↑ T . a ) ) *
( Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ ↑ x_1 * ↑ T . a ) * if x = x_1 then 1 else 0 ) =
0 ]
simp only [ mul_ite , mul_one , mul_zero , Finset.sum_ite_eq , Finset.mem_univ , ↓ reduceIte , hterm ] T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ ∑ x , ω ^ ↑ x = 0
rw [ Fin.sum_univ_eq_sum_range ( ω ^ · ) , T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ ∑ i ∈ Finset.range T . N , ω ^ i = 0 All goals completed! 🐙 geom_sum_eq hω_ne_one , T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ ( ω ^ T . N - 1 ) / ( ω - 1 ) = 0 All goals completed! 🐙 hω_pow , T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ ( 1 - 1 ) / ( ω - 1 ) = 0 All goals completed! 🐙 sub_self , T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ 0 / ( ω - 1 ) = 0 All goals completed! 🐙 zero_div T : TightBindingChain k1 : ↑ T . QuantaWaveNumber k2 : ↑ T . QuantaWaveNumber hne : k1 ≠ k2 ω : ℂ := Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hω_def : ω = Complex.exp ( Complex.I * ( ↑ ↑ k2 - ↑ ↑ k1 ) * ↑ T . a ) hterm : ∀ ( n : ℕ ),
( starRingEnd ℂ ) ( Complex.exp ( Complex.I * ↑ ↑ k1 * ↑ n * ↑ T . a ) ) * Complex.exp ( Complex.I * ↑ ↑ k2 * ↑ n * ↑ T . a ) = ω ^ n hω_pow : ω ^ T . N = 1 hω_ne_one : ω ≠ 1 ⊢ 0 = 0 All goals completed! 🐙 ] All goals completed! 🐙
F.3. The energy eigenvalues
F.4. The time-independent Schrodinger equation
The energy eigenstates satisfy the time-independent Schrodinger equation.
lemma hamiltonian_energyEigenstate ( k : T . QuantaWaveNumber ) :
T . hamiltonian ( T . energyEigenstate k ) = T . energyEigenvalue k • T . energyEigenstate k := by T : TightBindingChain k : ↑ T . QuantaWaveNumber ⊢ T . hamiltonian ( T . energyEigenstate k ) = T . energyEigenvalue k • T . energyEigenstate k
trans ( T . energyEigenvalue k : ℂ ) • T . energyEigenstate k T : TightBindingChain k : ↑ T . QuantaWaveNumber ⊢ T . hamiltonian ( T . energyEigenstate k ) = ↑ ( T . energyEigenvalue k ) • T . energyEigenstate k T : TightBindingChain k : ↑ T . QuantaWaveNumber ⊢ ↑ ( T . energyEigenvalue k ) • T . energyEigenstate k = T . energyEigenvalue k • T . energyEigenstate k
swap T : TightBindingChain k : ↑ T . QuantaWaveNumber ⊢ ↑ ( T . energyEigenvalue k ) • T . energyEigenstate k = T . energyEigenvalue k • T . energyEigenstate k T : TightBindingChain k : ↑ T . QuantaWaveNumber ⊢ T . hamiltonian ( T . energyEigenstate k ) = ↑ ( T . energyEigenvalue k ) • T . energyEigenstate k
· T : TightBindingChain k : ↑ T . QuantaWaveNumber ⊢ ↑ ( T . energyEigenvalue k ) • T . energyEigenstate k = T . energyEigenvalue k • T . energyEigenstate k rfl All goals completed! 🐙
rw [ energyEigenstate T : TightBindingChain k : ↑ T . QuantaWaveNumber ⊢ T . hamiltonian (∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState n ) =
↑ ( T . energyEigenvalue k ) • ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState n T : TightBindingChain k : ↑ T . QuantaWaveNumber ⊢ T . hamiltonian (∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState n ) =
↑ ( T . energyEigenvalue k ) • ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState n ] T : TightBindingChain k : ↑ T . QuantaWaveNumber ⊢ T . hamiltonian (∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState n ) =
↑ ( T . energyEigenvalue k ) • ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState n
have hp1 : ( ∑ n : Fin T . N , Complex.exp ( Complex.I * k * n * T . a ) • | n + 1 ⟩ )
= ∑ n : Fin T . N , Complex.exp ( Complex.I * k * ( n - 1 ) . val * T . a ) • | n ⟩ := by T : TightBindingChain k : ↑ T . QuantaWaveNumber ⊢ T . hamiltonian ( T . energyEigenstate k ) = T . energyEigenvalue k • T . energyEigenstate k T : TightBindingChain k : ↑ T . QuantaWaveNumber hp1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n + 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) • localizedState n ⊢ T . hamiltonian (∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState n ) =
↑ ( T . energyEigenvalue k ) • ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState n
conv_rhs => rw [ ← Equiv.sum_comp ( Equiv.addRight ( 1 : Fin T . N ) ) ] T : TightBindingChain k : ↑ T . QuantaWaveNumber | ∑ i , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( ( Equiv.addRight 1 ) i - 1 ) * ↑ T . a ) • localizedState ( ( Equiv.addRight 1 ) i ) T : TightBindingChain k : ↑ T . QuantaWaveNumber hp1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n + 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) • localizedState n ⊢ T . hamiltonian (∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState n ) =
↑ ( T . energyEigenvalue k ) • ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState n
simp [ Equiv.coe_addRight , add_sub_cancel_right ] T : TightBindingChain k : ↑ T . QuantaWaveNumber hp1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n + 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) • localizedState n ⊢ T . hamiltonian (∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState n ) =
↑ ( T . energyEigenvalue k ) • ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState n T : TightBindingChain k : ↑ T . QuantaWaveNumber hp1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n + 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) • localizedState n ⊢ T . hamiltonian (∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState n ) =
↑ ( T . energyEigenvalue k ) • ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState n
have hm1 : ( ∑ n : Fin T . N , Complex.exp ( Complex.I * k * n * T . a ) • | n - 1 ⟩ )
= ∑ n : Fin T . N , Complex.exp ( Complex.I * k * ( n + 1 ) . val * T . a ) • | n ⟩ := by T : TightBindingChain k : ↑ T . QuantaWaveNumber ⊢ T . hamiltonian ( T . energyEigenstate k ) = T . energyEigenvalue k • T . energyEigenstate k T : TightBindingChain k : ↑ T . QuantaWaveNumber hp1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n + 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) • localizedState n hm1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n - 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) • localizedState n ⊢ T . hamiltonian (∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState n ) =
↑ ( T . energyEigenvalue k ) • ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState n
conv_rhs => rw [ ← Equiv.sum_comp ( Equiv.subRight ( 1 : Fin T . N ) ) ] T : TightBindingChain k : ↑ T . QuantaWaveNumber hp1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n + 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) • localizedState n | ∑ i , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( ( Equiv.subRight 1 ) i + 1 ) * ↑ T . a ) • localizedState ( ( Equiv.subRight 1 ) i ) T : TightBindingChain k : ↑ T . QuantaWaveNumber hp1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n + 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) • localizedState n hm1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n - 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) • localizedState n ⊢ T . hamiltonian (∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState n ) =
↑ ( T . energyEigenvalue k ) • ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState n
simp [ Equiv.subRight_apply , sub_add_cancel ] T : TightBindingChain k : ↑ T . QuantaWaveNumber hp1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n + 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) • localizedState n hm1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n - 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) • localizedState n ⊢ T . hamiltonian (∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState n ) =
↑ ( T . energyEigenvalue k ) • ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState n T : TightBindingChain k : ↑ T . QuantaWaveNumber hp1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n + 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) • localizedState n hm1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n - 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) • localizedState n ⊢ T . hamiltonian (∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState n ) =
↑ ( T . energyEigenvalue k ) • ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState n
calc
_ = ∑ n : Fin T . N , Complex.exp ( Complex.I * k * n * T . a ) • T . hamiltonian | n ⟩ := by T : TightBindingChain k : ↑ T . QuantaWaveNumber hp1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n + 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) • localizedState n hm1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n - 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) • localizedState n ⊢ T . hamiltonian (∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState n ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • T . hamiltonian ( localizedState n ) simp All goals completed! 🐙
_ = ∑ n : Fin T . N , Complex.exp ( Complex.I * k * n * T . a ) • ( T . E0 • | n ⟩
- T . t • ( | n + 1 ⟩ + | n - 1 ⟩ ) ) := by T : TightBindingChain k : ↑ T . QuantaWaveNumber hp1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n + 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) • localizedState n hm1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n - 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) • localizedState n ⊢ ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • T . hamiltonian ( localizedState n ) =
∑ n ,
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) •
( T . E0 • localizedState n - T . t • ( localizedState ( n + 1 ) + localizedState ( n - 1 ) ) )
simp [ hamiltonian_apply_localizedState , Complex.coe_smul , smul_add ] All goals completed! 🐙
_ = T . E0 • ( ∑ n : Fin T . N , Complex.exp ( Complex.I * k * n * T . a ) • | n ⟩ )
- T . t • ( ( ∑ n : Fin T . N , Complex.exp ( Complex.I * k * n * T . a ) • | n + 1 ⟩ ) +
( ∑ n : Fin T . N , Complex.exp ( Complex.I * k * n * T . a ) • | n - 1 ⟩ ) ) := by T : TightBindingChain k : ↑ T . QuantaWaveNumber hp1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n + 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) • localizedState n hm1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n - 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) • localizedState n ⊢ ∑ n ,
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) •
( T . E0 • localizedState n - T . t • ( localizedState ( n + 1 ) + localizedState ( n - 1 ) ) ) =
T . E0 • ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState n -
T . t •
( ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n + 1 ) +
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n - 1 ) )
simp only [ smul_add , Finset.smul_sum , ← Finset.sum_add_distrib , ← Finset.sum_sub_distrib ] T : TightBindingChain k : ↑ T . QuantaWaveNumber hp1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n + 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) • localizedState n hm1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n - 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) • localizedState n ⊢ ∑ x ,
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ x * ↑ T . a ) •
( T . E0 • localizedState x - ( T . t • localizedState ( x + 1 ) + T . t • localizedState ( x - 1 ) ) ) =
∑ x ,
( T . E0 • Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ x * ↑ T . a ) • localizedState x -
( T . t • Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ x * ↑ T . a ) • localizedState ( x + 1 ) +
T . t • Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ x * ↑ T . a ) • localizedState ( x - 1 ) ) )
refine Finset.sum_congr rfl fun n _ => ? _ T : TightBindingChain k : ↑ T . QuantaWaveNumber hp1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n + 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) • localizedState n hm1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n - 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) • localizedState n n : Fin T . N x✝ : n ∈ Finset.univ ⊢ Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) •
( T . E0 • localizedState n - ( T . t • localizedState ( n + 1 ) + T . t • localizedState ( n - 1 ) ) ) =
T . E0 • Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState n -
( T . t • Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n + 1 ) +
T . t • Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n - 1 ) )
module All goals completed! 🐙
_ = T . E0 • ( ∑ n : Fin T . N , Complex.exp ( Complex.I * k * n * T . a ) • | n ⟩ )
- T . t • ( ( ∑ n : Fin T . N , Complex.exp ( Complex.I * k * ( n - 1 ) . val * T . a ) • | n ⟩ ) +
( ∑ n : Fin T . N , Complex.exp ( Complex.I * k * ( n + 1 ) . val * T . a ) • | n ⟩ ) ) := by T : TightBindingChain k : ↑ T . QuantaWaveNumber hp1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n + 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) • localizedState n hm1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n - 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) • localizedState n ⊢ T . E0 • ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState n -
T . t •
( ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n + 1 ) +
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n - 1 ) ) =
T . E0 • ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState n -
T . t •
( ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) • localizedState n +
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) • localizedState n )
rw [ hp1 , T : TightBindingChain k : ↑ T . QuantaWaveNumber hp1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n + 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) • localizedState n hm1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n - 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) • localizedState n ⊢ T . E0 • ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState n -
T . t •
( ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) • localizedState n +
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n - 1 ) ) =
T . E0 • ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState n -
T . t •
( ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) • localizedState n +
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) • localizedState n ) All goals completed! 🐙 hm1 T : TightBindingChain k : ↑ T . QuantaWaveNumber hp1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n + 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) • localizedState n hm1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n - 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) • localizedState n ⊢ T . E0 • ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState n -
T . t •
( ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) • localizedState n +
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) • localizedState n ) =
T . E0 • ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState n -
T . t •
( ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) • localizedState n +
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) • localizedState n ) All goals completed! 🐙 ] All goals completed! 🐙
_ = ∑ n : Fin T . N , ( T . E0 * Complex.exp ( Complex.I * k * n * T . a ) - T . t *
( Complex.exp ( Complex.I * k * ( n - 1 ) . val * T . a ) +
Complex.exp ( Complex.I * k * ( n + 1 ) . val * T . a ) ) ) • | n ⟩ := by T : TightBindingChain k : ↑ T . QuantaWaveNumber hp1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n + 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) • localizedState n hm1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n - 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) • localizedState n ⊢ T . E0 • ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState n -
T . t •
( ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) • localizedState n +
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) • localizedState n ) =
∑ n ,
( ↑ T . E0 * Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) -
↑ T . t * ( Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) + Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) ) ) •
localizedState n
simp [ Finset.smul_sum , ← Finset.sum_add_distrib ,
← add_smul , sub_smul , ← smul_smul , Finset.sum_sub_distrib ] All goals completed! 🐙
rw [ Finset.smul_sum calc.step T : TightBindingChain k : ↑ T . QuantaWaveNumber hp1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n + 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) • localizedState n hm1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n - 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) • localizedState n ⊢ ∑ n ,
( ↑ T . E0 * Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) -
↑ T . t * ( Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) + Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) ) ) •
localizedState n =
∑ x , ↑ ( T . energyEigenvalue k ) • Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ x * ↑ T . a ) • localizedState x calc.step T : TightBindingChain k : ↑ T . QuantaWaveNumber hp1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n + 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) • localizedState n hm1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n - 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) • localizedState n ⊢ ∑ n ,
( ↑ T . E0 * Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) -
↑ T . t * ( Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) + Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) ) ) •
localizedState n =
∑ x , ↑ ( T . energyEigenvalue k ) • Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ x * ↑ T . a ) • localizedState x ] calc.step T : TightBindingChain k : ↑ T . QuantaWaveNumber hp1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n + 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) • localizedState n hm1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n - 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) • localizedState n ⊢ ∑ n ,
( ↑ T . E0 * Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) -
↑ T . t * ( Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) + Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) ) ) •
localizedState n =
∑ x , ↑ ( T . energyEigenvalue k ) • Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ x * ↑ T . a ) • localizedState x
refine Finset.sum_congr rfl fun n _ => ? _ calc.step T : TightBindingChain k : ↑ T . QuantaWaveNumber hp1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n + 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) • localizedState n hm1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n - 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) • localizedState n n : Fin T . N x✝ : n ∈ Finset.univ ⊢ ( ↑ T . E0 * Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) -
↑ T . t * ( Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) + Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) ) ) •
localizedState n =
↑ ( T . energyEigenvalue k ) • Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState n
rw [ smul_smul calc.step T : TightBindingChain k : ↑ T . QuantaWaveNumber hp1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n + 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) • localizedState n hm1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n - 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) • localizedState n n : Fin T . N x✝ : n ∈ Finset.univ ⊢ ( ↑ T . E0 * Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) -
↑ T . t * ( Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) + Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) ) ) •
localizedState n =
( ↑ ( T . energyEigenvalue k ) * Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) ) • localizedState n calc.step T : TightBindingChain k : ↑ T . QuantaWaveNumber hp1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n + 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) • localizedState n hm1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n - 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) • localizedState n n : Fin T . N x✝ : n ∈ Finset.univ ⊢ ( ↑ T . E0 * Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) -
↑ T . t * ( Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) + Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) ) ) •
localizedState n =
( ↑ ( T . energyEigenvalue k ) * Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) ) • localizedState n ] calc.step T : TightBindingChain k : ↑ T . QuantaWaveNumber hp1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n + 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) • localizedState n hm1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n - 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) • localizedState n n : Fin T . N x✝ : n ∈ Finset.univ ⊢ ( ↑ T . E0 * Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) -
↑ T . t * ( Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) + Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) ) ) •
localizedState n =
( ↑ ( T . energyEigenvalue k ) * Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) ) • localizedState n
simp only [ quantaWaveNumber_exp_sub_one , quantaWaveNumber_exp_add_one , energyEigenvalue ,
Complex.ofReal_sub , Complex.ofReal_mul , Complex.ofReal_ofNat , Complex.ofReal_cos ,
Complex.cos.eq_1 ] calc.step T : TightBindingChain k : ↑ T . QuantaWaveNumber hp1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n + 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n - 1 ) * ↑ T . a ) • localizedState n hm1 : ∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) • localizedState ( n - 1 ) =
∑ n , Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ ( n + 1 ) * ↑ T . a ) • localizedState n n : Fin T . N x✝ : n ∈ Finset.univ ⊢ ( ↑ T . E0 * Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) -
↑ T . t *
( Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( - Complex.I * ↑ ↑ k * ↑ T . a ) +
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) * Complex.exp ( Complex.I * ↑ ↑ k * ↑ T . a ) ) ) •
localizedState n =
( ( ↑ T . E0 - 2 * ↑ T . t * ( ( Complex.exp ( ↑ ↑ k * ↑ T . a * Complex.I ) + Complex.exp ( - ( ↑ ↑ k * ↑ T . a ) * Complex.I ) ) / 2 ) ) *
Complex.exp ( Complex.I * ↑ ↑ k * ↑ ↑ n * ↑ T . a ) ) •
localizedState n
ring_nf All goals completed! 🐙