OAI/Probability/SKRatio/Quantization/BinPullback.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKRatio.Bins.integral_finite_partition_prod line 15
  2. lemma OAI.SKRatio.Bins.fieldRadicand_pullback line 26
  3. lemma OAI.SKRatio.Bins.fieldDiagonal_partition line 39
  4. lemma OAI.SKRatio.Bins.field_diagonal_pullback line 45
  5. lemma OAI.SKRatio.Bins.field_kernel_pullback line 56
  6. theorem OAI.SKRatio.Bins.fieldForm_pullback line 71