OAI/Analysis/BoundedHochschild/WalkEndpoints.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Reversed paths, endpoint distributions and eventual endpoint mass.

  1. lemma OAI.HochschildWalk.iid_extract line 25
  2. def OAI.HochschildWalk.signed line 36
  3. lemma OAI.HochschildWalk.signed_preserving line 39
  4. lemma OAI.HochschildWalk.iid_signed_extract line 45
  5. def OAI.HochschildWalk.reversePath line 52
  6. lemma OAI.HochschildWalk.reversePath_preserving line 54
  7. lemma OAI.HochschildWalk.ofFn_reverse_inv line 63
  8. lemma OAI.HochschildWalk.reversePath_prod line 76
  9. def OAI.HochschildWalk.endpointIndex line 81
  10. lemma OAI.HochschildWalk.endpointIndex_injective line 86
  11. lemma OAI.HochschildWalk.endpoint_prefixes_preserving line 113
  12. lemma OAI.HochschildProbability.mass_transfer line 131
  13. lemma OAI.HochschildProbability.mass_transfer_two line 135
  14. lemma OAI.HochschildProbability.norm_error_mass line 142
  15. lemma OAI.HochschildProbability.ball_mass_transfer line 153
  16. lemma OAI.HochschildProbability.two_ball_mass_transfer line 170
  17. lemma OAI.HochschildWalk.finite_memLp line 207
  18. lemma OAI.HochschildWalk.finite_ball_mass line 214
  19. lemma OAI.HochschildWalk.finite_cauchy_bound line 222
  20. lemma OAI.HochschildWalk.endpoint_prefix_ball_mass line 234
  21. lemma OAI.HochschildWalk.reverse_finite_cauchy_bound line 248
  22. lemma OAI.HochschildWalk.two_endpoint_lower_bound line 283
  23. theorem OAI.HochschildWalk.endpoint_mass_eventually line 327