Potential

📁 Source: PhysLean/Particles/StandardModel/HiggsBoson/Potential.lean

Statistics

Metric	Count
Definitions `Potential`, `IsBounded`, `isBounded_iff_of_𝓵_zero`, `neg`, `quadDiscrim`, `toFun`, `μ2`, `𝓵`	8
Theorems `as_quad`, `complete_square`, `eq_zero_iff_of_μSq_nonpos_𝓵_pos`, `isBounded_of_𝓵_pos`, `isBounded_𝓵_nonneg`, `isMaxOn_iff_field_of_𝓵_neg`, `isMaxOn_iff_isMinOn_neg`, `isMinOn_iff_field_of_μSq_nonneg_𝓵_pos`, `isMinOn_iff_field_of_μSq_nonpos_𝓵_pos`, `isMinOn_iff_field_of_𝓵_pos`, `isMinOn_iff_of_μSq_nonneg_𝓵_pos`, `isMinOn_iff_of_μSq_nonpos_𝓵_pos`, `neg_𝓵_quadDiscrim_zero_bound`, `neg_𝓵_sol_exists_iff`, `neg_𝓵_toFun_neg`, `pos_𝓵_quadDiscrim_zero_bound`, `pos_𝓵_sol_exists_iff`, `pos_𝓵_toFun_pos`, `quadDiscrim_eq_sqrt_mul_sqrt`, `quadDiscrim_eq_zero_iff`, `quadDiscrim_eq_zero_iff_normSq`, `quadDiscrim_nonneg`, `toFun_eq_zero_iff`, `toFun_neg`, `toFun_smooth`, `toFun_zero`, `μ2_neg`, `𝓵_neg`	28
Total	36

StandardModel.HiggsField

Definitions

Name	Category	Theorems
`Potential` 📖	CompData	—

StandardModel.HiggsField.Potential

Definitions

