GramMatrix

📁 Source: PhysLean/Particles/BeyondTheStandardModel/TwoHDM/GramMatrix.lean

Statistics

Metric	Count
Definitions `gramMatrix`, `gramVector`	2
Theorems `eq_fst_norm_of_eq_gramMatrix`, `eq_snd_norm_of_eq_gramMatrix`, `gaugeGroupI_exists_fst_eq`, `gaugeGroupI_exists_fst_eq_snd_eq`, `gaugeGroupI_smul_fst_gramVector`, `gaugeGroupI_smul_gramMatrix`, `gramMatrix_det_eq`, `gramMatrix_det_eq_gramVector`, `gramMatrix_det_eq_real`, `gramMatrix_det_nonneg`, `gramMatrix_eq_component_gramVector`, `gramMatrix_eq_gramVector_sum_pauliMatrix`, `gramMatrix_selfAdjoint`, `gramMatrix_surjective_det_tr`, `gramMatrix_tr_nonneg`, `gramVector_inl_eq_trace_gramMatrix`, `gramVector_inl_nonneg`, `gramVector_inl_zero_eq`, `gramVector_inl_zero_eq_gramMatrix`, `gramVector_inr_one_eq`, `gramVector_inr_one_eq_gramMatrix`, `gramVector_inr_sum_sq_le_inl`, `gramVector_inr_two_eq`, `gramVector_inr_two_eq_gramMatrix`, `gramVector_inr_zero_eq`, `gramVector_inr_zero_eq_gramMatrix`, `gramVector_surjective`, `mem_orbit_gaugeGroupI_iff_gramMatrix`, `normSq_Φ1_eq_gramVector`, `normSq_Φ2_eq_gramVector`, `Φ1_inner_Φ2_eq_gramVector`, `Φ1_inner_Φ2_normSq_eq_gramVector`, `Φ2_inner_Φ1_eq_gramVector`	33
Total	35

TwoHiggsDoublet

Definitions

