Model.lean`

40 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.SignedDisk.CenteredDiskEndpoint.Plane line 15
Source documentation
The Euclidean plane, not the product space with its max norm.
Also declared: ComparatorChallenges/SignedFiniteBand.lean:15 (same declaration text).
```
abbrev Plane := EuclideanSpace ℝ (Fin 2)
```
def OAI.SignedDisk.CenteredDiskEndpoint.diskAverage line 17
Also declared: ComparatorChallenges/SignedFiniteBand.lean:17 (same declaration text).
def OAI.SignedDisk.CenteredDiskEndpoint.absoluteDiskAverage line 21
Source documentation
Absolute disk average, retaining possible infinite values.
```
def absoluteDiskAverage (f : Plane → ℝ) (x : Plane) (r : ℝ) : ℝ≥0∞ :=
…
```
Mentions: OAI.SignedDisk.CenteredDiskEndpoint.Plane
def OAI.SignedDisk.CenteredDiskEndpoint.maximal line 26
Source documentation
The actual centered disk maximal function, over every positive real radius.
```
def maximal (f : Plane → ℝ) (x : Plane) : ℝ≥0∞ :=
…
```
Mentions: OAI.SignedDisk.CenteredDiskEndpoint.Plane
def OAI.SignedDisk.CenteredDiskEndpoint.maximalReal line 30
Source documentation
Real representative; the endpoint also asserts that maximal f is finite a.e.
```
def maximalReal (f : Plane → ℝ) (x : Plane) : ℝ := (maximal f x).toReal
```
Mentions: OAI.SignedDisk.CenteredDiskEndpoint.Plane, OAI.SignedDisk.CenteredDiskEndpoint.maximal
def OAI.SignedDisk.CenteredDiskEndpoint.testPartial line 33
Source documentation
The i-th coordinate derivative of a smooth test function.
Also declared: ComparatorChallenges/SignedFiniteBand.lean:21 (same declaration text).
```
def testPartial (φ : Plane → ℝ) (i : Fin 2) (x : Plane) : ℝ :=
…
```
Mentions: OAI.SignedDisk.CenteredDiskEndpoint.Plane
def OAI.SignedDisk.CenteredDiskEndpoint.HasWeakGradient line 37
Source documentation
Distributional first derivatives represented by a vector-valued function.
Also declared: ComparatorChallenges/SignedFiniteBand.lean:25 (same declaration text).
```
def HasWeakGradient (f : Plane → ℝ) (g : Plane → Plane) : Prop :=
…
```
Mentions: OAI.SignedDisk.CenteredDiskEndpoint.Plane
def OAI.SignedDisk.CenteredDiskEndpoint.InW11 line 42
Source documentation
Real inhomogeneous W^(1,1) on the whole plane.
```
def InW11 (f : Plane → ℝ) : Prop :=
…
```
Mentions: OAI.SignedDisk.CenteredDiskEndpoint.Plane
def OAI.SignedDisk.CenteredDiskEndpoint.InW11Loc line 46
Source documentation
Local W^(1,1), expressed using the same distributional gradient convention.
```
def InW11Loc (f : Plane → ℝ) : Prop :=
…
```
Mentions: OAI.SignedDisk.CenteredDiskEndpoint.Plane
def OAI.SignedDisk.CenteredDiskEndpoint.gradientNorm line 51
Source documentation
The gradient L1 norm in Euclidean norm.
Also declared: ComparatorChallenges/SignedFiniteBand.lean:30 (same declaration text).
```
def gradientNorm (g : Plane → Plane) : ℝ := ∫ x, ‖g x‖
```
Mentions: OAI.SignedDisk.CenteredDiskEndpoint.Plane
def OAI.SignedDisk.CenteredDiskEndpoint.signedBand line 54
Source documentation
Signed envelope over all real radii in the closed band, including its endpoints.
Also declared: ComparatorChallenges/SignedFiniteBand.lean:33 (same declaration text).
```
def signedBand (f : Plane → ℝ) (a b : ℝ) (x : Plane) : ℝ :=
…
```
Mentions: OAI.SignedDisk.CenteredDiskEndpoint.Plane
def OAI.SignedDisk.CenteredDiskEndpoint.SignedFiniteBandStatement line 57
Also declared: ComparatorChallenges/SignedFiniteBand.lean:36 (same declaration text).
def OAI.SignedDisk.CenteredDiskEndpoint.EndpointStatement line 69
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.
```
def EndpointStatement : Prop :=
…
```
theorem OAI.SignedDisk.CenteredDiskEndpoint.volume_disk line 80
Source documentation
The normalization is precisely planar Lebesgue disk area.
```
theorem volume_disk (x : Plane) {r : ℝ} (hr : 0 ≤ r) :
    volume (Metric.ball x r) = ENNReal.ofReal (Real.pi * r ^ 2) := by
