OAI/Probability/BinarySweep/TensorBounds/EmpiricalTensor.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinaryCoordinateSweeps.Density.tensorAmplitude line 16
  2. def OAI.BinaryCoordinateSweeps.Density.tensorProductVector line 18
  3. def OAI.BinaryCoordinateSweeps.Density.phasedVector line 20
  4. lemma OAI.BinaryCoordinateSweeps.Density.tensorProductVector_phased line 24
  5. lemma OAI.BinaryCoordinateSweeps.Density.tensorAmplitude_counts line 30
  6. lemma OAI.BinaryCoordinateSweeps.Density.tensorAmplitude_sq line 34
  7. def OAI.BinaryCoordinateSweeps.Density.phaseAverage line 41
  8. lemma OAI.BinaryCoordinateSweeps.Density.phaseAverage_psd line 45
  9. lemma OAI.BinaryCoordinateSweeps.Density.phaseAverage_apply line 49
  10. lemma OAI.BinaryCoordinateSweeps.Density.phaseAverage_kernel line 79
  11. lemma OAI.BinaryCoordinateSweeps.Density.phasedVector_norm line 88
  12. lemma OAI.BinaryCoordinateSweeps.Density.phasedVector_trace line 100
  13. def OAI.BinaryCoordinateSweeps.Density.empirical line 116
  14. lemma OAI.BinaryCoordinateSweeps.Density.empirical_nonneg line 118
  15. lemma OAI.BinaryCoordinateSweeps.Density.empirical_sum line 121
  16. lemma OAI.BinaryCoordinateSweeps.Density.type_mass_inv line 125
  17. theorem OAI.BinaryCoordinateSweeps.Density.finite_postselection line 134