OAI/Probability/GaussianRegression/Caps.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Spherical cap mass bounds along sequential routes.

  1. def OAI.NoiselessRegression.capWeight line 26
  2. lemma OAI.NoiselessRegression.measurable_capWeight line 30
  3. lemma OAI.NoiselessRegression.capWeight_le_one line 34
  4. lemma OAI.NoiselessRegression.capWeight_mass line 39
  5. lemma OAI.NoiselessRegression.ambient_mass_bound line 47
  6. lemma OAI.NoiselessRegression.continuation_cap_integral_bound line 58
  7. lemma OAI.NoiselessRegression.route_cap_bound line 72