OAI/Probability/SKBarriers/Hierarchy/WeightedAugment.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SK.Analytic.weightedVariance_append line 14
  2. theorem OAI.SK.Analytic.weightedCross_append line 18
  3. theorem OAI.SK.Analytic.weightedVariance_zeroWeight line 22
  4. theorem OAI.SK.Analytic.weightedCross_zeroWeight line 25
  5. theorem OAI.SK.Analytic.weightedCrossPenalty_append line 28
  6. theorem OAI.SK.Analytic.weightedCrossPenalty_zeroWeight line 33
  7. theorem OAI.SK.Analytic.weightedVariance_full line 41
  8. theorem OAI.SK.Analytic.weightedCrossPenalty_full line 44
  9. theorem OAI.SK.Analytic.weighted_mass_iff line 48
  10. theorem OAI.SK.Analytic.weighted_sorted_iff line 54
  11. theorem OAI.SK.Analytic.weightedFull_spin_early_le line 58