OAI/Probability/CriticalPercolation/Harmonic/GraphHarmonicLinear.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.harmonic_constant_of_attained_max line 21
  2. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.harmonic_constant_of_finite_range line 35
  3. def OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.translateFunction line 42
  4. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.translate_harmonic line 43
  5. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.translate_polynomial_growth line 50
  6. def OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.harmonicTranslation line 66
  7. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.harmonicTranslation_apply line 76
  8. def OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.harmonicRepresentation line 79
  9. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.harmonicTranslation_eq_of_agree line 85
  10. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.finite_stabilizer_harmonic_image line 97
  11. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.finite_range_of_finite_harmonic_image line 115
  12. lemma OAI.CriticalPercolation.HomogeneousAnalysis.Geometry.infinite_harmonic_linear_image line 127