Basis of LinSols in the odd case

We give a basis of LinSols in the odd case. This basis has the special property that splits into two planes on which every point is a solution to the ACCs.

theorem PureU1.VectorLikeOddPlane.odd_shift_eq (n : ℕ) : 1 + n + n = 2 * n + 1

theorem PureU1.VectorLikeOddPlane.odd_shift_shift_eq (n : ℕ) : 1 + n + 1 + n.succ = 2 * n.succ + 1

def PureU1.VectorLikeOddPlane.oddFst {n : ℕ} (j : Fin n) : Fin (2 * n + 1)

The inclusion of Fin n into Fin ((n + 1) + n) via the first n. This is then casted to Fin (2 * n + 1).

Equations

• PureU1.VectorLikeOddPlane.oddFst j = Fin.cast ⋯ (Fin.castAdd n (Fin.castAdd 1 j))

def PureU1.VectorLikeOddPlane.oddSnd {n : ℕ} (j : Fin n) : Fin (2 * n + 1)

The inclusion of Fin n into Fin ((n + 1) + n) via the second n. This is then casted to Fin (2 * n + 1).

Equations

• PureU1.VectorLikeOddPlane.oddSnd j = Fin.cast ⋯ (Fin.natAdd (n + 1) j)

def PureU1.VectorLikeOddPlane.oddMid {n : ℕ} : Fin (2 * n + 1)

The element representing 1 in Fin ((n + 1) + n). This is then casted to Fin (2 * n + 1).

Equations

• PureU1.VectorLikeOddPlane.oddMid = Fin.cast ⋯ (Fin.castAdd n (Fin.natAdd n 1))

def PureU1.VectorLikeOddPlane.oddShiftFst {n : ℕ} (j : Fin n) : Fin (2 * n + 1)

The inclusion of Fin n into Fin (1 + n + n) via the first n. This is then casted to Fin (2 * n + 1).

Equations

• PureU1.VectorLikeOddPlane.oddShiftFst j = Fin.cast ⋯ (Fin.castAdd n (Fin.natAdd 1 j))

def PureU1.VectorLikeOddPlane.oddShiftSnd {n : ℕ} (j : Fin n) : Fin (2 * n + 1)

The inclusion of Fin n into Fin (1 + n + n) via the second n. This is then casted to Fin (2 * n + 1).

Equations

• PureU1.VectorLikeOddPlane.oddShiftSnd j = Fin.cast ⋯ (Fin.natAdd (1 + n) j)

def PureU1.VectorLikeOddPlane.oddShiftZero {n : ℕ} : Fin (2 * n + 1)

The element representing the 1 in Fin (1 + n + n). This is then casted to Fin (2 * n + 1).

Equations

• PureU1.VectorLikeOddPlane.oddShiftZero = Fin.cast ⋯ (Fin.castAdd n (Fin.castAdd n 1))

def PureU1.VectorLikeOddPlane.oddShiftShiftZero {n : ℕ} : Fin (2 * n.succ + 1)

The element representing the first 1 in Fin (1 + n + 1 + n.succ) casted to Fin (2 * n.succ + 1).

Equations

• PureU1.VectorLikeOddPlane.oddShiftShiftZero = Fin.cast ⋯ (Fin.castAdd n.succ (Fin.castAdd 1 (Fin.castAdd n 1)))

def PureU1.VectorLikeOddPlane.oddShiftShiftFst {n : ℕ} (j : Fin n) : Fin (2 * n.succ + 1)

The inclusion of Fin n into Fin (1 + n + 1 + n.succ) via the first n and casted to Fin (2 * n.succ + 1).

Equations

• PureU1.VectorLikeOddPlane.oddShiftShiftFst j = Fin.cast ⋯ (Fin.castAdd n.succ (Fin.castAdd 1 (Fin.natAdd 1 j)))

def PureU1.VectorLikeOddPlane.oddShiftShiftMid {n : ℕ} : Fin (2 * n.succ + 1)

The element representing the second 1 in Fin (1 + n + 1 + n.succ) casted to 2 * n.succ + 1.

Equations

• PureU1.VectorLikeOddPlane.oddShiftShiftMid = Fin.cast ⋯ (Fin.castAdd n.succ (Fin.natAdd (1 + n) 1))

def PureU1.VectorLikeOddPlane.oddShiftShiftSnd {n : ℕ} (j : Fin n.succ) : Fin (2 * n.succ + 1)

The inclusion of Fin n.succ into Fin (1 + n + 1 + n.succ) via the n.succ and casted to Fin (2 * n.succ + 1).

