GeometricRigidity.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Rigidity reduction with geometric source-area control

Source area and square-summability of the source radii follow from the geometry of disjoint source disks. The target area follows from an exterior-area bound. Together with the finite-hole flux estimate, these bounds force rigidity through the length-area argument.

theorem OAI.CircleDomainRigidity.identity_of_disk_geometry_and_target_flux line 25

Source documentation

A principal-normalized conformal map is the identity once the target area and flux estimates are established. Source area and square-summable source radii follow from disjoint disk geometry.

theorem identity_of_disk_geometry_and_target_flux {ι : Type*} [Countable ι]
    {f : ℂ → ℂ} {D : Set ℂ} (centers : ι → ℂ) (r s : ι → ℝ) (R : ℝ)
    (hD : IsOpen D) (hconn : IsPreconnected D) (hf : DifferentiableOn ℂ f D)
    (hDinf : IsBounded Dᶜ)
    (hnorm : Tendsto (fun z : ℂ => f z - z) (cobounded ℂ) (𝓝 0))
    (hR : 0 ≤ R) (hr : ∀ j, 0 ≤ r j)
    (hWne : (D ∩ ball 0 R).Nonempty)
    (hpair : Pairwise (Disjoint on fun j => ball (centers j) (r j)))
    (hdisj : ∀ j, Disjoint D (ball (centers j) (r j)))
    (hcontain : ∀ j, ball (centers j) (r j) ⊆ ball 0 R)
    (hi : Integrable (fun z => ‖deriv f z‖) (volume.restrict (D ∩ ball 0 R)))
    (hi2 : Integrable (fun z => ‖deriv f z‖ ^ 2) (volume.restrict (D ∩ ball 0 R)))
…

theorem OAI.CircleDomainRigidity.identity_of_disk_geometry_exterior_area_and_flux line 60

Source documentation

All area and integrability premises follow from geometric disjointness and the exterior omitted-area bound, under the limiting-flux inequality.

theorem identity_of_disk_geometry_exterior_area_and_flux
    {ι : Type*} [Countable ι] {f : ℂ → ℂ} {D : Set ℂ}
    (sourceCenters targetCenters : ι → ℂ) (r s : ι → ℝ) (R : ℝ)
    (hD : IsOpen D) (hconn : IsPreconnected D) (hf : DifferentiableOn ℂ f D)
    (hinj : InjOn f D)
    (hExterior : (closedBall (0 : ℂ) R)ᶜ ⊆ D)
    (hnorm : Tendsto (fun z : ℂ => f z - z) (cobounded ℂ) (𝓝 0))
    (hR : 0 ≤ R) (hr : ∀ j, 0 ≤ r j) (hs : ∀ j, 0 ≤ s j)
    (hWne : (D ∩ ball 0 R).Nonempty)
    (hSourcePair : Pairwise (Disjoint on fun j => ball (sourceCenters j) (r j)))
    (hSourceDisj : ∀ j, Disjoint D (ball (sourceCenters j) (r j)))
    (hSourceContain : ∀ j, ball (sourceCenters j) (r j) ⊆ ball 0 R)
…

theorem OAI.CircleDomainRigidity.identity_of_disk_geometry_exterior_area_and_finite_flux line 94

Source documentation

The finite-hole flux estimates suffice for normalized rigidity. Source and target geometry imply the required square-summability, so the remaining tail tends to zero without any separate convergence assumption.

theorem identity_of_disk_geometry_exterior_area_and_finite_flux
    {ι : Type*} [Countable ι] {f : ℂ → ℂ} {D : Set ℂ}
    (sourceCenters targetCenters : ι → ℂ) (r s : ι → ℝ) (R : ℝ)
    (hD : IsOpen D) (hconn : IsPreconnected D) (hf : DifferentiableOn ℂ f D)
    (hinj : InjOn f D)
    (hExterior : (closedBall (0 : ℂ) R)ᶜ ⊆ D)
    (hnorm : Tendsto (fun z : ℂ => f z - z) (cobounded ℂ) (𝓝 0))
    (hR : 0 ≤ R) (hr : ∀ j, 0 ≤ r j) (hs : ∀ j, 0 ≤ s j)
    (hWne : (D ∩ ball 0 R).Nonempty)
    (hSourcePair : Pairwise (Disjoint on fun j => ball (sourceCenters j) (r j)))
    (hSourceDisj : ∀ j, Disjoint D (ball (sourceCenters j) (r j)))
    (hSourceContain : ∀ j, ball (sourceCenters j) (r j) ⊆ ball 0 R)
…