Name	Category	Theorems
`IsBounded` 📖	MathDef	1 math math: `isBounded_of_𝓵_pos`
`isBounded_iff_of_𝓵_zero` 📖	CompOp	—
`neg` 📖	CompOp	4 math math: `μ2_neg`, `isMaxOn_iff_isMinOn_neg`, `𝓵_neg`, `toFun_neg`
`quadDiscrim` 📖	CompOp	4 math math: `quadDiscrim_eq_zero_iff`, `quadDiscrim_eq_zero_iff_normSq`, `quadDiscrim_nonneg`, `quadDiscrim_eq_sqrt_mul_sqrt`
`toFun` 📖	CompOp	21 math math: `quadDiscrim_eq_zero_iff`, `isMinOn_iff_of_μSq_nonpos_𝓵_pos`, `pos_𝓵_sol_exists_iff`, `pos_𝓵_toFun_pos`, `as_quad`, `isMinOn_iff_field_of_μSq_nonneg_𝓵_pos`, `toFun_smooth`, `neg_𝓵_toFun_neg`, `pos_𝓵_quadDiscrim_zero_bound`, `neg_𝓵_sol_exists_iff`, `eq_zero_iff_of_μSq_nonpos_𝓵_pos`, `isMaxOn_iff_field_of_𝓵_neg`, `toFun_zero`, `isMaxOn_iff_isMinOn_neg`, `neg_𝓵_quadDiscrim_zero_bound`, `isMinOn_iff_of_μSq_nonneg_𝓵_pos`, `isMinOn_iff_field_of_𝓵_pos`, `toFun_eq_zero_iff`, `isMinOn_iff_field_of_μSq_nonpos_𝓵_pos`, `toFun_neg`, `complete_square`
`μ2` 📖	CompOp	14 math math: `quadDiscrim_eq_zero_iff`, `pos_𝓵_sol_exists_iff`, `pos_𝓵_toFun_pos`, `as_quad`, `neg_𝓵_toFun_neg`, `pos_𝓵_quadDiscrim_zero_bound`, `neg_𝓵_sol_exists_iff`, `isMaxOn_iff_field_of_𝓵_neg`, `μ2_neg`, `quadDiscrim_eq_zero_iff_normSq`, `neg_𝓵_quadDiscrim_zero_bound`, `isMinOn_iff_field_of_𝓵_pos`, `toFun_eq_zero_iff`, `complete_square`
`𝓵` 📖	CompOp	7 math math: `quadDiscrim_eq_zero_iff`, `isBounded_𝓵_nonneg`, `as_quad`, `quadDiscrim_eq_zero_iff_normSq`, `𝓵_neg`, `toFun_eq_zero_iff`, `complete_square`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`as_quad` 📖	mathematical	—	`𝓵` `StandardModel.HiggsField.normSq` `μ2` `toFun`	—	—
`complete_square` 📖	mathematical	—	`toFun` `𝓵` `StandardModel.HiggsField.normSq` `μ2`	—	—
`eq_zero_iff_of_μSq_nonpos_𝓵_pos` 📖	mathematical	`𝓵` `μ2`	`toFun` `StandardModel.HiggsField` `SpaceTime` `StandardModel.HiggsBundle` `Lorentz.Vector` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector.asSmoothManifold` `Lorentz.Vector.instChartedSpace` `StandardModel.HiggsVec`	—	`toFun_eq_zero_iff` `StandardModel.HiggsField.normSq_nonneg`
`isBounded_of_𝓵_pos` 📖	mathematical	`𝓵`	`IsBounded`	—	`pos_𝓵_quadDiscrim_zero_bound`
`isBounded_𝓵_nonneg` 📖	mathematical	`IsBounded`	`𝓵`	—	`neg_𝓵_sol_exists_iff`
`isMaxOn_iff_field_of_𝓵_neg` 📖	mathematical	`𝓵`	`StandardModel.HiggsField` `SpaceTime` `toFun` `μ2` `StandardModel.HiggsField.normSq` `StandardModel.HiggsBundle` `Lorentz.Vector` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector.asSmoothManifold` `Lorentz.Vector.instChartedSpace` `StandardModel.HiggsVec`	—	`isMaxOn_iff_isMinOn_neg` `isMinOn_iff_field_of_𝓵_pos` `𝓵_neg` `μ2_neg`
`isMaxOn_iff_isMinOn_neg` 📖	mathematical	—	`StandardModel.HiggsField` `SpaceTime` `toFun` `neg`	—	`toFun_neg`
`isMinOn_iff_field_of_μSq_nonneg_𝓵_pos` 📖	mathematical	`𝓵` `μ2`	`StandardModel.HiggsField` `SpaceTime` `toFun` `StandardModel.HiggsField.normSq`	—	`isMinOn_iff_of_μSq_nonneg_𝓵_pos` `quadDiscrim_eq_zero_iff_normSq` `quadDiscrim_eq_zero_iff`
`isMinOn_iff_field_of_μSq_nonpos_𝓵_pos` 📖	mathematical	`𝓵` `μ2`	`StandardModel.HiggsField` `SpaceTime` `toFun` `StandardModel.HiggsBundle` `Lorentz.Vector` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector.asSmoothManifold` `Lorentz.Vector.instChartedSpace` `StandardModel.HiggsVec`	—	`isMinOn_iff_of_μSq_nonpos_𝓵_pos` `eq_zero_iff_of_μSq_nonpos_𝓵_pos`
`isMinOn_iff_field_of_𝓵_pos` 📖	mathematical	`𝓵`	`StandardModel.HiggsField` `SpaceTime` `toFun` `μ2` `StandardModel.HiggsField.normSq` `StandardModel.HiggsBundle` `Lorentz.Vector` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector.asSmoothManifold` `Lorentz.Vector.instChartedSpace` `StandardModel.HiggsVec`	—	`isMinOn_iff_field_of_μSq_nonneg_𝓵_pos` `isMinOn_iff_field_of_μSq_nonpos_𝓵_pos`
`isMinOn_iff_of_μSq_nonneg_𝓵_pos` 📖	mathematical	`𝓵` `μ2`	`StandardModel.HiggsField` `SpaceTime` `toFun`	—	`pos_𝓵_sol_exists_iff`
`isMinOn_iff_of_μSq_nonpos_𝓵_pos` 📖	mathematical	`𝓵` `μ2`	`StandardModel.HiggsField` `SpaceTime` `toFun`	—	`pos_𝓵_sol_exists_iff` `toFun_zero`
`neg_𝓵_quadDiscrim_zero_bound` 📖	mathematical	`𝓵`	`toFun` `μ2`	—	`quadDiscrim_nonneg`
`neg_𝓵_sol_exists_iff` 📖	mathematical	`𝓵`	`toFun` `μ2`	—	`neg_𝓵_toFun_neg` `neg_𝓵_quadDiscrim_zero_bound` `StandardModel.HiggsVec.ofReal_normSq`
`neg_𝓵_toFun_neg` 📖	mathematical	`𝓵`	`μ2` `toFun`	—	—
`pos_𝓵_quadDiscrim_zero_bound` 📖	mathematical	`𝓵`	`μ2` `toFun`	—	`neg_𝓵_quadDiscrim_zero_bound` `toFun_neg` `μ2_neg` `𝓵_neg`
`pos_𝓵_sol_exists_iff` 📖	mathematical	`𝓵`	`toFun` `μ2`	—	`neg_𝓵_sol_exists_iff` `𝓵_neg` `toFun_neg` `μ2_neg`
`pos_𝓵_toFun_pos` 📖	mathematical	`𝓵`	`μ2` `toFun`	—	`μ2_neg` `toFun_neg` `neg_𝓵_toFun_neg` `𝓵_neg`
`quadDiscrim_eq_sqrt_mul_sqrt` 📖	mathematical	—	`quadDiscrim`	—	`quadDiscrim_nonneg`
`quadDiscrim_eq_zero_iff` 📖	mathematical	—	`quadDiscrim` `toFun` `μ2` `𝓵`	—	`quadDiscrim.eq_1`
`quadDiscrim_eq_zero_iff_normSq` 📖	mathematical	—	`quadDiscrim` `StandardModel.HiggsField.normSq` `μ2` `𝓵`	—	`quadDiscrim_eq_zero_iff` `as_quad` `toFun.eq_1`
`quadDiscrim_nonneg` 📖	mathematical	—	`quadDiscrim`	—	`as_quad`
`toFun_eq_zero_iff` 📖	mathematical	—	`toFun` `StandardModel.HiggsField` `SpaceTime` `StandardModel.HiggsBundle` `Lorentz.Vector` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector.asSmoothManifold` `Lorentz.Vector.instChartedSpace` `StandardModel.HiggsVec` `StandardModel.HiggsField.normSq` `μ2` `𝓵`	—	`as_quad`
`toFun_neg` 📖	mathematical	—	`toFun` `neg`	—	—
`toFun_smooth` 📖	mathematical	—	`SpaceTime` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector.instChartedSpace` `toFun`	—	`StandardModel.HiggsField.normSq_smooth`
`toFun_zero` 📖	mathematical	—	`toFun` `StandardModel.HiggsField` `Lorentz.Vector` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.isNormedSpace` `Lorentz.Vector.asSmoothManifold` `SpaceTime` `Lorentz.Vector.instChartedSpace` `StandardModel.HiggsVec` `StandardModel.HiggsBundle`	—	—
`μ2_neg` 📖	mathematical	—	`μ2` `neg`	—	—
`𝓵_neg` 📖	mathematical	—	`𝓵` `neg`	—	—

---

← Back to Index