OAI/Probability/FreeIsing/Brownian/FiltrationUniformIntegral.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.BrownianFiltrationGrid.preBrownian_difference_isometry line 13
  2. theorem OAI.Problem367.BrownianFiltrationGrid.preBrownian_uniform_difference_isometry line 35
  3. theorem OAI.Problem367.BrownianFiltrationGrid.preBrownian_uniform_difference_bound line 62
  4. theorem OAI.Problem367.BrownianFiltrationGrid.integralSum_memLp line 88
  5. theorem OAI.Problem367.BrownianFiltrationGrid.uniformSum_memLp line 102
  6. theorem OAI.Problem367.BrownianFiltrationGrid.preBrownian_uniform_difference_bound_of_modulus line 114
  7. theorem OAI.Problem367.BrownianFiltrationGrid.preBrownian_uniform_pair_bound line 135
  8. def OAI.Problem367.BrownianFiltrationGrid.uniformSumLp line 156
  9. lemma OAI.Problem367.BrownianFiltrationGrid.coe_uniformSumLp line 166
  10. theorem OAI.Problem367.BrownianFiltrationGrid.cauchySeq_uniformSumLp line 177
  11. theorem OAI.Problem367.BrownianFiltrationGrid.exists_uniformSumLp_limit line 222
  12. theorem OAI.Problem367.BrownianFiltrationGrid.exists_uniform_integral line 236
  13. theorem OAI.Problem367.BrownianFiltrationGrid.exists_uniform_integral_of_bounded_continuous line 264
  14. theorem OAI.Problem367.BrownianFiltrationGrid.uniformSumLp_norm_sq line 288
  15. theorem OAI.Problem367.BrownianFiltrationGrid.uniformSumLp_limit_isometry line 311