OAI/Probability/SKRatio/Variational/FieldFunctional.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKRatio.Bins.fieldDiagonal line 16
  2. def OAI.SKRatio.Bins.fieldForm line 19
  3. lemma OAI.SKRatio.Bins.fieldForm_id line 28
  4. lemma OAI.SKRatio.Bins.measurable_fieldDiagonal line 31
  5. lemma OAI.SKRatio.Bins.fieldDiagonal_integrable line 38
  6. lemma OAI.SKRatio.Bins.abs_fieldDiagonal_le line 44
  7. lemma OAI.SKRatio.Bins.fieldDiagonal_error line 49
  8. lemma OAI.SKRatio.Bins.fieldKernel_integrable line 57
  9. lemma OAI.SKRatio.Bins.fieldKernel_error line 71
  10. lemma OAI.SKRatio.Bins.field_pair_difference line 93
  11. lemma OAI.SKRatio.Bins.field_pair_v_abs line 102
  12. lemma OAI.SKRatio.Bins.mean_abs_le_one line 108
  13. lemma OAI.SKRatio.Bins.memLp_Hv line 112
  14. lemma OAI.SKRatio.Bins.Hv_error line 117
  15. lemma OAI.SKRatio.Bins.field_radical_pair_error line 136
  16. theorem OAI.SKRatio.Bins.fieldForm_error line 152