Name	Category	Theorems
`gramMatrix` 📖	CompOp	18 math math: `gramMatrix_det_nonneg`, `gramVector_inl_zero_eq_gramMatrix`, `gramMatrix_eq_gramVector_sum_pauliMatrix`, `gaugeGroupI_smul_gramMatrix`, `gramVector_inr_zero_eq_gramMatrix`, `gaugeGroupI_exists_fst_eq`, `gramMatrix_eq_component_gramVector`, `gramMatrix_tr_nonneg`, `gaugeGroupI_exists_fst_eq_snd_eq`, `gramMatrix_det_eq_real`, `gramVector_inr_one_eq_gramMatrix`, `gramMatrix_surjective_det_tr`, `gramMatrix_selfAdjoint`, `gramMatrix_det_eq_gramVector`, `gramVector_inl_eq_trace_gramMatrix`, `gramVector_inr_two_eq_gramMatrix`, `gramMatrix_det_eq`, `mem_orbit_gaugeGroupI_iff_gramMatrix`
`gramVector` 📖	CompOp	23 math math: `gramVector_inl_zero_eq_gramMatrix`, `gramVector_surjective`, `gramMatrix_eq_gramVector_sum_pauliMatrix`, `gramVector_inr_one_eq`, `normSq_Φ2_eq_gramVector`, `massTerm_eq_gramVector`, `gramVector_inl_zero_eq`, `gramVector_inr_zero_eq_gramMatrix`, `gramMatrix_eq_component_gramVector`, `gramVector_inr_one_eq_gramMatrix`, `normSq_Φ1_eq_gramVector`, `Φ2_inner_Φ1_eq_gramVector`, `gramVector_inr_two_eq`, `gramVector_inr_sum_sq_le_inl`, `gramVector_inr_zero_eq`, `gramMatrix_det_eq_gramVector`, `quarticTerm_eq_gramVector`, `gramVector_inl_nonneg`, `gramVector_inl_eq_trace_gramMatrix`, `Φ1_inner_Φ2_eq_gramVector`, `gramVector_inr_two_eq_gramMatrix`, `Φ1_inner_Φ2_normSq_eq_gramVector`, `gaugeGroupI_smul_fst_gramVector`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_fst_norm_of_eq_gramMatrix` 📖	mathematical	`gramMatrix`	`StandardModel.HiggsVec` `Φ1`	—	`gramMatrix.eq_1`
`eq_snd_norm_of_eq_gramMatrix` 📖	mathematical	`gramMatrix`	`StandardModel.HiggsVec` `Φ2`	—	`gramMatrix.eq_1`
`gaugeGroupI_exists_fst_eq` 📖	mathematical	—	`StandardModel.GaugeGroupI` `StandardModel.HiggsVec` `StandardModel.HiggsVec.instSMulGaugeGroupI` `Φ1` `Φ2` `gramMatrix`	—	`gramMatrix_det_eq_real` `StandardModel.HiggsVec.mem_orbit_gaugeGroupI_iff` `StandardModel.HiggsVec.gaugeGroupI_smul_inner` `StandardModel.HiggsVec.gaugeGroupI_smul_norm`
`gaugeGroupI_exists_fst_eq_snd_eq` 📖	mathematical	—	`StandardModel.GaugeGroupI` `StandardModel.HiggsVec` `StandardModel.HiggsVec.instSMulGaugeGroupI` `Φ1` `Φ2` `gramMatrix`	—	`gaugeGroupI_exists_fst_eq` `StandardModel.HiggsVec.gaugeGroupI_smul_phase_snd`
`gaugeGroupI_smul_fst_gramVector` 📖	mathematical	—	`gramVector` `StandardModel.GaugeGroupI` `TwoHiggsDoublet` `instSMulGaugeGroupI`	—	`gramMatrix_selfAdjoint` `gramVector.eq_1` `gaugeGroupI_smul_gramMatrix`
`gaugeGroupI_smul_gramMatrix` 📖	mathematical	—	`gramMatrix` `StandardModel.GaugeGroupI` `TwoHiggsDoublet` `instSMulGaugeGroupI`	—	`gramMatrix.eq_1` `gaugeGroupI_smul_fst` `gaugeGroupI_smul_snd` `StandardModel.HiggsVec.gaugeGroupI_smul_norm` `StandardModel.HiggsVec.gaugeGroupI_smul_inner`
`gramMatrix_det_eq` 📖	mathematical	—	`gramMatrix` `StandardModel.HiggsVec` `Φ1` `Φ2`	—	`gramMatrix.eq_1`
`gramMatrix_det_eq_gramVector` 📖	mathematical	—	`gramMatrix` `gramVector`	—	`gramMatrix_det_eq_real` `normSq_Φ1_eq_gramVector` `normSq_Φ2_eq_gramVector` `Φ1_inner_Φ2_normSq_eq_gramVector`
`gramMatrix_det_eq_real` 📖	mathematical	—	`gramMatrix` `StandardModel.HiggsVec` `Φ1` `Φ2`	—	`gramMatrix_det_eq`
`gramMatrix_det_nonneg` 📖	mathematical	—	`gramMatrix`	—	`gramMatrix_det_eq_real`
`gramMatrix_eq_component_gramVector` 📖	mathematical	—	`gramMatrix` `gramVector`	—	`gramMatrix_eq_gramVector_sum_pauliMatrix`
`gramMatrix_eq_gramVector_sum_pauliMatrix` 📖	mathematical	—	`gramMatrix` `gramVector` `PauliMatrix.pauliMatrix`	—	`gramMatrix_selfAdjoint` `PauliMatrix.pauliSelfAdjoint_linearly_independent` `PauliMatrix.pauliSelfAdjoint_span`
`gramMatrix_selfAdjoint` 📖	mathematical	—	`gramMatrix`	—	`gramMatrix.eq_1`
`gramMatrix_surjective_det_tr` 📖	mathematical	—	`gramMatrix`	—	—
`gramMatrix_tr_nonneg` 📖	mathematical	—	`gramMatrix`	—	`gramMatrix.eq_1`
`gramVector_inl_eq_trace_gramMatrix` 📖	mathematical	—	`gramVector` `gramMatrix`	—	`gramMatrix_eq_component_gramVector`
`gramVector_inl_nonneg` 📖	mathematical	—	`gramVector`	—	`gramVector_inl_eq_trace_gramMatrix` `gramMatrix_tr_nonneg`
`gramVector_inl_zero_eq` 📖	mathematical	—	`gramVector` `StandardModel.HiggsVec` `Φ1` `Φ2`	—	`normSq_Φ1_eq_gramVector` `normSq_Φ2_eq_gramVector`
`gramVector_inl_zero_eq_gramMatrix` 📖	mathematical	—	`gramVector` `gramMatrix`	—	`gramVector_inl_zero_eq`
`gramVector_inr_one_eq` 📖	mathematical	—	`gramVector` `StandardModel.HiggsVec` `Φ1` `Φ2`	—	`Φ1_inner_Φ2_eq_gramVector`
`gramVector_inr_one_eq_gramMatrix` 📖	mathematical	—	`gramVector` `gramMatrix`	—	`gramMatrix.eq_1` `gramVector_inr_one_eq`
`gramVector_inr_sum_sq_le_inl` 📖	mathematical	—	`gramVector`	—	`gramMatrix_det_nonneg` `gramMatrix_det_eq_gramVector`
`gramVector_inr_two_eq` 📖	mathematical	—	`gramVector` `StandardModel.HiggsVec` `Φ1` `Φ2`	—	`normSq_Φ1_eq_gramVector` `normSq_Φ2_eq_gramVector`
`gramVector_inr_two_eq_gramMatrix` 📖	mathematical	—	`gramVector` `gramMatrix`	—	`gramVector_inr_two_eq`
`gramVector_inr_zero_eq` 📖	mathematical	—	`gramVector` `StandardModel.HiggsVec` `Φ1` `Φ2`	—	`Φ1_inner_Φ2_eq_gramVector`
`gramVector_inr_zero_eq_gramMatrix` 📖	mathematical	—	`gramVector` `gramMatrix`	—	`gramMatrix.eq_1` `gramVector_inr_zero_eq`
`gramVector_surjective` 📖	mathematical	—	`gramVector`	—	`gramMatrix_surjective_det_tr` `gramVector_inl_zero_eq_gramMatrix` `gramVector_inr_zero_eq_gramMatrix` `gramVector_inr_one_eq_gramMatrix` `gramVector_inr_two_eq_gramMatrix`
`mem_orbit_gaugeGroupI_iff_gramMatrix` 📖	mathematical	—	`TwoHiggsDoublet` `StandardModel.GaugeGroupI` `instSMulGaugeGroupI` `gramMatrix`	—	`gaugeGroupI_smul_gramMatrix` `StandardModel.HiggsVec.mem_orbit_gaugeGroupI_iff` `ext_of_fst_snd` `eq_fst_norm_of_eq_gramMatrix` `eq_snd_norm_of_eq_gramMatrix` `gaugeGroupI_exists_fst_eq_snd_eq`
`normSq_Φ1_eq_gramVector` 📖	mathematical	—	`StandardModel.HiggsVec` `Φ1` `gramVector`	—	`gramMatrix_eq_component_gramVector`
`normSq_Φ2_eq_gramVector` 📖	mathematical	—	`StandardModel.HiggsVec` `Φ2` `gramVector`	—	`gramMatrix_eq_component_gramVector`
`Φ1_inner_Φ2_eq_gramVector` 📖	mathematical	—	`StandardModel.HiggsVec` `Φ1` `Φ2` `gramVector`	—	`gramMatrix_eq_component_gramVector`
`Φ1_inner_Φ2_normSq_eq_gramVector` 📖	mathematical	—	`StandardModel.HiggsVec` `Φ1` `Φ2` `gramVector`	—	`Φ1_inner_Φ2_eq_gramVector` `Φ2_inner_Φ1_eq_gramVector`
`Φ2_inner_Φ1_eq_gramVector` 📖	mathematical	—	`StandardModel.HiggsVec` `Φ2` `Φ1` `gramVector`	—	`gramMatrix_eq_component_gramVector`

---

← Back to Index