OAI/Probability/GaussianReplacement/ActualRow.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentProjection.actualExperiment line 13

    Also declared: ComparatorChallenges/GaussianReplacement.lean:105 (same declaration text).

  2. instance OAI.CurrentProjection.actualExperiment_isProbabilityMeasure line 17

    Also declared: ComparatorChallenges/GaussianReplacement.lean:109 (same declaration text).

  3. def OAI.CurrentProjection.actualRowsSignal line 22
  4. def OAI.CurrentProjection.actualObservation line 26

    Also declared: ComparatorChallenges/GaussianReplacement.lean:114 (same declaration text).

  5. lemma OAI.CurrentProjection.measurable_actualRowsSignal line 31
  6. lemma OAI.CurrentProjection.measurable_actualObservation line 36
  7. instance OAI.CurrentProjection.actualObservation_isProbabilityMeasure line 42

    Also declared: ComparatorChallenges/GaussianReplacement.lean:119 (same declaration text).

  8. lemma OAI.CurrentProjection.map_actualRowsSignal line 47
  9. lemma OAI.CurrentProjection.actualObservation_ac line 85
  10. def OAI.CurrentProjection.selectedCube line 126

    Also declared: ComparatorChallenges/GaussianReplacement.lean:124 (same declaration text).

  11. def OAI.CurrentProjection.selectedExact line 129

    Also declared: ComparatorChallenges/GaussianReplacement.lean:127 (same declaration text).

  12. lemma OAI.CurrentProjection.measurable_countable_selection line 132
  13. lemma OAI.CurrentProjection.measurable_selectedCube line 141
  14. lemma OAI.CurrentProjection.measurable_selectedExact line 147
  15. lemma OAI.CurrentProjection.exactDensity_ne_top line 153
  16. lemma OAI.CurrentProjection.actual_cube_limit line 159
  17. lemma OAI.CurrentProjection.actual_conditional_label_ac line 180
  18. def OAI.CurrentProjection.momentBound line 196

    Also declared: ComparatorChallenges/GaussianReplacement.lean:130 (same declaration text).

  19. lemma OAI.CurrentProjection.momentBound_nonneg line 199
  20. lemma OAI.CurrentProjection.cubeAverage_inner_finite line 204
  21. lemma OAI.CurrentProjection.actual_smoothed_log_bound line 216
  22. lemma OAI.CurrentProjection.log_lintegral_bound_of_ae_tendsto line 243
  23. def OAI.CurrentProjection.logPositive line 262

    Also declared: ComparatorChallenges/GaussianReplacement.lean:133 (same declaration text).

  24. def OAI.CurrentProjection.logNegative line 264

    Also declared: ComparatorChallenges/GaussianReplacement.lean:135 (same declaration text).

  25. def OAI.CurrentProjection.extendedLogExpectation line 267

    Also declared: ComparatorChallenges/GaussianReplacement.lean:137 (same declaration text).

  26. lemma OAI.CurrentProjection.logPositive_le_log_one_add line 272
  27. lemma OAI.CurrentProjection.log_bound_consequences line 278
  28. def OAI.CurrentProjection.PositiveMessage line 308

    Also declared: ComparatorChallenges/GaussianReplacement.lean:142 (same declaration text).

  29. def OAI.CurrentProjection.completeFamily line 310

    Also declared: ComparatorChallenges/GaussianReplacement.lean:144 (same declaration text).

  30. instance OAI.CurrentProjection.completeFamily_finite line 314
  31. lemma OAI.CurrentProjection.completeFamily_pos line 322
  32. lemma OAI.CurrentProjection.completeFamily_growth line 330
  33. structure OAI.CurrentProjection.ActualRowConclusion line 341

    Also declared: ComparatorChallenges/GaussianReplacement.lean:148 (same declaration text).

  34. theorem OAI.CurrentProjection.actualRowMain line 375

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

  35. theorem OAI.CurrentProjection.actualRowRefinement line 433

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