Model.lean`

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.CenteredDiskEndpoint.Plane line 12
Source documentation
The Euclidean plane, not the product space with its max norm.
Also declared: ComparatorChallenges/DiskMaximal.lean:12 (same declaration text).
```
abbrev Plane := EuclideanSpace ℝ (Fin 2)
```
def OAI.CenteredDiskEndpoint.absoluteDiskAverage line 15
Source documentation
Absolute disk average, retaining possible infinite values.
Also declared: ComparatorChallenges/DiskMaximal.lean:15 (same declaration text).
```
def absoluteDiskAverage (f : Plane → ℝ) (x : Plane) (r : ℝ) : ℝ≥0∞ :=
…
```
Mentions: OAI.CenteredDiskEndpoint.Plane
def OAI.CenteredDiskEndpoint.maximal line 20
Source documentation
The actual centered disk maximal function, over every positive real radius.
Also declared: ComparatorChallenges/DiskMaximal.lean:20 (same declaration text).
```
def maximal (f : Plane → ℝ) (x : Plane) : ℝ≥0∞ :=
…
```
Mentions: OAI.CenteredDiskEndpoint.Plane
def OAI.CenteredDiskEndpoint.maximalReal line 24
Source documentation
Real representative; the endpoint also asserts that maximal f is finite a.e.
Also declared: ComparatorChallenges/DiskMaximal.lean:24 (same declaration text).
```
def maximalReal (f : Plane → ℝ) (x : Plane) : ℝ := (maximal f x).toReal
```
Mentions: OAI.CenteredDiskEndpoint.Plane, OAI.CenteredDiskEndpoint.maximal
def OAI.CenteredDiskEndpoint.testPartial line 27
Source documentation
The i-th coordinate derivative of a smooth test function.
Also declared: ComparatorChallenges/DiskMaximal.lean:27 (same declaration text).
```
def testPartial (φ : Plane → ℝ) (i : Fin 2) (x : Plane) : ℝ :=
…
```
Mentions: OAI.CenteredDiskEndpoint.Plane
def OAI.CenteredDiskEndpoint.HasWeakGradient line 31
Source documentation
Distributional first derivatives represented by a vector-valued function.
Also declared: ComparatorChallenges/DiskMaximal.lean:31 (same declaration text).
```
def HasWeakGradient (f : Plane → ℝ) (g : Plane → Plane) : Prop :=
…
```
Mentions: OAI.CenteredDiskEndpoint.Plane
def OAI.CenteredDiskEndpoint.InW11Loc line 36
Source documentation
Local W^(1,1), expressed using the same distributional gradient convention.
Also declared: ComparatorChallenges/DiskMaximal.lean:36 (same declaration text).
```
def InW11Loc (f : Plane → ℝ) : Prop :=
…
```
Mentions: OAI.CenteredDiskEndpoint.Plane
def OAI.CenteredDiskEndpoint.gradientNorm line 41
Source documentation
The gradient L1 norm in Euclidean norm.
Also declared: ComparatorChallenges/DiskMaximal.lean:41 (same declaration text).
```
def gradientNorm (g : Plane → Plane) : ℝ := ∫ x, ‖g x‖
```
Mentions: OAI.CenteredDiskEndpoint.Plane
def OAI.CenteredDiskEndpoint.EndpointStatement line 46
Source documentation
Exact endpoint, including finiteness before passing to the real representative. Quantifying the input gradient makes the norm bound independent of a choice of representative of its weak derivatives.
Also declared: ComparatorChallenges/DiskMaximal.lean:46 (same declaration text).
```
def EndpointStatement : Prop :=
…
```
def OAI.CenteredDiskEndpoint.diskAverage line 56
def OAI.CenteredDiskEndpoint.InW11 line 60
Source documentation
Real inhomogeneous W^(1,1) on the whole plane.
```
def InW11 (f : Plane → ℝ) : Prop :=
…
```
Mentions: OAI.CenteredDiskEndpoint.Plane