OAI/Probability/LatticeSurface/Dynamics/IntervalResampling.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.IntervalResampling.affine_measureline 13 - lemma
OAI.IntervalResampling.affine_integralline 34 - def
OAI.IntervalResampling.regionline 45 - lemma
OAI.IntervalResampling.measurable_regionline 47 - lemma
OAI.IntervalResampling.slice_integralline 52 - lemma
OAI.IntervalResampling.invariantline 70