OAI/Probability/GaussianReplacement/FiberEquality.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CurrentProjection.fiberLeft_finite line 13
  2. lemma OAI.CurrentProjection.fiberBilinear_integral_ne_top line 23
  3. lemma OAI.CurrentProjection.fiberBilinear_add_left line 40
  4. lemma OAI.CurrentProjection.fiberBilinear_add_right line 49
  5. lemma OAI.CurrentProjection.fiber_bilinear_eq line 58
  6. lemma OAI.CurrentProjection.fiber_indicator_lintegral line 89
  7. lemma OAI.CurrentProjection.fst_restrict_sphere_rectangle line 102
  8. lemma OAI.CurrentProjection.snd_restrict_sphere_rectangle line 111
  9. lemma OAI.CurrentProjection.fiber_three_rectangle_eq line 121
  10. theorem OAI.CurrentProjection.fiberTwoPointMain line 141

    Distinct definitions of this name: ComparatorChallenges/GaussianReplacement.lean:514 (same statement text; different proof or body). Qualify references as OAI.CurrentProjection.fiberTwoPointMain@path.

  11. def OAI.CurrentProjection.fiberTwoPointFromVersions line 164
  12. lemma OAI.CurrentProjection.fiberTwoPoint_version_invariance line 177
  13. lemma OAI.CurrentProjection.fiberTwoPoint_allVersions line 220