OAI/Probability/GaussianReplacement/MixedReplica.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CurrentProjection.AmbientGrowth.affine_span_null line 16
  2. theorem OAI.CurrentProjection.AmbientGrowth.ae_gramSchmidt_ne_zero line 43
  3. theorem OAI.CurrentProjection.AmbientGrowth.ae_replica_linearIndependent line 71
  4. def OAI.CurrentProjection.mixedReplicaWeight line 88
  5. lemma OAI.CurrentProjection.measurable_mixedReplicaWeight line 91
  6. lemma OAI.CurrentProjection.mixedReplicaWeight_snoc line 99
  7. theorem OAI.CurrentProjection.AmbientGrowth.mixed_inverse_uniform line 109
  8. theorem OAI.CurrentProjection.AmbientGrowth.mixed_replica_integral line 121
  9. lemma OAI.CurrentProjection.gaussian_fixed_kernel_bound line 159
  10. def OAI.CurrentProjection.rowKernel line 183
  11. lemma OAI.CurrentProjection.measurable_rowKernel line 186
  12. lemma OAI.CurrentProjection.measurable_rowKernel_right line 191
  13. lemma OAI.CurrentProjection.measurable_rowKernel_left line 196
  14. lemma OAI.CurrentProjection.gaussian_fresh_kernel_bound line 201
  15. lemma OAI.CurrentProjection.rowKernel_append line 218
  16. lemma OAI.CurrentProjection.mixedReplicaWeight_factor line 224
  17. theorem OAI.CurrentProjection.AmbientGrowth.mixed_kernel_moment line 235