OAI/Probability/GaussianRegression/ReplicaMoments.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Inverse Gram moments and almost-everywhere replica independence.

  1. def OAI.NoiselessRegression.replicaWeight line 24
  2. lemma OAI.NoiselessRegression.measurable_replicaWeight line 27
  3. lemma OAI.NoiselessRegression.replicaWeight_snoc line 34
  4. def OAI.NoiselessRegression.replicaConstant line 44
  5. lemma OAI.NoiselessRegression.affine_inverse_moment_le_replicaConstant line 48
  6. theorem OAI.NoiselessRegression.replica_integral_bound line 60
  7. lemma OAI.NoiselessRegression.ae_pi_snoc line 97
  8. lemma OAI.NoiselessRegression.measurableSet_gramSchmidt_ne_zero line 122
  9. theorem OAI.NoiselessRegression.ae_gramSchmidt_ne_zero line 131
  10. theorem OAI.NoiselessRegression.ae_replica_linearIndependent line 167
  11. lemma OAI.NoiselessRegression.sqrt_det_gram line 179
  12. lemma OAI.NoiselessRegression.replicaWeight_eq_det line 185
  13. theorem OAI.NoiselessRegression.gram_integral_bound line 191