OAI/MeasureTheory/Falconer/Shells/TwoProfileMaskedShell.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The scalar shell for two actual descriptor products

The Fourier law is formed from the original two measures. Its inverse terms keep the two profile and descriptor data throughout the shell bound.

  1. theorem OAI.Falconer.exists_two_profile_masked_shell_order line 18