OAI/Probability/LatticeSurface/Dynamics/ShiftAssembly.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FeasibleShift.ShiftData.active line 29
  2. def OAI.FeasibleShift.ShiftData.H line 31
  3. def OAI.FeasibleShift.ShiftData.good line 34
  4. instance OAI.FeasibleShift.ShiftData.law_isProbabilityMeasure line 36
  5. lemma OAI.FeasibleShift.ShiftData.active_le line 39
  6. lemma OAI.FeasibleShift.ShiftData.active_degree line 41
  7. lemma OAI.FeasibleShift.ShiftData.H_pos line 46
  8. lemma OAI.FeasibleShift.ShiftData.H_le_card line 49
  9. lemma OAI.FeasibleShift.ShiftData.H_measurable line 52
  10. lemma OAI.FeasibleShift.ShiftData.good_measurable line 64
  11. lemma OAI.FeasibleShift.ShiftData.H_tail line 71
  12. lemma OAI.FeasibleShift.ShiftData.H_integrable line 82
  13. lemma OAI.FeasibleShift.ShiftData.H_moment line 87
  14. lemma OAI.FeasibleShift.ShiftData.mem_local_of_not_ground line 93
  15. lemma OAI.FeasibleShift.ShiftData.H_outside_local line 97
  16. lemma OAI.FeasibleShift.ShiftData.bad_good_bound line 120
  17. lemma OAI.FeasibleShift.ShiftData.active_or_ground line 143
  18. lemma OAI.FeasibleShift.ShiftData.shift_lipschitz line 149
  19. lemma OAI.FeasibleShift.ShiftData.extend_map line 153
  20. lemma OAI.FeasibleShift.ShiftData.map_feasible line 160
  21. lemma OAI.FeasibleShift.ShiftData.map_injective line 181
  22. lemma OAI.FeasibleShift.ShiftData.approximation_on_good line 195
  23. lemma OAI.FeasibleShift.ShiftData.derivative_on_good line 209
  24. lemma OAI.FeasibleShift.ShiftData.derivative_cost_bound line 219
  25. lemma OAI.FeasibleShift.ShiftData.derivative_integrable line 251
  26. lemma OAI.FeasibleShift.ShiftData.divergence_square_identity line 257
  27. lemma OAI.FeasibleShift.ShiftData.trace_square_le_cost_integral line 269
  28. lemma OAI.FeasibleShift.ShiftData.cost_integral_bound line 287
  29. lemma OAI.FeasibleShift.ShiftData.uniform_moment_bound line 305
  30. theorem OAI.FeasibleShift.feasible_shifts line 333