OAI/Probability/LatticeSurface/Convexity/AnchoredCoupling.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.AnchoredBoundedData.compact_bodyline 14 - lemma
OAI.AnchoredBoundedData.neighbor_nonemptyline 33 - def
OAI.AnchoredBoundedData.bodyMeasureline 43 - lemma
OAI.AnchoredBoundedData.bodyMeasure_mapline 52 - lemma
OAI.AnchoredBoundedData.bodyUpdate_preservesline 61 - lemma
OAI.AnchoredBoundedData.continuous_restore_functionline 85 - theorem
OAI.AnchoredBoundedData.one_sample_bounded_data_anchoredline 88