OAI/Probability/SKBarriers/Scalar/ScalarLevelRepresentation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SK.Analytic.scalarLevelField line 14
2. theorem OAI.SK.Analytic.scalarSpinField_succ line 20
3. theorem OAI.SK.Analytic.gaussianStep_scalarSpinField line 29
4. theorem OAI.SK.Analytic.hierarchyLevel_scalar_representation line 39
5. theorem OAI.SK.Analytic.scalarLevelField_last line 57
6. theorem OAI.SK.Analytic.scalar_comp_directional line 63
7. theorem OAI.SK.Analytic.hierarchyLevel_scalar_direction_bounds line 94