OAI/Probability/GaussianRegression/Blocks.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Localization, finite selection, and block mass propagation.

  1. def OAI.NoiselessRegression.PolynomialMass line 25
  2. def OAI.NoiselessRegression.localNormalize line 28
  3. lemma OAI.NoiselessRegression.localNormalize_univ line 32
  4. lemma OAI.NoiselessRegression.localNormalize_finite line 42
  5. lemma OAI.NoiselessRegression.localNormalize_support line 48
  6. lemma OAI.NoiselessRegression.localNormalize_local line 64
  7. lemma OAI.NoiselessRegression.replicaConstant_le line 90
  8. lemma OAI.NoiselessRegression.projectionLaw_uniform_set_bound line 114
  9. lemma OAI.NoiselessRegression.finite_rpow_holder line 137
  10. lemma OAI.NoiselessRegression.normalized_routing_bound line 149
  11. lemma OAI.NoiselessRegression.localNormalize_reconstruct line 209
  12. lemma OAI.NoiselessRegression.projectionLaw_smul line 222
  13. lemma OAI.NoiselessRegression.projectionLaw_affine line 227
  14. lemma OAI.NoiselessRegression.localized_routing_bound line 237
  15. lemma OAI.NoiselessRegression.projectionLaw_withDensity_apply line 267
  16. def OAI.NoiselessRegression.blockValue line 286
  17. lemma OAI.NoiselessRegression.measurable_finite_select line 290
  18. lemma OAI.NoiselessRegression.measurable_blockValue line 300
  19. lemma OAI.NoiselessRegression.blockValue_le_one line 308
  20. lemma OAI.NoiselessRegression.blockValue_mass_identity line 318
  21. lemma OAI.NoiselessRegression.blockValue_mass_bound line 358