OAI/Analysis/IrrationalRotation/Product/ProductWeightNonconstant.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.ProductModel.logarithmicCost_coordinate_increase line 11
2. theorem OAI.Invariant233.ProductModel.measure_representative_cylinder line 29
3. theorem OAI.Invariant233.ProductModel.weight_not_ae_constant_of_ae_ne_zero line 41
4. theorem OAI.Invariant233.ProductModel.weight_not_ae_constant line 90
5. theorem OAI.Invariant233.ProductModel.weight_rotation_joint_fiber_measure_zero_of_admissible line 98
6. theorem OAI.Invariant233.ProductModel.fullPolarAlgebra_weight_diffuse_of_admissible line 104