OAI/Probability/FreeIsing/Brownian/SpatialPrimitive.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.BrownianArrayFiltration.spatialSquareDensity line 14
  2. theorem OAI.Problem367.BrownianArrayFiltration.nonnegativeCompensator_eq_integral_of_continuous line 18
  3. theorem OAI.Problem367.BrownianArrayFiltration.summable_integral_sq_of_integer line 25
  4. theorem OAI.Problem367.BrownianArrayFiltration.integral_spatial_sq_tsum line 37
  5. theorem OAI.Problem367.BrownianArrayFiltration.ae_spatialCompensator_eq_primitive line 57
  6. theorem OAI.Problem367.BrownianArrayFiltration.spatialSquareDensity_isStronglyProgressive line 81
  7. theorem OAI.Problem367.BrownianArrayFiltration.compensatedSquare_spatial_primitive line 90
  8. theorem OAI.Problem367.BrownianArrayFiltration.integrable_spatialSquareDensity_interval line 107