OAI/Probability/LatticePassage/CalibrationMean.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CompanionFPP.DirectionalCalibration.integrable line 10
  2. lemma OAI.CompanionFPP.DirectionalCalibration.mean_translation line 13
  3. def OAI.CompanionFPP.DirectionalCalibration.meanHom line 27
  4. lemma OAI.CompanionFPP.DirectionalCalibration.meanHom_direction line 46
  5. lemma OAI.CompanionFPP.DirectionalCalibration.scaleVertex_eq_nsmul line 48
  6. lemma OAI.CompanionFPP.DirectionalCalibration.meanHom_scale line 51
  7. lemma OAI.CompanionFPP.DirectionalCalibration.meanHom_le_mean line 54
  8. theorem OAI.CompanionFPP.DirectionalCalibration.meanHom_le_directionalMeanConstant line 60
  9. lemma OAI.CompanionFPP.DirectionalCalibration.meanHom_coordinates line 69
  10. def OAI.CompanionFPP.DirectionalCalibration.meanLinear line 75
  11. lemma OAI.CompanionFPP.DirectionalCalibration.meanLinear_embed line 80
  12. lemma OAI.CompanionFPP.DirectionalCalibration.mean_value line 83
  13. theorem OAI.CompanionFPP.DirectionalCalibration.meanHom_eq_of_flat_neighborhood line 89
  14. theorem OAI.CompanionFPP.exists_calibration_prescribed_mean line 111