OAI/Analysis/RotationWeights/ProjectionFields.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ContinuousCircleWeight.measurable_projection_version line 35
  2. lemma OAI.ContinuousCircleWeight.fiber_commutes_indicators line 67
  3. lemma OAI.ContinuousCircleWeight.fiber_commutes_circleJ line 74
  4. theorem OAI.ContinuousCircleWeight.extract_projection_field line 80
  5. def OAI.ContinuousCircleWeight.borelWeightedField line 102
  6. lemma OAI.ContinuousCircleWeight.borelWeightedField_coe line 104
  7. lemma OAI.ContinuousCircleWeight.decomposable_one_sub line 110
  8. lemma OAI.ContinuousCircleWeight.decomposable_invariant line 118
  9. lemma OAI.ContinuousCircleWeight.realPiField_proj_eigen line 132
  10. lemma OAI.ContinuousCircleWeight.weighted_invariant_diagonal line 144
  11. lemma OAI.ContinuousCircleWeight.borel_invariant_diagonal_strict line 159