SourceArea.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The source-area inequality for circle domains

The source region and the interiors of its complementary disks are disjoint subsets of one outer disk. Countable additivity gives the source-area inequality used in Section 6 of the rigidity manuscript. No regularity of the remaining point components is needed.

theorem OAI.CircleDomainRigidity.measure_source_add_disks_le line 23

Source documentation

Countable additivity for a disjoint measurable family, together with one further disjoint source set, gives an area bound in a containing set.

theorem measure_source_add_disks_le {X ι : Type*} [MeasurableSpace X] [Countable ι]
    (μ : Measure X) {U O : Set X} (D : ι → Set X)
    (hD : ∀ j, MeasurableSet (D j))
    (hpair : Pairwise (Disjoint on D))
    (hdisj : ∀ j, Disjoint U (D j))
    (hUO : U ⊆ O) (hDO : ∀ j, D j ⊆ O) :
    μ U + ∑' j, μ (D j) ≤ μ O := by
…

theorem OAI.CircleDomainRigidity.sourceArea_le line 37

Source documentation

The actual geometric source-area bound for pairwise disjoint disks.

theorem sourceArea_le {ι : Type*} [Countable ι] {U : Set ℂ}
    (centers : ι → ℂ) (radii : ι → ℝ) (R : ℝ)
    (hpair : Pairwise (Disjoint on fun j => ball (centers j) (radii j)))
    (hdisj : ∀ j, Disjoint U (ball (centers j) (radii j)))
    (hUO : U ⊆ ball 0 R)
    (hDO : ∀ j, ball (centers j) (radii j) ⊆ ball 0 R) :
    volume U + ∑' j, volume (ball (centers j) (radii j)) ≤ volume (ball (0 : ℂ) R) :=
…

theorem OAI.CircleDomainRigidity.real_volume_ball line 48

Source documentation

Planar ball area, expressed as an ordinary real number.

theorem real_volume_ball (center : ℂ) {r : ℝ} (hr : 0 ≤ r) :
    (volume (ball center r)).toReal = Real.pi * r ^ 2 := by
…

theorem OAI.CircleDomainRigidity.summable_radii_sq line 56

Source documentation

Finitely bounded, pairwise disjoint disks have square-summable radii.

theorem summable_radii_sq {ι : Type*} [Countable ι]
    (centers : ι → ℂ) (radii : ι → ℝ) (R : ℝ)
    (hr : ∀ j, 0 ≤ radii j)
    (hpair : Pairwise (Disjoint on fun j => ball (centers j) (radii j)))
    (hDO : ∀ j, ball (centers j) (radii j) ⊆ ball 0 R) :
    Summable (fun j => radii j ^ 2) := by
…

theorem OAI.CircleDomainRigidity.sourceArea_real_le line 73

Source documentation

The real source-area inequality, with the familiar factor π.

theorem sourceArea_real_le {ι : Type*} [Countable ι] {U : Set ℂ}
    (centers : ι → ℂ) (radii : ι → ℝ) (R : ℝ)
    (hr : ∀ j, 0 ≤ radii j) (hR : 0 ≤ R)
    (hpair : Pairwise (Disjoint on fun j => ball (centers j) (radii j)))
    (hdisj : ∀ j, Disjoint U (ball (centers j) (radii j)))
    (hUO : U ⊆ ball 0 R)
    (hDO : ∀ j, ball (centers j) (radii j) ⊆ ball 0 R) :
    (volume U).toReal + Real.pi * (∑' j, radii j ^ 2) ≤ Real.pi * R ^ 2 := by
…