OAI/Probability/FreeIsing/Brownian/UniformGrid.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.BrownianGrid.uniformGrid line 11
  2. lemma OAI.Problem367.BrownianGrid.uniformGrid_zero line 13
  3. lemma OAI.Problem367.BrownianGrid.uniformGrid_mono line 16
  4. lemma OAI.Problem367.BrownianGrid.uniformGrid_end line 21
  5. lemma OAI.Problem367.BrownianGrid.uniformGrid_refine line 27
  6. lemma OAI.Problem367.BrownianGrid.uniformGrid_le_horizon line 34
  7. lemma OAI.Problem367.BrownianGrid.uniformGrid_floor_le line 38
  8. lemma OAI.Problem367.BrownianGrid.uniformGrid_floor_sub_le line 43
  9. def OAI.Problem367.BrownianGrid.uniformSum line 61
  10. theorem OAI.Problem367.BrownianGrid.preBrownian_uniform_difference_isometry line 64
  11. theorem OAI.Problem367.BrownianGrid.preBrownian_uniform_difference_bound line 89
  12. theorem OAI.Problem367.BrownianGrid.integralSum_memLp line 113
  13. theorem OAI.Problem367.BrownianGrid.uniformSum_memLp line 125
  14. theorem OAI.Problem367.BrownianGrid.preBrownian_uniform_difference_bound_of_modulus line 135
  15. lemma OAI.Problem367.BrownianGrid.integral_sq_sub_le_two line 154
  16. theorem OAI.Problem367.BrownianGrid.preBrownian_uniform_pair_bound line 170