OAI/MeasureTheory/Falconer/Estimates/NoncomparableOriginalPointwise.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Pointwise noncomparable decay before nonnegative integration

  1. theorem OAI.Falconer.jetStateOriginalKernel_swap line 12
  2. theorem OAI.Falconer.exists_jetState_noncomparable_original_pointwise line 25
  3. theorem OAI.Falconer.lintegral_norm_restrict_le_of_bound line 73