OAI/Probability/CriticalPercolation/Harmonic/FiniteHilbert.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalPercolation.HomogeneousAnalysis.finiteHilbert line 16
  2. abbrev OAI.CriticalPercolation.HomogeneousAnalysis.FH line 36
  3. instance OAI.CriticalPercolation.HomogeneousAnalysis.FH.(instance at line 38) line 38
  4. lemma OAI.CriticalPercolation.HomogeneousAnalysis.FH.ext line 39
  5. lemma OAI.CriticalPercolation.HomogeneousAnalysis.FH.zero_apply line 42
  6. lemma OAI.CriticalPercolation.HomogeneousAnalysis.FH.add_apply line 43
  7. lemma OAI.CriticalPercolation.HomogeneousAnalysis.FH.sub_apply line 44
  8. lemma OAI.CriticalPercolation.HomogeneousAnalysis.FH.smul_apply line 45
  9. lemma OAI.CriticalPercolation.HomogeneousAnalysis.FH.sum_apply line 46
  10. def OAI.CriticalPercolation.HomogeneousAnalysis.FH.support line 50
  11. lemma OAI.CriticalPercolation.HomogeneousAnalysis.FH.mem_support line 51
  12. lemma OAI.CriticalPercolation.HomogeneousAnalysis.FH.eq_zero_of_not_mem line 53
  13. def OAI.CriticalPercolation.HomogeneousAnalysis.FH.ofFunction line 56
  14. lemma OAI.CriticalPercolation.HomogeneousAnalysis.FH.ofFunction_apply line 58
  15. def OAI.CriticalPercolation.HomogeneousAnalysis.FH.delta line 61
  16. lemma OAI.CriticalPercolation.HomogeneousAnalysis.FH.delta_apply line 67
  17. lemma OAI.CriticalPercolation.HomogeneousAnalysis.FH.delta_inner line 69
  18. lemma OAI.CriticalPercolation.HomogeneousAnalysis.FH.inner_eq_sum line 74
  19. lemma OAI.CriticalPercolation.HomogeneousAnalysis.FH.norm_sq_eq_sum line 81
  20. lemma OAI.CriticalPercolation.HomogeneousAnalysis.FH.norm_coordinate_le line 86
  21. def OAI.CriticalPercolation.HomogeneousAnalysis.FH.transportLinear line 89
  22. def OAI.CriticalPercolation.HomogeneousAnalysis.FH.transport line 103
  23. lemma OAI.CriticalPercolation.HomogeneousAnalysis.FH.transport_apply line 108
  24. lemma OAI.CriticalPercolation.HomogeneousAnalysis.FH.transport_one line 110
  25. lemma OAI.CriticalPercolation.HomogeneousAnalysis.FH.transport_mul line 111
  26. lemma OAI.CriticalPercolation.HomogeneousAnalysis.FH.transport_delta line 113
  27. lemma OAI.CriticalPercolation.HomogeneousAnalysis.FH.delta_decomposition line 120
  28. lemma OAI.CriticalPercolation.HomogeneousAnalysis.FH.sum_sq_le_norm_sq line 128
  29. lemma OAI.CriticalPercolation.HomogeneousAnalysis.FH.summable line 133
  30. def OAI.CriticalPercolation.HomogeneousAnalysis.FH.mass line 135
  31. lemma OAI.CriticalPercolation.HomogeneousAnalysis.FH.mass_delta line 139
  32. lemma OAI.CriticalPercolation.HomogeneousAnalysis.FH.hasSum_mass line 143