Equations

• PureU1.VectorLikeOddPlane.oddShiftShiftSnd j = Fin.cast ⋯ (Fin.natAdd (1 + n + 1) j)

theorem PureU1.VectorLikeOddPlane.oddShiftShiftZero_eq_oddFst_zero {n : ℕ} : oddShiftShiftZero = oddFst 0

theorem PureU1.VectorLikeOddPlane.oddShiftShiftZero_eq_oddShiftZero {n : ℕ} : oddShiftShiftZero = oddShiftZero

theorem PureU1.VectorLikeOddPlane.oddShiftShiftFst_eq_oddFst_succ {n : ℕ} (j : Fin n) : oddShiftShiftFst j = oddFst j.succ

theorem PureU1.VectorLikeOddPlane.oddShiftShiftFst_eq_oddShiftFst_castSucc {n : ℕ} (j : Fin n) : oddShiftShiftFst j = oddShiftFst j.castSucc

theorem PureU1.VectorLikeOddPlane.oddShiftShiftMid_eq_oddMid {n : ℕ} : oddShiftShiftMid = oddMid

theorem PureU1.VectorLikeOddPlane.oddShiftShiftMid_eq_oddShiftFst_last {n : ℕ} : oddShiftShiftMid = oddShiftFst (Fin.last n)

theorem PureU1.VectorLikeOddPlane.oddShiftShiftSnd_eq_oddSnd {n : ℕ} (j : Fin n.succ) : oddShiftShiftSnd j = oddSnd j

theorem PureU1.VectorLikeOddPlane.oddShiftShiftSnd_eq_oddShiftSnd {n : ℕ} (j : Fin n.succ) : oddShiftShiftSnd j = oddShiftSnd j

theorem PureU1.VectorLikeOddPlane.oddSnd_eq_oddShiftSnd {n : ℕ} (j : Fin n) : oddSnd j = oddShiftSnd j

theorem PureU1.VectorLikeOddPlane.sum_odd {n : ℕ} (S : Fin (2 * n + 1) → ℚ) : ∑ i : Fin (2 * n + 1), S i = S oddMid + ∑ i : Fin n, ((S ∘ oddFst) i + (S ∘ oddSnd) i)

theorem PureU1.VectorLikeOddPlane.sum_oddShift {n : ℕ} (S : Fin (2 * n + 1) → ℚ) : ∑ i : Fin (2 * n + 1), S i = S oddShiftZero + ∑ i : Fin n, ((S ∘ oddShiftFst) i + (S ∘ oddShiftSnd) i)

def PureU1.VectorLikeOddPlane.basisAsCharges {n : ℕ} (j : Fin n) : (PureU1 (2 * n + 1)).Charges

The first part of the basis as charge assignments.

Equations

• PureU1.VectorLikeOddPlane.basisAsCharges j i = if i = PureU1.VectorLikeOddPlane.oddFst j then 1 else if i = PureU1.VectorLikeOddPlane.oddSnd j then -1 else 0

def PureU1.VectorLikeOddPlane.basis!AsCharges {n : ℕ} (j : Fin n) : (PureU1 (2 * n + 1)).Charges

The second part of the basis as charge assignments.

Equations

• PureU1.VectorLikeOddPlane.basis!AsCharges j i = if i = PureU1.VectorLikeOddPlane.oddShiftFst j then 1 else if i = PureU1.VectorLikeOddPlane.oddShiftSnd j then -1 else 0

theorem PureU1.VectorLikeOddPlane.basis_on_oddFst_self {n : ℕ} (j : Fin n) : basisAsCharges j (oddFst j) = 1

theorem PureU1.VectorLikeOddPlane.basis!_on_oddShiftFst_self {n : ℕ} (j : Fin n) : basis!AsCharges j (oddShiftFst j) = 1

theorem PureU1.VectorLikeOddPlane.basis_on_oddFst_other {n : ℕ} {k j : Fin n} (h : k ≠ j) : basisAsCharges k (oddFst j) = 0

theorem PureU1.VectorLikeOddPlane.basis!_on_oddShiftFst_other {n : ℕ} {k j : Fin n} (h : k ≠ j) : basis!AsCharges k (oddShiftFst j) = 0

theorem PureU1.VectorLikeOddPlane.basis_on_other {n : ℕ} {k : Fin n} {j : Fin (2 * n + 1)} (h1 : j ≠ oddFst k) (h2 : j ≠ oddSnd k) : basisAsCharges k j = 0

