Basic.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.CenteredDiskEndpoint.volume_disk line 13
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.CenteredDiskEndpoint.Plane
theorem OAI.CenteredDiskEndpoint.absoluteDiskAverage_eq_ofReal line 21
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.CenteredDiskEndpoint.Plane, OAI.CenteredDiskEndpoint.absoluteDiskAverage, OAI.CenteredDiskEndpoint.diskAverage
theorem OAI.CenteredDiskEndpoint.absoluteDiskAverage_ne_top line 28
theorem OAI.CenteredDiskEndpoint.absoluteDiskAverage_le_maximal line 34
theorem OAI.CenteredDiskEndpoint.maximal_abs line 38
theorem OAI.CenteredDiskEndpoint.inW11_of_gradient line 42
theorem OAI.CenteredDiskEndpoint.inW11Loc_of_gradient line 46
theorem OAI.CenteredDiskEndpoint.integral_smul_sub_const line 50

theorem OAI.CenteredDiskEndpoint.localized_cancellation line 63

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.CenteredDiskEndpoint.Plane

theorem OAI.CenteredDiskEndpoint.HasWeakGradient.congr_ae line 97
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.CenteredDiskEndpoint.Plane, OAI.CenteredDiskEndpoint.HasWeakGradient
theorem OAI.CenteredDiskEndpoint.HasWeakGradient.ae_unique line 113
theorem OAI.CenteredDiskEndpoint.classicalGradient_apply line 130
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.CenteredDiskEndpoint.Plane, OAI.CenteredDiskEndpoint.testPartial
theorem OAI.CenteredDiskEndpoint.contDiff_hasWeakGradient line 137
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.CenteredDiskEndpoint.Plane, OAI.CenteredDiskEndpoint.HasWeakGradient
theorem OAI.CenteredDiskEndpoint.disk_ae_eq_closedDisk line 165
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.CenteredDiskEndpoint.Plane
theorem OAI.CenteredDiskEndpoint.average_closedDisk_eq line 172
theorem OAI.CenteredDiskEndpoint.ae_tendsto_diskAverage_abs line 179
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.CenteredDiskEndpoint.Plane, OAI.CenteredDiskEndpoint.diskAverage
theorem OAI.CenteredDiskEndpoint.diskAverage_abs_le_of_radius_le line 191
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.CenteredDiskEndpoint.Plane, OAI.CenteredDiskEndpoint.diskAverage
theorem OAI.CenteredDiskEndpoint.ae_maximal_ne_top line 211
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.CenteredDiskEndpoint.Plane, OAI.CenteredDiskEndpoint.maximal