Defs

📁 Source: PhysLean/Mathematics/Geometry/Metric/PseudoRiemannian/Defs.lean

Statistics

Metric	Count
Definitions `PseudoRiemannianMetric`, `coeFunInst`, `cotangentMetricVal`, `cotangentToBilinForm`, `cotangentToQuadraticForm`, `flat`, `flatEquiv`, `flatL`, `inner`, `sharp`, `sharpEquiv`, `sharpL`, `toBilinForm`, `toQuadraticForm`, `val`, `negDim`	16
Theorems `apply_sharp_sharp`, `apply_vec_sharp`, `coe_flatEquiv`, `coe_sharpEquiv`, `cotangentMetricVal_eq_apply_sharp`, `cotangentMetricVal_nondegenerate`, `cotangentMetricVal_symm`, `cotangentToBilinForm_apply`, `cotangentToBilinForm_isSymm`, `cotangentToBilinForm_nondegenerate`, `cotangentToQuadraticForm_apply`, `ext`, `ext_iff`, `flatEquiv_apply`, `flatL_apply`, `flatL_apply_sharpL`, `flatL_inj`, `flatL_surj`, `flat_apply`, `flat_inj`, `flat_sharp_apply`, `inner_apply`, `negDim_isLocallyConstant`, `nondegenerate`, `sharpL_apply_flatL`, `sharpL_eq_toContinuousLinearMap`, `sharp_flat_apply`, `smooth_in_charts'`, `symm`, `toBilinForm_apply`, `toBilinForm_isSymm`, `toBilinForm_nondegenerate`, `toQuadraticForm_apply`, `weightedSumSquares_basis_vector`, `neg_weight_implies_neg_value`, `posDef_no_neg_weights`, `rankNeg_eq_zero`	37
Total	53

PseudoRiemannianMetric

Definitions

