OAI/MeasureTheory/FalconerCompletion/Shells/ComplexShellEnergyEq.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Dyadic shells and prefix decompositions.

  1. lemma OAI.CurrentFalconer.MonotoneShell.complexShellEnergy_eq line 22
  2. lemma OAI.CurrentFalconer.MonotoneShell.complexShellEnergy_nonneg line 33
  3. lemma OAI.CurrentFalconer.MonotoneShell.complexMultiplier_energy_le line 35
  4. def OAI.CurrentFalconer.MonotoneShell.lowKernel line 61
  5. lemma OAI.CurrentFalconer.MonotoneShell.lowKernel_continuous line 63
  6. lemma OAI.CurrentFalconer.MonotoneShell.lowKernel_integrable line 67
  7. lemma OAI.CurrentFalconer.MonotoneShell.lowKernel_uniform line 73
  8. lemma OAI.CurrentFalconer.MonotoneShell.lowKernel_inverse line 79
  9. lemma OAI.CurrentFalconer.MonotoneShell.shellKernel_eq_sub_low line 88
  10. def OAI.CurrentFalconer.MonotoneShell.lowTerm line 109
  11. lemma OAI.CurrentFalconer.MonotoneShell.lowTerm_norm_le line 113
  12. lemma OAI.CurrentFalconer.MonotoneShell.lowTerm_add line 120
  13. lemma OAI.CurrentFalconer.MonotoneShell.lowTerm_sub_of_le line 134
  14. lemma OAI.CurrentFalconer.MonotoneShell.lowTerm_zero line 139