OAI/Probability/FirstPassage/SpatialChunkWitness.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.PlanarFPP.negative_midpoint_spatial_witnessline 9 - theorem
OAI.PlanarFPP.full_chunk_transverse_witnessline 30 - lemma
OAI.PlanarFPP.negative_longitudinal_chunk_not_cheapline 52