Name	Category	Theorems
`coeFunInst` 📖	CompOp	—
`cotangentMetricVal` 📖	CompOp	4 math math: `cotangentMetricVal_symm`, `cotangentToQuadraticForm_apply`, `cotangentToBilinForm_apply`, `cotangentMetricVal_eq_apply_sharp`
`cotangentToBilinForm` 📖	CompOp	3 math math: `cotangentToBilinForm_isSymm`, `cotangentToBilinForm_apply`, `cotangentToBilinForm_nondegenerate`
`cotangentToQuadraticForm` 📖	CompOp	1 math math: `cotangentToQuadraticForm_apply`
`flat` 📖	CompOp	4 math math: `flat_sharp_apply`, `flat_apply`, `flat_inj`, `sharp_flat_apply`
`flatEquiv` 📖	CompOp	2 math math: `coe_flatEquiv`, `flatEquiv_apply`
`flatL` 📖	CompOp	6 math math: `flatL_apply_sharpL`, `sharpL_apply_flatL`, `flatL_surj`, `coe_flatEquiv`, `flatL_inj`, `flatL_apply`
`inner` 📖	CompOp	1 math math: `inner_apply`
`sharp` 📖	CompOp	2 math math: `flat_sharp_apply`, `sharp_flat_apply`
`sharpEquiv` 📖	CompOp	2 math math: `coe_sharpEquiv`, `sharpL_eq_toContinuousLinearMap`
`sharpL` 📖	CompOp	7 math math: `flatL_apply_sharpL`, `coe_sharpEquiv`, `sharpL_apply_flatL`, `apply_vec_sharp`, `sharpL_eq_toContinuousLinearMap`, `apply_sharp_sharp`, `cotangentMetricVal_eq_apply_sharp`
`toBilinForm` 📖	CompOp	3 math math: `toBilinForm_isSymm`, `toBilinForm_nondegenerate`, `toBilinForm_apply`
`toQuadraticForm` 📖	CompOp	3 math math: `RiemannianMetric.riemannian_metric_negDim_zero`, `toQuadraticForm_apply`, `RiemannianMetric.toQuadraticForm_posDef`
`val` 📖	CompOp	14 math math: `RiemannianMetric.pos_def'`, `smooth_in_charts'`, `symm`, `RiemannianMetric.ext_iff`, `RiemannianMetric.pos_def`, `ext_iff`, `apply_vec_sharp`, `inner_apply`, `toQuadraticForm_apply`, `flat_apply`, `apply_sharp_sharp`, `flatEquiv_apply`, `flatL_apply`, `toBilinForm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_sharp_sharp` 📖	mathematical	—	`val` `sharpL`	—	`flatL_apply` `flatL_apply_sharpL`
`apply_vec_sharp` 📖	mathematical	—	`val` `sharpL`	—	`symm` `flatL_apply` `flatL_apply_sharpL`
`coe_flatEquiv` 📖	mathematical	—	`flatEquiv` `flatL`	—	—
`coe_sharpEquiv` 📖	mathematical	—	`sharpEquiv` `sharpL`	—	—
`cotangentMetricVal_eq_apply_sharp` 📖	mathematical	—	`cotangentMetricVal` `sharpL`	—	`cotangentMetricVal.eq_1` `apply_sharp_sharp`
`cotangentMetricVal_nondegenerate` 📖	—	`cotangentMetricVal`	—	—	`sharpL_apply_flatL` `cotangentMetricVal_eq_apply_sharp`
`cotangentMetricVal_symm` 📖	mathematical	—	`cotangentMetricVal`	—	`symm`
`cotangentToBilinForm_apply` 📖	mathematical	—	`cotangentToBilinForm` `cotangentMetricVal`	—	—
`cotangentToBilinForm_isSymm` 📖	mathematical	—	`cotangentToBilinForm`	—	`cotangentMetricVal_symm`
`cotangentToBilinForm_nondegenerate` 📖	mathematical	—	`cotangentToBilinForm`	—	`cotangentMetricVal_nondegenerate`
`cotangentToQuadraticForm_apply` 📖	mathematical	—	`cotangentToQuadraticForm` `cotangentMetricVal`	—	—
`ext` 📖	—	`val`	—	—	—
`ext_iff` 📖	mathematical	—	`val`	—	`ext`
`flatEquiv_apply` 📖	mathematical	—	`flatEquiv` `val`	—	—
`flatL_apply` 📖	mathematical	—	`flatL` `val`	—	—
`flatL_apply_sharpL` 📖	mathematical	—	`flatL` `sharpL`	—	—
`flatL_inj` 📖	mathematical	—	`flatL`	—	—
`flatL_surj` 📖	mathematical	—	`flatL`	—	—
`flat_apply` 📖	mathematical	—	`flat` `val`	—	—
`flat_inj` 📖	mathematical	—	`flat`	—	`nondegenerate`
`flat_sharp_apply` 📖	mathematical	—	`flat` `sharp`	—	`flatL_apply_sharpL`
`inner_apply` 📖	mathematical	—	`inner` `val`	—	—
`negDim_isLocallyConstant` 📖	—	—	—	—	—
`nondegenerate` 📖	—	`val`	—	—	—
`sharpL_apply_flatL` 📖	mathematical	—	`sharpL` `flatL`	—	—
`sharpL_eq_toContinuousLinearMap` 📖	mathematical	—	`sharpL` `sharpEquiv`	—	—
`sharp_flat_apply` 📖	mathematical	—	`sharp` `flat`	—	`sharpL_apply_flatL`
`smooth_in_charts'` 📖	mathematical	—	`val`	—	—
`symm` 📖	mathematical	—	`val`	—	—
`toBilinForm_apply` 📖	mathematical	—	`toBilinForm` `val`	—	—
`toBilinForm_isSymm` 📖	mathematical	—	`toBilinForm`	—	`symm`
`toBilinForm_nondegenerate` 📖	mathematical	—	`toBilinForm`	—	`nondegenerate`
`toQuadraticForm_apply` 📖	mathematical	—	`toQuadraticForm` `val`	—	—

QuadraticForm

Definitions

Name	Category	Theorems
`negDim` 📖	CompOp	2 math math: `PseudoRiemannianMetric.RiemannianMetric.riemannian_metric_negDim_zero`, `rankNeg_eq_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`neg_weight_implies_neg_value` 📖	—	—	—	—	`QuadraticMap.weightedSumSquares_basis_vector`
`posDef_no_neg_weights` 📖	—	—	—	—	`neg_weight_implies_neg_value`
`rankNeg_eq_zero` 📖	mathematical	—	`negDim`	—	`posDef_no_neg_weights`

QuadraticForm.QuadraticMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`weightedSumSquares_basis_vector` 📖	—	—	—	—	—

(root)

Definitions

Name	Category	Theorems
`PseudoRiemannianMetric` 📖	CompData	—

---

← Back to Index