OAI/NumberTheory/Ostmann/Supply/TensorModeEnergy.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Supply.TensorModes.norm_sq_complex line 11
2. theorem OAI.Ostmann.Supply.TensorModes.exactMode_inner_eq_zero line 17
3. theorem OAI.Ostmann.Supply.TensorModes.norm_lowModes_sq line 29
4. def OAI.Ostmann.Supply.TensorModes.augmentedPoint line 48
5. def OAI.Ostmann.Supply.TensorModes.empiricalTensor line 51
6. theorem OAI.Ostmann.Supply.TensorModes.exactMode_pureTensor_inner line 55
7. theorem OAI.Ostmann.Supply.TensorModes.norm_exactMode_empirical_eq_gram line 82
8. def OAI.Ostmann.Supply.TensorModes.residueCenteredFamily line 94
9. def OAI.Ostmann.Supply.TensorModes.residueCenteredVector line 98
10. theorem OAI.Ostmann.Supply.TensorModes.norm_residue_exactMode_sq line 102
11. theorem OAI.Ostmann.Supply.TensorModes.norm_residue_lowModes_sq line 127