DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Update BoundPlaneDim.lean

Browse source
This commit is contained in:
Pietro Monticone 2024-08-31 18:08:57 +02:00
parent 56e4d6cf40
commit fc71ed0aad
1 changed files with 3 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

10
HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean
View file

@ -24,19 +24,15 @@ open BigOperators
/-- A proposition which is true if for a given `n`, a plane of charges of dimension `n` exists
in which each point is a solution. -/
def ExistsPlane (n : ℕ) : Prop := ∃ (B : Fin n → (PlusU1 3).Charges),
LinearIndependent ℚ B ∧ ∀ (f : Fin n → ℚ), (PlusU1 3).IsSolution (∑ i, f i • B i)
LinearIndependent ℚ B ∧ ∀ (f : Fin n → ℚ), (PlusU1 3).IsSolution (∑ i, f i • B i)
lemma exists_plane_exists_basis {n : ℕ} (hE : ExistsPlane n) :
∃ (B : Fin 11 ⊕ Fin n → (PlusU1 3).Charges), LinearIndependent ℚ B := by
obtain ⟨E, hE1, hE2⟩ := hE
obtain ⟨B, hB1, hB2⟩ := eleven_dim_plane_of_no_sols_exists
let Y := Sum.elim B E
use Y
apply Fintype.linearIndependent_iff.mpr
intro g hg
rw [@Fintype.sum_sum_type] at hg
rw [@add_eq_zero_iff_eq_neg] at hg
rw [← @Finset.sum_neg_distrib] at hg
refine ⟨Y, Fintype.linearIndependent_iff.mpr fun g hg ↦ ?_⟩
rw [@Fintype.sum_sum_type, @add_eq_zero_iff_eq_neg, ← @Finset.sum_neg_distrib] at hg
have h1 : ∑ x : Fin n, -(g (Sum.inr x) • Y (Sum.inr x)) =
∑ x : Fin n, (-g (Sum.inr x)) • Y (Sum.inr x) := by
apply Finset.sum_congr