…
```
Mentions: OAI.SignedDisk.CenteredDiskEndpoint.Plane
theorem OAI.SignedDisk.CenteredDiskEndpoint.absoluteDiskAverage_eq_ofReal line 88
Source documentation
For every admissible input and positive radius the extended average agrees with the real absolute-value average, rather than a signed average.
```
theorem absoluteDiskAverage_eq_ofReal {f : Plane → ℝ} {x : Plane} {r : ℝ}
    (hf : IntegrableOn f (Metric.ball x r)) (hr : 0 < r) :
    absoluteDiskAverage f x r = ENNReal.ofReal (diskAverage (fun y => |f y|) x r) := by
…
```
Mentions: OAI.SignedDisk.CenteredDiskEndpoint.Plane, OAI.SignedDisk.CenteredDiskEndpoint.absoluteDiskAverage, OAI.SignedDisk.CenteredDiskEndpoint.diskAverage
theorem OAI.SignedDisk.CenteredDiskEndpoint.absoluteDiskAverage_ne_top line 95
theorem OAI.SignedDisk.CenteredDiskEndpoint.absoluteDiskAverage_le_maximal line 101
theorem OAI.SignedDisk.CenteredDiskEndpoint.maximal_abs line 105
theorem OAI.SignedDisk.CenteredDiskEndpoint.inW11_of_gradient line 109
theorem OAI.SignedDisk.CenteredDiskEndpoint.inW11Loc_of_gradient line 113
theorem OAI.SignedDisk.CenteredDiskEndpoint.integral_smul_sub_const line 117

theorem OAI.SignedDisk.CenteredDiskEndpoint.localized_cancellation line 130

Source documentation

The small-support zero-mass discount for actual integrable vector densities. The kernel need only be Lipschitz; no smoothness or unproved moment estimate is assumed.

theorem localized_cancellation {b : Plane → Plane} {K : Plane → ℝ}
    (hb : Integrable b) (hzero : ∫ y, b y = 0)
    {L : ℝ≥0} (hK : LipschitzWith L K) (z : Plane) {s : ℝ}
    (hsupp : ∀ᵐ y, b y ≠ 0 → ‖y - z‖ ≤ s) :
    ‖∫ y, K y • b y‖ ≤ (L : ℝ) * s * ∫ y, ‖b y‖ := by
…

Mentions: OAI.SignedDisk.CenteredDiskEndpoint.Plane

theorem OAI.SignedDisk.CenteredDiskEndpoint.HasWeakGradient.congr_ae line 161
Source documentation
A change of representatives on null sets does not change weak derivatives.
```
theorem HasWeakGradient.congr_ae {f f' : Plane → ℝ} {g g' : Plane → Plane}
    (h : HasWeakGradient f g) (hf : f =ᵐ[volume] f') (hg : g =ᵐ[volume] g') :
    HasWeakGradient f' g' := by
