OAI/MeasureTheory/FalconerCompletion/Shells/AngularCorrelation.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Dyadic shells and prefix decompositions.

  1. def OAI.GraphLiteralSupport.Attempt4PrefixShell.sourceAngularCorrelationND line 19
  2. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.sourceAngularCorrelationND_measurable line 22
  3. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.sourceAngularCorrelationND_bound line 29
  4. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.sourceAngularCorrelationND_weighted_integrable line 40
  5. theorem OAI.GraphLiteralSupport.Attempt4PrefixShell.sourceAngularHFND_shell_bound line 56
  6. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.weighted_shell_normalizationND line 92
  7. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.sourceAngularCorrelationND_parameter_measurable line 117
  8. theorem OAI.GraphLiteralSupport.Attempt4PrefixShell.continuous_HF_shell_boundND line 127
  9. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.shell_square_multiplierND line 166
  10. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.shell_add_squareND line 184
  11. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.shell_lengthND line 201
  12. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.shell_error_squareND line 209
  13. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.shell_leading_squareND line 219
  14. theorem OAI.GraphLiteralSupport.Attempt4PrefixShell.normalized_list_shellND line 226
  15. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.integrable_add_squareND line 263
  16. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.list_shell_integrabilityND line 274
  17. theorem OAI.GraphLiteralSupport.Attempt4PrefixShell.normalized_list_shell_remainderND line 290