OAI/MeasureTheory/FalconerCompletion/Shells/ContinuousCoefficientMeasurableSquare.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Dyadic shells and prefix decompositions.

  1. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.continuous_coefficient_measurable_squareND line 18
  2. theorem OAI.GraphLiteralSupport.Attempt4PrefixShell.full_HF_shell_mixtureND line 43
  3. def OAI.GraphLiteralSupport.Attempt4PrefixShell.shellRadialMultiplierND line 112
  4. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.positive_shell_ratioND line 115
  5. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.shellRadialMultiplierND_bound line 124
  6. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.shellRadialMultiplierND_measurable line 138
  7. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.positive_inverse_coefficient_splitND line 143
  8. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.dyadic_inverse_coefficient_splitND line 151
  9. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.sum_range_flatMapND line 181
  10. def OAI.GraphLiteralSupport.Attempt4PrefixShell.inverseTermListND line 196
  11. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.sum_inverseTermListND line 199
  12. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.mem_inverseTermListND line 205
  13. def OAI.GraphLiteralSupport.Attempt4PrefixShell.spatialEndpointTransformND line 216
  14. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.spatialEndpointTransformND_measurable line 222
  15. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.spatialEndpointTransformND_bound line 235
  16. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.all_mask_shell_factorizationND line 247
  17. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.inverseTermListND_paid_cost line 276