OAI/Probability/SKRatio/Variational/FieldRadical.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKRatio.Bins.fieldRadicand line 14
  2. lemma OAI.SKRatio.Bins.fieldRadicand_nonneg line 19
  3. lemma OAI.SKRatio.Bins.memLp_sum_v_field line 25
  4. lemma OAI.SKRatio.Bins.field_energy_integrable line 32
  5. lemma OAI.SKRatio.Bins.fieldRadicand_expansion line 40
  6. lemma OAI.SKRatio.Bins.fieldRadicand_le line 52
  7. lemma OAI.SKRatio.Bins.measurable_fieldRadicand line 63
  8. lemma OAI.SKRatio.Bins.abs_square_sub_le line 78
  9. lemma OAI.SKRatio.Bins.fieldRadicand_error line 84
  10. lemma OAI.SKRatio.Bins.sqrt_fieldRadicand_error line 123