OAI/Analysis/BrownMeasure/Weight.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.productWeightValues line 13
2. lemma OAI.FiniteFactor.productWeightValues_countable line 15
3. lemma OAI.FiniteFactor.sourceCocycle_mem_values line 16
4. lemma OAI.FiniteFactor.sourceWeight_ae_countable line 20
5. lemma OAI.FiniteFactor.SourceAngles.lt_one line 24
6. lemma OAI.FiniteFactor.unitInterval_floor_lintegral line 32
7. lemma OAI.FiniteFactor.source_coordinate_log_integral line 54
8. lemma OAI.FiniteFactor.sourceLog_nonneg line 65
9. lemma OAI.FiniteFactor.sourceLog_lintegral_prefix line 74
10. theorem OAI.FiniteFactor.sourceLog_lintegral_top line 92