DiskGeometry1.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.SignedDisk.DiskGeometry.monotone_increment_interval line 19

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.SignedDisk.DiskGeometry.monotone_increment_integrable line 42

theorem OAI.SignedDisk.DiskGeometry.monotone_jump_window_measure line 65

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.SignedDisk.DiskGeometry.volume_le_radial_sections line 98

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.SignedDisk.DiskGeometry.tangentMass line 162
Source documentation
Mass in the increasing family of tangent disks, away from its tangency cap.
```
def tangentMass (S : Measure ℂ) (ρ : ℝ) (z θ : ℂ) (L : ℝ) : ℝ :=
…
```
theorem OAI.SignedDisk.DiskGeometry.tangentMass_nonneg line 165
theorem OAI.SignedDisk.DiskGeometry.tangentMass_mono line 168
theorem OAI.SignedDisk.DiskGeometry.measurable_tangentMass line 178
def OAI.SignedDisk.DiskGeometry.rayCondition line 190
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.SignedDisk.DiskGeometry.measurableSet_rayCondition line 196

theorem OAI.SignedDisk.DiskGeometry.volume_rayCondition line 207

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.SignedDisk.DiskGeometry.rayCondition

def OAI.SignedDisk.DiskGeometry.thinShell line 239
theorem OAI.SignedDisk.DiskGeometry.measurableSet_thinShell line 241
theorem OAI.SignedDisk.DiskGeometry.shell_center_bounds line 244
theorem OAI.SignedDisk.DiskGeometry.shell_pair_close line 252

theorem OAI.SignedDisk.DiskGeometry.shell_subset_tangent_difference line 263

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.SignedDisk.DiskGeometry.shell_mass_le_jump line 295

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.SignedDisk.DiskGeometry.thinShell, OAI.SignedDisk.DiskGeometry.tangentMass

theorem OAI.SignedDisk.DiskGeometry.earlier_mass_le_interior line 341

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.SignedDisk.DiskGeometry.thinShell, OAI.SignedDisk.DiskGeometry.tangentMass

theorem OAI.SignedDisk.DiskGeometry.volume_interval_fibers line 372

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.SignedDisk.DiskGeometry.volume_affine_strip line 400

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.SignedDisk.DiskGeometry.complex_coordinate_separation line 421
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.SignedDisk.DiskGeometry.volume_two_point_strip line 430

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
…