OAI/Analysis/RieszRectifiability/Model.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.RieszRectifiability.Ambient line 10

   Also declared: ComparatorChallenges/RieszQuantitative.lean:10 (same declaration text).

2. def OAI.RieszRectifiability.AdmissibleRadius line 12

   Also declared: ComparatorChallenges/RieszQuantitative.lean:12 (same declaration text).

3. def OAI.RieszRectifiability.kernel line 15

   Also declared: ComparatorChallenges/RieszQuantitative.lean:15 (same declaration text).

4. def OAI.RieszRectifiability.truncated line 18

   Also declared: ComparatorChallenges/RieszQuantitative.lean:18 (same declaration text).

5. def OAI.RieszRectifiability.ADRegularWithConstant line 22

   Also declared: ComparatorChallenges/RieszQuantitative.lean:22 (same declaration text).

6. def OAI.RieszRectifiability.RieszL2BoundedWithConstant line 28

   Also declared: ComparatorChallenges/RieszQuantitative.lean:28 (same declaration text).

7. def OAI.RieszRectifiability.BallImageConclusion line 34

   Also declared: ComparatorChallenges/RieszQuantitative.lean:34 (same declaration text).

8. def OAI.RieszRectifiability.QuantitativeFullStatement line 42

   Source documentation

   A single mass fraction and Lipschitz bound work for all measures with fixed AD and Riesz bounds.

   Also declared: ComparatorChallenges/RieszQuantitative.lean:42 (same declaration text).

   def QuantitativeFullStatement : Prop :=
   …