OAI/Probability/SKRatio/Variational/CompactField.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SKRatio.Planted.FieldWeight line 14
  2. instance OAI.SKRatio.Planted.(instance at line 16) line 16
  3. def OAI.SKRatio.Planted.compactWeight line 18
  4. lemma OAI.SKRatio.Planted.compactWeight_lipschitz line 21
  5. lemma OAI.SKRatio.Planted.compactWeight_coe line 27
  6. def OAI.SKRatio.Planted.compactV line 29
  7. def OAI.SKRatio.Planted.compactF line 31
  8. def OAI.SKRatio.Planted.compactK line 33
  9. lemma OAI.SKRatio.Planted.compactV_nonneg line 36
  10. lemma OAI.SKRatio.Planted.compactV_le_one line 38
  11. lemma OAI.SKRatio.Planted.compactV_le line 41
  12. lemma OAI.SKRatio.Planted.compactF_nonneg line 44
  13. lemma OAI.SKRatio.Planted.compactK_nonneg line 47
  14. lemma OAI.SKRatio.Planted.compactF_bound line 51
  15. lemma OAI.SKRatio.Planted.compactK_bound line 61
  16. lemma OAI.SKRatio.Planted.continuous_compactV line 71
  17. lemma OAI.SKRatio.Planted.continuous_compact_div line 73
  18. lemma OAI.SKRatio.Planted.continuous_compactF line 89
  19. lemma OAI.SKRatio.Planted.continuous_compactK line 94
  20. lemma OAI.SKRatio.Planted.compactV_weight line 101
  21. lemma OAI.SKRatio.Planted.compactF_weight line 106
  22. lemma OAI.SKRatio.Planted.compactK_weight line 112