OAI/Probability/GaussianInformation/Kernel/SimplexApproximation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.KernelPotential.NoisyDrift.continuous_ae_approx line 18
  2. def OAI.KernelPotential.NoisyDrift.Simplex.clip line 41
  3. def OAI.KernelPotential.NoisyDrift.Simplex.total line 42
  4. def OAI.KernelPotential.NoisyDrift.Simplex.normalize line 43
  5. lemma OAI.KernelPotential.NoisyDrift.Simplex.clip_lower line 44
  6. lemma OAI.KernelPotential.NoisyDrift.Simplex.clip_upper line 45
  7. lemma OAI.KernelPotential.NoisyDrift.Simplex.total_pos line 46
  8. lemma OAI.KernelPotential.NoisyDrift.Simplex.total_upper line 50
  9. lemma OAI.KernelPotential.NoisyDrift.Simplex.normalize_lower line 52
  10. lemma OAI.KernelPotential.NoisyDrift.Simplex.normalize_sum line 56
  11. lemma OAI.KernelPotential.NoisyDrift.Simplex.continuous_normalize line 61
  12. lemma OAI.KernelPotential.NoisyDrift.Simplex.normalize_eq line 65
  13. lemma OAI.KernelPotential.NoisyDrift.PositiveRule.lower_le_one line 77
  14. lemma OAI.KernelPotential.NoisyDrift.PositiveRule.exists_continuous_approx line 79