theorem PureU1.VectorLikeOddPlane.basis!_on_other {n : ℕ} {k : Fin n} {j : Fin (2 * n + 1)} (h1 : j ≠ oddShiftFst k) (h2 : j ≠ oddShiftSnd k) : basis!AsCharges k j = 0

theorem PureU1.VectorLikeOddPlane.basis_oddSnd_eq_minus_oddFst {n : ℕ} (j i : Fin n) : basisAsCharges j (oddSnd i) = -basisAsCharges j (oddFst i)

theorem PureU1.VectorLikeOddPlane.basis!_oddShiftSnd_eq_minus_oddShiftFst {n : ℕ} (j i : Fin n) : basis!AsCharges j (oddShiftSnd i) = -basis!AsCharges j (oddShiftFst i)

theorem PureU1.VectorLikeOddPlane.basis_on_oddSnd_self {n : ℕ} (j : Fin n) : basisAsCharges j (oddSnd j) = -1

theorem PureU1.VectorLikeOddPlane.basis!_on_oddShiftSnd_self {n : ℕ} (j : Fin n) : basis!AsCharges j (oddShiftSnd j) = -1

theorem PureU1.VectorLikeOddPlane.basis_on_oddSnd_other {n : ℕ} {k j : Fin n} (h : k ≠ j) : basisAsCharges k (oddSnd j) = 0

theorem PureU1.VectorLikeOddPlane.basis!_on_oddShiftSnd_other {n : ℕ} {k j : Fin n} (h : k ≠ j) : basis!AsCharges k (oddShiftSnd j) = 0

theorem PureU1.VectorLikeOddPlane.basis_on_oddMid {n : ℕ} (j : Fin n) : basisAsCharges j oddMid = 0

theorem PureU1.VectorLikeOddPlane.basis!_on_oddShiftZero {n : ℕ} (j : Fin n) : basis!AsCharges j oddShiftZero = 0

theorem PureU1.VectorLikeOddPlane.basis_linearACC {n : ℕ} (j : Fin n) : (accGrav (2 * n + 1)) (basisAsCharges j) = 0

theorem PureU1.VectorLikeOddPlane.basis!_linearACC {n : ℕ} (j : Fin n) : (accGrav (2 * n + 1)) (basis!AsCharges j) = 0

def PureU1.VectorLikeOddPlane.basis {n : ℕ} (j : Fin n) : (PureU1 (2 * n + 1)).LinSols

The first part of the basis as LinSols.

Equations

• PureU1.VectorLikeOddPlane.basis j = { val := PureU1.VectorLikeOddPlane.basisAsCharges j, linearSol := ⋯ }

@[simp]

theorem PureU1.VectorLikeOddPlane.basis_val {n : ℕ} (j : Fin n) : (basis j).val = basisAsCharges j

def PureU1.VectorLikeOddPlane.basis! {n : ℕ} (j : Fin n) : (PureU1 (2 * n + 1)).LinSols

The second part of the basis as LinSols.

Equations

• PureU1.VectorLikeOddPlane.basis! j = { val := PureU1.VectorLikeOddPlane.basis!AsCharges j, linearSol := ⋯ }

@[simp]

theorem PureU1.VectorLikeOddPlane.basis!_val {n : ℕ} (j : Fin n) : (basis! j).val = basis!AsCharges j

def PureU1.VectorLikeOddPlane.basisa {n : ℕ} : Fin n ⊕ Fin n → (PureU1 (2 * n + 1)).LinSols

The whole basis as LinSols.

Equations

• PureU1.VectorLikeOddPlane.basisa (Sum.inl i_2) = PureU1.VectorLikeOddPlane.basis i_2
• PureU1.VectorLikeOddPlane.basisa (Sum.inr i_2) = PureU1.VectorLikeOddPlane.basis! i_2

theorem PureU1.VectorLikeOddPlane.swap!_as_add {n : ℕ} {S S' : (PureU1 (2 * n + 1)).LinSols} (j : Fin n) (hS : ((FamilyPermutations (2 * n + 1)).linSolRep (pairSwap (oddShiftFst j) (oddShiftSnd j))) S = S') : S'.val = S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j

Swapping the elements oddShiftFst j and oddShiftSnd j is equivalent to adding a vector basis!AsCharges j.

def PureU1.VectorLikeOddPlane.P {n : ℕ} (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).Charges

A point in the span of the first part of the basis as a charge.

Equations

• PureU1.VectorLikeOddPlane.P f = ∑ i : Fin n, f i • PureU1.VectorLikeOddPlane.basisAsCharges i

