OAI/Analysis/RotationWeights/ProjectionIdentity.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.CircleSampling.ModelProjectionField line 67
2. def OAI.CircleSampling.rationalCap line 77
3. lemma OAI.CircleSampling.rationalCap_ge_one line 78
4. lemma OAI.CircleSampling.stageGraph_ae line 82
5. lemma OAI.CircleSampling.rationalGraph_pair line 101
6. lemma OAI.CircleSampling.rational_pair_graph line 126
7. lemma OAI.CircleSampling.rational_pair line 132
8. lemma OAI.ContinuousCircleWeight.stronglyMeasurable_lp_field line 147
9. lemma OAI.ContinuousCircleWeight.stronglyMeasurable_field_simple line 165
10. lemma OAI.ContinuousCircleWeight.stronglyMeasurable_field_apply line 176
11. lemma OAI.ContinuousCircleWeight.measurable_cappedDiagonal line 184
12. lemma OAI.ContinuousCircleWeight.measurableSet_cappedPairRelation line 203