Geometry.lean`

47 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DiskGeometry.mem_tangent_ball_iff line 17
theorem OAI.DiskGeometry.tangent_ball_mono line 25
def OAI.DiskGeometry.entryParameter line 38
theorem OAI.DiskGeometry.mem_tangent_ball_iff_entry line 40

theorem OAI.DiskGeometry.shell_square_error line 47

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.DiskGeometry.shell_projection_lower line 59

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.DiskGeometry.entry_window line 69

theorem OAI.DiskGeometry.shell_entry_window line 86

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.DiskGeometry.entryParameter

theorem OAI.DiskGeometry.earlier_tangent_disk_subset line 108

theorem OAI.DiskGeometry.monotone_increment_interval line 151

Source documentation

Cancellation of translated monotone integrals on a finite interval.

theorem monotone_increment_interval {G : ℝ → ℝ} (hG : Monotone G)
    {C v : ℝ} (h0 : ∀ x, 0 ≤ G x) (hC : ∀ x, G x ≤ C) (hv : 0 ≤ v)
    (a b : ℝ) :
    (∫ l in a..b, (G (l + v) - G (l - v))) ≤ 2 * v * C := by
…

theorem OAI.DiskGeometry.monotone_increment_integrable line 174

theorem OAI.DiskGeometry.monotone_jump_window_measure line 197

Source documentation

The permitted jump times have uniformly bounded length, independent of the size of the original positive measure. Only its truncated distribution is used.

theorem monotone_jump_window_measure {H : ℝ → ℝ} (hH : Monotone H)
    (hH0 : ∀ l, 0 ≤ H l) {T U v : ℝ} (hT : 0 ≤ T) (hU : 0 < U) (hv : 0 ≤ v) :
    volume {l | H (l - v) ≤ T ∧ U ≤ H (l + v) - H (l - v)} ≤
      ENNReal.ofReal (2 * v * (1 + T / U)) := by
…

theorem OAI.DiskGeometry.volume_le_radial_sections line 234

Source documentation

A polar-coordinate area bound from uniform lengths of radial sections.

theorem volume_le_radial_sections {s : Set ℂ} (hs : MeasurableSet s)
    (z : ℂ) {R : ℝ} (hR : 0 ≤ R) {B : ℝ≥0∞}
    (hbound : ∀ x ∈ s, ‖x - z‖ ≤ R)
    (hsections : ∀ θ : ℝ, volume {r : ℝ | 0 < r ∧
      z + (r : ℂ) * ((Real.cos θ : ℂ) + (Real.sin θ : ℂ) * Complex.I) ∈ s} ≤ B) :
    volume s ≤ ENNReal.ofReal (2 * Real.pi * R) * B := by
…

def OAI.DiskGeometry.tangentMass line 302
Source documentation
Mass in the increasing family of tangent disks, away from its tangency cap.
```
def tangentMass (S : Measure ℂ) (ρ : ℝ) (z θ : ℂ) (L : ℝ) : ℝ :=
…
```
theorem OAI.DiskGeometry.tangentMass_nonneg line 305
theorem OAI.DiskGeometry.tangentMass_mono line 308
theorem OAI.DiskGeometry.measurable_tangentMass line 318
def OAI.DiskGeometry.rayCondition line 330
Source documentation
The measurable condition whose planar cost is bounded by the ray-length estimate.
```
def rayCondition (S : Measure ℂ) (ρ T U v : ℝ) (x z : ℂ) : Prop :=
…
```
theorem OAI.DiskGeometry.measurableSet_rayCondition line 336

theorem OAI.DiskGeometry.volume_rayCondition line 347

Source documentation

Full two-dimensional ray-condition estimate, independent of the chosen radius.

theorem volume_rayCondition (S : Measure ℂ) [IsFiniteMeasure S] (ρ : ℝ)
    {T U v : ℝ} (hT : 0 ≤ T) (hU : 0 < U) (hv : 0 ≤ v) (z : ℂ) :
    volume {x : ℂ | rayCondition S ρ T U v x z} ≤
      ENNReal.ofReal (6 * Real.pi) * ENNReal.ofReal (2 * v * (1 + T / U)) := by
…

Mentions: OAI.DiskGeometry.rayCondition

def OAI.DiskGeometry.thinShell line 383
theorem OAI.DiskGeometry.measurableSet_thinShell line 385
theorem OAI.DiskGeometry.shell_center_bounds line 388
theorem OAI.DiskGeometry.shell_pair_close line 396

theorem OAI.DiskGeometry.shell_subset_tangent_difference line 407

Source documentation

Every distant point of the thin shell crosses the tangent disks in the short window.

theorem shell_subset_tangent_difference {z θ : ℂ} (hθ : ‖θ‖ = 1) {l ρ δ : ℝ}
    (hl : 1 / 2 ≤ l) (hl3 : l ≤ 3) (hρ : 0 < ρ) (hρ1 : ρ ≤ 1)
    (hδ : 0 < δ) (hδρ : δ ≤ ρ ^ 2 / 1600) :
    {y : ℂ | ρ ≤ ‖y - z‖ ∧ |‖y - (z + l • θ)‖ - l| ≤ 2 * δ} ⊆
      ({y : ℂ | ρ ≤ ‖y - z‖} ∩
        Metric.ball (z + (l + 200 * δ / ρ ^ 2) • θ) (l + 200 * δ / ρ ^ 2)) \
      ({y : ℂ | ρ ≤ ‖y - z‖} ∩
        Metric.ball (z + (l - 200 * δ / ρ ^ 2) • θ) (l - 200 * δ / ρ ^ 2)) := by
…

theorem OAI.DiskGeometry.shell_mass_le_jump line 439

Source documentation

The shell mass away from a cap is bounded by the one-dimensional tangent-mass jump.

theorem shell_mass_le_jump (S : Measure ℂ) [IsFiniteMeasure S]
    {x z : ℂ} {r ρ δ : ℝ} (hr : r ∈ Icc (1 : ℝ) 2) (hρ : 0 < ρ) (hρ1 : ρ ≤ 1)
    (hδ : 0 < δ) (hδρ : δ ≤ ρ ^ 2 / 1600) (hz : z ∈ thinShell x r δ) :
    (S (thinShell x r δ \ Metric.ball z ρ)).toReal ≤
      tangentMass S ρ z (‖x - z‖⁻¹ • (x - z)) (‖x - z‖ + 200 * δ / ρ ^ 2) -
      tangentMass S ρ z (‖x - z‖⁻¹ • (x - z)) (‖x - z‖ - 200 * δ / ρ ^ 2) := by
…

Mentions: OAI.DiskGeometry.thinShell, OAI.DiskGeometry.tangentMass

theorem OAI.DiskGeometry.earlier_mass_le_interior line 485

Source documentation

The earlier tangent-disk mass is controlled by the concentric interior mass.

theorem earlier_mass_le_interior (S : Measure ℂ) [IsFiniteMeasure S]
    {x z : ℂ} {r ρ δ : ℝ} (hr : r ∈ Icc (1 : ℝ) 2) (hρ : 0 < ρ) (hρ1 : ρ ≤ 1)
    (hδ : 0 < δ) (hδρ : δ ≤ ρ ^ 2 / 1600) (hz : z ∈ thinShell x r δ) :
    tangentMass S ρ z (‖x - z‖⁻¹ • (x - z)) (‖x - z‖ - 200 * δ / ρ ^ 2) ≤
      (S (Metric.ball x (r - δ))).toReal := by
…

Mentions: OAI.DiskGeometry.thinShell, OAI.DiskGeometry.tangentMass

theorem OAI.DiskGeometry.volume_interval_fibers line 520

Source documentation

Area of a strip with continuously moving interval fibers.

theorem volume_interval_fibers (c : ℝ → ℝ) (hc : Continuous c)
    (lo hi w : ℝ) :
    volume {p : ℝ × ℝ | p.2 ∈ Icc lo hi ∧
      p.1 ∈ Icc (c p.2 - w) (c p.2 + w)} =
      ENNReal.ofReal (hi - lo) * ENNReal.ofReal (2 * w) := by
…

theorem OAI.DiskGeometry.volume_affine_strip line 548

Source documentation

A nonvertical affine strip cut off in the second coordinate.

theorem volume_affine_strip {a : ℝ} (ha : a ≠ 0) (b c d R w : ℝ) :
    volume {p : ℝ × ℝ | |p.2 - d| ≤ R ∧ |a * p.1 + b * p.2 + c| ≤ w} =
      ENNReal.ofReal (2 * R) * ENNReal.ofReal (2 * (w / |a|)) := by
…

theorem OAI.DiskGeometry.complex_coordinate_separation line 569
Source documentation
At least one coordinate sees half the Euclidean separation.
```
theorem complex_coordinate_separation {z : ℂ} {ρ : ℝ} (hz : ρ ≤ ‖z‖) :
    ρ / 2 ≤ |z.re| ∨ ρ / 2 ≤ |z.im| := by