def PureU1.VectorLikeOddPlane.P! {n : ℕ} (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).Charges

A point in the span of the second part of the basis as a charge.

Equations

• PureU1.VectorLikeOddPlane.P! f = ∑ i : Fin n, f i • PureU1.VectorLikeOddPlane.basis!AsCharges i

def PureU1.VectorLikeOddPlane.Pa {n : ℕ} (f g : Fin n → ℚ) : (PureU1 (2 * n + 1)).Charges

A point in the span of the basis as a charge.

Equations

• PureU1.VectorLikeOddPlane.Pa f g = PureU1.VectorLikeOddPlane.P f + PureU1.VectorLikeOddPlane.P! g

theorem PureU1.VectorLikeOddPlane.P_oddFst {n : ℕ} (f : Fin n → ℚ) (j : Fin n) : P f (oddFst j) = f j

theorem PureU1.VectorLikeOddPlane.P!_oddShiftFst {n : ℕ} (f : Fin n → ℚ) (j : Fin n) : P! f (oddShiftFst j) = f j

theorem PureU1.VectorLikeOddPlane.P_oddSnd {n : ℕ} (f : Fin n → ℚ) (j : Fin n) : P f (oddSnd j) = -f j

theorem PureU1.VectorLikeOddPlane.P!_oddShiftSnd {n : ℕ} (f : Fin n → ℚ) (j : Fin n) : P! f (oddShiftSnd j) = -f j

theorem PureU1.VectorLikeOddPlane.P_oddMid {n : ℕ} (f : Fin n → ℚ) : P f oddMid = 0

theorem PureU1.VectorLikeOddPlane.P!_oddShiftZero {n : ℕ} (f : Fin n → ℚ) : P! f oddShiftZero = 0

theorem PureU1.VectorLikeOddPlane.Pa_oddShiftShiftZero {n : ℕ} (f g : Fin n.succ → ℚ) : Pa f g oddShiftShiftZero = f 0

theorem PureU1.VectorLikeOddPlane.Pa_oddShiftShiftFst {n : ℕ} (f g : Fin n.succ → ℚ) (j : Fin n) : Pa f g (oddShiftShiftFst j) = f j.succ + g j.castSucc

theorem PureU1.VectorLikeOddPlane.Pa_oddShiftShiftMid {n : ℕ} (f g : Fin n.succ → ℚ) : Pa f g oddShiftShiftMid = g (Fin.last n)

theorem PureU1.VectorLikeOddPlane.Pa_oddShiftShiftSnd {n : ℕ} (f g : Fin n.succ → ℚ) (j : Fin n.succ) : Pa f g (oddShiftShiftSnd j) = -f j - g j

theorem PureU1.VectorLikeOddPlane.P_linearACC {n : ℕ} (f : Fin n → ℚ) : (accGrav (2 * n + 1)) (P f) = 0

theorem PureU1.VectorLikeOddPlane.P!_linearACC {n : ℕ} (f : Fin n → ℚ) : (accGrav (2 * n + 1)) (P! f) = 0

theorem PureU1.VectorLikeOddPlane.P_accCube {n : ℕ} (f : Fin n → ℚ) : (accCube (2 * n + 1)) (P f) = 0

theorem PureU1.VectorLikeOddPlane.P!_accCube {n : ℕ} (f : Fin n → ℚ) : (accCube (2 * n + 1)) (P! f) = 0

theorem PureU1.VectorLikeOddPlane.P_P_P!_accCube {n : ℕ} (g : Fin n → ℚ) (j : Fin n) : ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = P g (oddShiftFst j) ^ 2 - g j ^ 2

theorem PureU1.VectorLikeOddPlane.P_zero {n : ℕ} (f : Fin n → ℚ) (h : P f = 0) (i : Fin n) : f i = 0

theorem PureU1.VectorLikeOddPlane.P!_zero {n : ℕ} (f : Fin n → ℚ) (h : P! f = 0) (i : Fin n) : f i = 0

theorem PureU1.VectorLikeOddPlane.Pa_zero {n : ℕ} (f g : Fin n.succ → ℚ) (h : Pa f g = 0) (i : Fin n.succ) : f i = 0

theorem PureU1.VectorLikeOddPlane.Pa_zero! {n : ℕ} (f g : Fin n.succ → ℚ) (h : Pa f g = 0) (i : Fin n.succ) : g i = 0

def PureU1.VectorLikeOddPlane.P' {n : ℕ} (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).LinSols

A point in the span of the first part of the basis.

Equations