…
```
Mentions: OAI.SignedDisk.CenteredDiskEndpoint.Plane, OAI.SignedDisk.CenteredDiskEndpoint.HasWeakGradient
theorem OAI.SignedDisk.CenteredDiskEndpoint.HasWeakGradient.ae_unique line 178
Source documentation
The distributional gradient is unique as an a.e. class.
```
theorem HasWeakGradient.ae_unique {f : Plane → ℝ} {g g' : Plane → Plane}
    (h : HasWeakGradient f g) (h' : HasWeakGradient f g')
    (hg : LocallyIntegrable g) (hg' : LocallyIntegrable g') : g =ᵐ[volume] g' := by
…
```
Mentions: OAI.SignedDisk.CenteredDiskEndpoint.Plane, OAI.SignedDisk.CenteredDiskEndpoint.HasWeakGradient
theorem OAI.SignedDisk.CenteredDiskEndpoint.classicalGradient_apply line 195
Source documentation
Coordinate convention agreement with Mathlib's classical Euclidean gradient.
```
theorem classicalGradient_apply (f : Plane → ℝ) (x : Plane) (i : Fin 2) :
    gradient f x i = testPartial f i x := by
…
```
Mentions: OAI.SignedDisk.CenteredDiskEndpoint.Plane, OAI.SignedDisk.CenteredDiskEndpoint.testPartial
theorem OAI.SignedDisk.CenteredDiskEndpoint.contDiff_hasWeakGradient line 202
Source documentation
No integrability hypothesis is smuggled into the definition of the weak identity: every C¹ function satisfies it when tested against compact support.
```
theorem contDiff_hasWeakGradient {f : Plane → ℝ} (hf : ContDiff ℝ 1 f) :
    HasWeakGradient f (gradient f) := by
…
```
Mentions: OAI.SignedDisk.CenteredDiskEndpoint.Plane, OAI.SignedDisk.CenteredDiskEndpoint.HasWeakGradient
theorem OAI.SignedDisk.CenteredDiskEndpoint.disk_ae_eq_closedDisk line 230
Source documentation
Spherical boundaries are null, so the choice of an open disk does not alter Lebesgue differentiation averages.
```
theorem disk_ae_eq_closedDisk (x : Plane) (r : ℝ) :
    Metric.ball x r =ᵐ[volume] Metric.closedBall x r := by
…
```
Mentions: OAI.SignedDisk.CenteredDiskEndpoint.Plane
theorem OAI.SignedDisk.CenteredDiskEndpoint.average_closedDisk_eq line 237
theorem OAI.SignedDisk.CenteredDiskEndpoint.ae_tendsto_diskAverage_abs line 244
Source documentation
Almost every point is a Lebesgue point for absolute disk averages.
```
theorem ae_tendsto_diskAverage_abs {f : Plane → ℝ} (hf : Integrable f) :
    ∀ᵐ x, Tendsto (fun r => diskAverage (fun y => |f y|) x r)
      (𝓝[>] (0 : ℝ)) (𝓝 |f x|) := by
…
```
Mentions: OAI.SignedDisk.CenteredDiskEndpoint.Plane, OAI.SignedDisk.CenteredDiskEndpoint.diskAverage
theorem OAI.SignedDisk.CenteredDiskEndpoint.diskAverage_abs_le_of_radius_le line 256
Source documentation
Away from zero the denominator alone bounds all absolute averages.
```
theorem diskAverage_abs_le_of_radius_le {f : Plane → ℝ} (hf : Integrable f)
    (x : Plane) {a r : ℝ} (ha : 0 < a) (har : a ≤ r) :
    diskAverage (fun y => |f y|) x r ≤ (∫ y, |f y|) / (Real.pi * a ^ 2) := by
…
```
Mentions: OAI.SignedDisk.CenteredDiskEndpoint.Plane, OAI.SignedDisk.CenteredDiskEndpoint.diskAverage
theorem OAI.SignedDisk.CenteredDiskEndpoint.ae_maximal_ne_top line 276
Source documentation
A genuine clause of the endpoint, in fact valid for every L¹ input. No maximal bound, gradient hypothesis, or selected radius is used here.
```
theorem ae_maximal_ne_top {f : Plane → ℝ} (hf : Integrable f) :
    ∀ᵐ x, maximal f x ≠ ⊤ := by
…
```
Mentions: OAI.SignedDisk.CenteredDiskEndpoint.Plane, OAI.SignedDisk.CenteredDiskEndpoint.maximal
theorem OAI.SignedDisk.DiskGeometry.mem_tangent_ball_iff line 307
theorem OAI.SignedDisk.DiskGeometry.tangent_ball_mono line 315
def OAI.SignedDisk.DiskGeometry.entryParameter line 328
theorem OAI.SignedDisk.DiskGeometry.mem_tangent_ball_iff_entry line 330

theorem OAI.SignedDisk.DiskGeometry.shell_square_error line 337

Source documentation

Uniform estimate on the affine difference of squared distances in a thin shell.

theorem shell_square_error {l δ d : ℝ} (hl : 0 ≤ l) (hl3 : l ≤ 3)
    (hδ : 0 ≤ δ) (hδ1 : δ ≤ 1 / 4) (hd : 0 ≤ d) (hclose : |d - l| ≤ 2 * δ) :
    |d ^ 2 - l ^ 2| ≤ 13 * δ := by
…

theorem OAI.SignedDisk.DiskGeometry.shell_projection_lower line 349

Source documentation

A shell point separated from the tangency point has positive radial projection.

theorem shell_projection_lower {ρ δ l a w2 : ℝ}
    (hρ : 0 < ρ) (hl : 0 < l) (hl3 : l ≤ 3)
    (hδ : δ ≤ ρ ^ 2 / 1600) (hw : ρ ^ 2 ≤ w2)
    (herr : |w2 - 2 * l * a| ≤ 13 * δ) :
    ρ ^ 2 / 12 ≤ a := by
…

theorem OAI.SignedDisk.DiskGeometry.entry_window line 359

theorem OAI.SignedDisk.DiskGeometry.shell_entry_window line 376

Source documentation

Bound for the entry parameter for an actual shell near a tangent disk.

theorem shell_entry_window {z y θ : E} (hθ : ‖θ‖ = 1) {l ρ δ : ℝ}
    (hl : 1 / 2 ≤ l) (hl3 : l ≤ 3) (hρ : 0 < ρ) (hρ1 : ρ ≤ 1)
    (hδ : 0 < δ) (hδρ : δ ≤ ρ ^ 2 / 1600)
    (hsep : ρ ≤ ‖y - z‖)
    (hclose : |dist y (z + l • θ) - l| ≤ 2 * δ) :
    ρ ^ 2 / 12 ≤ ⟪y - z, θ⟫ ∧
    |entryParameter z y θ - l| ≤ 78 * δ / ρ ^ 2 := by
…

Mentions: OAI.SignedDisk.DiskGeometry.entryParameter

theorem OAI.SignedDisk.DiskGeometry.earlier_tangent_disk_subset line 398