OAI/MeasureTheory/FalconerCompletion/Graphs/ComplexOfPositiveFinite.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Graph energies and pair estimates.

  1. instance OAI.CurrentFalconer.MonotoneShell.complexOfPositive_finite line 20
  2. lemma OAI.CurrentFalconer.MonotoneShell.complexConv_memLp_two line 23
  3. lemma OAI.CurrentFalconer.MonotoneShell.complexConv_energy line 27
  4. def OAI.CurrentFalconer.MonotoneShell.complexBand1 line 32
  5. def OAI.CurrentFalconer.MonotoneShell.complexBand2 line 34
  6. lemma OAI.CurrentFalconer.MonotoneShell.complexBand1_norm line 36
  7. lemma OAI.CurrentFalconer.MonotoneShell.complexBand2_norm line 42
  8. lemma OAI.CurrentFalconer.MonotoneShell.complex_band_recombine line 49