• PureU1.VectorLikeOddPlane.P' f = ∑ i : Fin n, f i • PureU1.VectorLikeOddPlane.basis i

def PureU1.VectorLikeOddPlane.P!' {n : ℕ} (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).LinSols

A point in the span of the second part of the basis.

Equations

• PureU1.VectorLikeOddPlane.P!' f = ∑ i : Fin n, f i • PureU1.VectorLikeOddPlane.basis! i

def PureU1.VectorLikeOddPlane.Pa' {n : ℕ} (f : Fin n ⊕ Fin n → ℚ) : (PureU1 (2 * n + 1)).LinSols

A point in the span of the whole basis.

Equations

• PureU1.VectorLikeOddPlane.Pa' f = ∑ i : Fin n ⊕ Fin n, f i • PureU1.VectorLikeOddPlane.basisa i

theorem PureU1.VectorLikeOddPlane.Pa'_P'_P!' {n : ℕ} (f : Fin n ⊕ Fin n → ℚ) : Pa' f = P' (f ∘ Sum.inl) + P!' (f ∘ Sum.inr)

theorem PureU1.VectorLikeOddPlane.P'_val {n : ℕ} (f : Fin n → ℚ) : (P' f).val = P f

theorem PureU1.VectorLikeOddPlane.P!'_val {n : ℕ} (f : Fin n → ℚ) : (P!' f).val = P! f

theorem PureU1.VectorLikeOddPlane.basis_linear_independent {n : ℕ} : LinearIndependent ℚ basis

theorem PureU1.VectorLikeOddPlane.basis!_linear_independent {n : ℕ} : LinearIndependent ℚ basis!

theorem PureU1.VectorLikeOddPlane.basisa_linear_independent {n : ℕ} : LinearIndependent ℚ basisa

theorem PureU1.VectorLikeOddPlane.Pa'_eq {n : ℕ} (f f' : Fin n.succ ⊕ Fin n.succ → ℚ) : Pa' f = Pa' f' ↔ f = f'

def PureU1.VectorLikeOddPlane.join {n : ℕ} (g f : Fin n → ℚ) : Fin n ⊕ Fin n → ℚ

A helper function for what follows.

Equations

• PureU1.VectorLikeOddPlane.join g f (Sum.inl i_2) = g i_2
• PureU1.VectorLikeOddPlane.join g f (Sum.inr i_2) = f i_2

theorem PureU1.VectorLikeOddPlane.join_ext {n : ℕ} (g g' f f' : Fin n → ℚ) : join g f = join g' f' ↔ g = g' ∧ f = f'

theorem PureU1.VectorLikeOddPlane.join_Pa {n : ℕ} (g g' f f' : Fin n.succ → ℚ) : Pa' (join g f) = Pa' (join g' f') ↔ Pa g f = Pa g' f'

theorem PureU1.VectorLikeOddPlane.Pa_eq {n : ℕ} (g g' f f' : Fin n.succ → ℚ) : Pa g f = Pa g' f' ↔ g = g' ∧ f = f'

theorem PureU1.VectorLikeOddPlane.basisa_card {n : ℕ} : Fintype.card (Fin n.succ ⊕ Fin n.succ) = Module.finrank ℚ (PureU1 (2 * n.succ + 1)).LinSols

noncomputable def PureU1.VectorLikeOddPlane.basisaAsBasis {n : ℕ} : Basis (Fin n.succ ⊕ Fin n.succ) ℚ (PureU1 (2 * n.succ + 1)).LinSols

The basis formed out of our basisa vectors.

Equations

• PureU1.VectorLikeOddPlane.basisaAsBasis = basisOfLinearIndependentOfCardEqFinrank ⋯ ⋯

theorem PureU1.VectorLikeOddPlane.span_basis {n : ℕ} (S : (PureU1 (2 * n.succ + 1)).LinSols) : ∃ (g : Fin n.succ → ℚ) (f : Fin n.succ → ℚ), S.val = P g + P! f

theorem PureU1.VectorLikeOddPlane.span_basis_swap! {n : ℕ} {S' S : (PureU1 (2 * n.succ + 1)).LinSols} (j : Fin n.succ) (hS : ((FamilyPermutations (2 * n.succ + 1)).linSolRep (pairSwap (oddShiftFst j) (oddShiftSnd j))) S = S') (g f : Fin n.succ → ℚ) (hS1 : S.val = P g + P! f) : ∃ (g' : Fin n.succ → ℚ) (f' : Fin n.succ → ℚ), S'.val = P g' + P! f' ∧ P! f' = P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∧ g' = g