…
```

theorem OAI.DiskGeometry.volume_two_point_strip line 578

Source documentation

The centers of two separated points lying on an almost common circle form an affine strip of small area. No selected radius occurs here.

theorem volume_two_point_strip {y z : ℂ} {ρ δ : ℝ} (hρ : 0 < ρ) (hδ : 0 ≤ δ)
    (hyz : ρ ≤ ‖y - z‖) :
    volume {x : ℂ | ‖x - z‖ ≤ 3 ∧ |‖x - y‖ ^ 2 - ‖x - z‖ ^ 2| ≤ 13 * δ} ≤
      ENNReal.ofReal (156 * δ / ρ) := by
…

def OAI.DiskGeometry.pairCondition line 644
theorem OAI.DiskGeometry.measurableSet_pairCondition line 648
theorem OAI.DiskGeometry.volume_pairCondition line 657
def OAI.DiskGeometry.pairMass line 676
theorem OAI.DiskGeometry.measurable_pairMass line 679
def OAI.DiskGeometry.rayIndicator line 683
theorem OAI.DiskGeometry.measurable_rayIndicator line 686

theorem OAI.DiskGeometry.lintegral_pairMass line 691

Source documentation

The first contribution to the Borel majorant is controlled by the two-point strip.

theorem lintegral_pairMass (ν : Measure ℂ) [IsFiniteMeasure ν] {ρ δ : ℝ}
    (hρ : 0 < ρ) (hδ : 0 ≤ δ) (hδquarter : δ ≤ 1 / 4) :
    (∫⁻ x : ℂ, ∫⁻ z : ℂ, pairMass ν ρ δ x z ∂ν) ≤
      ENNReal.ofReal (156 * δ / ρ) * ν univ * ν univ := by
…

Mentions: OAI.DiskGeometry.pairMass

theorem OAI.DiskGeometry.lintegral_rayIndicator line 727

Source documentation

The second contribution is controlled by monotone ray jumps and polar coordinates.

theorem lintegral_rayIndicator (ν S : Measure ℂ) [IsFiniteMeasure ν] [IsFiniteMeasure S]
    (ρ : ℝ) {T U v : ℝ} (hT : 0 ≤ T) (hU : 0 < U) (hv : 0 ≤ v) :
    (∫⁻ x : ℂ, ∫⁻ z : ℂ, rayIndicator S ρ T U v x z ∂ν) ≤
      (ENNReal.ofReal (6 * Real.pi) * ENNReal.ofReal (2 * v * (1 + T / U))) * ν univ := by
…

Mentions: OAI.DiskGeometry.rayIndicator

theorem OAI.DiskGeometry.bad_cap_bracket line 754

Source documentation

Failure of every cap forces the majorant bracket to be at least one.

theorem bad_cap_bracket (S ν : Measure ℂ) [IsFiniteMeasure S] [IsFiniteMeasure ν]
    {x z : ℂ} {r ρ δ T U : ℝ} (hr : r ∈ Icc (1 : ℝ) 2)
    (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (hδ : 0 < δ) (hδρ : δ ≤ ρ ^ 2 / 1600)
    (hT : 0 ≤ T) (hU : 0 < U) (hz : z ∈ thinShell x r δ)
    (hi : S (Metric.ball x (r - δ)) ≤ ENNReal.ofReal T)
    (hb : ENNReal.ofReal (2 * U) < (S + ν) (thinShell x r δ \ Metric.ball z ρ)) :
    1 ≤ (ENNReal.ofReal U)⁻¹ * pairMass ν ρ δ x z +
      rayIndicator S ρ T U (200 * δ / ρ ^ 2) x z := by
…

Mentions: OAI.DiskGeometry.thinShell, OAI.DiskGeometry.pairMass, OAI.DiskGeometry.rayIndicator

def OAI.DiskGeometry.shellMajorant line 799
Source documentation
A radius-independent Borel majorant combining separated shell pairs and ray jumps.
```
def shellMajorant (ν S : Measure ℂ) (ρ δ T U : ℝ) (x : ℂ) : ℝ≥0∞ :=
…
```
theorem OAI.DiskGeometry.measurable_shellMajorant line 803
theorem OAI.DiskGeometry.shellMajorant_eq_bracket line 808

theorem OAI.DiskGeometry.lintegral_shellMajorant line 820

Source documentation

The majorant is integrable uniformly over all radii.

theorem lintegral_shellMajorant (ν S : Measure ℂ) [IsFiniteMeasure ν] [IsFiniteMeasure S]
    {ρ δ T U : ℝ} (hρ : 0 < ρ) (hδ : 0 ≤ δ) (hδquarter : δ ≤ 1 / 4)
    (hT : 0 ≤ T) (hU : 0 < U) :
    (∫⁻ x, shellMajorant ν S ρ δ T U x) ≤
      (ENNReal.ofReal U)⁻¹ ^ 2 * (ENNReal.ofReal (156 * δ / ρ) * ν univ * ν univ) +
      (ENNReal.ofReal U)⁻¹ * ((ENNReal.ofReal (6 * Real.pi) *
        ENNReal.ofReal (2 * (200 * δ / ρ ^ 2) * (1 + T / U))) * ν univ) := by
…

Mentions: OAI.DiskGeometry.shellMajorant

theorem OAI.DiskGeometry.one_le_majorant_of_no_cap line 838

Source documentation

The majorant detects simultaneous failure of concentration at every cap.

theorem one_le_majorant_of_no_cap (ν S : Measure ℂ) [IsFiniteMeasure ν] [IsFiniteMeasure S]
    {ρ δ T U : ℝ} (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (hδ : 0 < δ)
    (hδρ : δ ≤ ρ ^ 2 / 1600) (hT : 0 ≤ T) (hU : 0 < U)
    {x : ℂ} {r : ℝ} (hr : r ∈ Icc (1 : ℝ) 2)
    (hν : ENNReal.ofReal U ≤ ν (thinShell x r δ))
    (hS : S (Metric.ball x (r - δ)) ≤ ENNReal.ofReal T)
    (hbad : ∀ z ∈ thinShell x r δ,
      ENNReal.ofReal (2 * U) < (S + ν) (thinShell x r δ \ Metric.ball z ρ)) :
    1 ≤ shellMajorant ν S ρ δ T U x := by
…

Mentions: OAI.DiskGeometry.thinShell, OAI.DiskGeometry.shellMajorant

theorem OAI.DiskGeometry.shell_concentration line 866

Source documentation

Full radius-independent shell concentration, with explicit absolute constants.

theorem shell_concentration (ν S : Measure ℂ) [IsFiniteMeasure ν] [IsFiniteMeasure S]
    {ρ δ T U : ℝ} (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (hδ : 0 < δ)
    (hδρ : δ ≤ ρ ^ 2 / 1600) (hT : 0 ≤ T) (hU : 0 < U) :
    ∃ E : Set ℂ, MeasurableSet E ∧
      volume E ≤
        (ENNReal.ofReal U)⁻¹ ^ 2 * (ENNReal.ofReal (156 * δ / ρ) * ν univ * ν univ) +
        (ENNReal.ofReal U)⁻¹ * ((ENNReal.ofReal (6 * Real.pi) *
          ENNReal.ofReal (2 * (200 * δ / ρ ^ 2) * (1 + T / U))) * ν univ) ∧
      ∀ x ∉ E, ∀ r ∈ Icc (1 : ℝ) 2,
        ENNReal.ofReal U ≤ ν (thinShell x r δ) →
        S (Metric.ball x (r - δ)) ≤ ENNReal.ofReal T →
        ∃ z ∈ thinShell x r δ,
…

Mentions: OAI.DiskGeometry.thinShell