TargetArea.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Target area from the exterior area theorem

Ahlfors, Conformal Invariants (1973), Exterior Area Theorem, supplies the area bound for the set omitted by a normalized univalent exterior map. The numerical bound yields the target-area estimate by change of variables and disjointness of the image and omitted disks.

def OAI.CircleDomainRigidity.ExteriorOmittedAreaBound line 24
Source documentation
The specialization of the published exterior area bound needed here. The map is evaluated only outside the closed source disk. Univalence and principal normalization are the hypotheses needed to obtain this bound from the exterior area theorem; this predicate is its numerical conclusion.
```
def ExteriorOmittedAreaBound (f : ℂ → ℂ) (R : ℝ) : Prop :=
…
```

theorem OAI.CircleDomainRigidity.integral_norm_deriv_sq_eq_image_area line 29

Source documentation

Complex change of variables identifies image area with Dirichlet area of an injective holomorphic map.

theorem integral_norm_deriv_sq_eq_image_area {f : ℂ → ℂ} {U : Set ℂ}
    (hU : MeasurableSet U) (hf : ∀ z ∈ U, DifferentiableAt ℂ f z)
    (hinj : InjOn f U) :
    (∫ z in U, ‖deriv f z‖ ^ 2) = (volume (f '' U)).toReal := by
…

theorem OAI.CircleDomainRigidity.integrable_norm_deriv_sq_of_image_area_finite line 47

Source documentation

Finite image area also gives actual integrability of the squared holomorphic derivative, so the Bochner integral cannot vanish by being undefined.

theorem integrable_norm_deriv_sq_of_image_area_finite {f : ℂ → ℂ} {U : Set ℂ}
    (hU : MeasurableSet U) (hf : ∀ z ∈ U, DifferentiableAt ℂ f z)
    (hinj : InjOn f U) (hfinite : volume (f '' U) ≠ ∞) :
    Integrable (fun z => ‖deriv f z‖ ^ 2) (volume.restrict U) := by
…

theorem OAI.CircleDomainRigidity.targetArea_of_exterior_area_bound line 68

Source documentation

The genuine exterior-area input yields target-radius summability, squared-derivative integrability, and the complete target-area estimate. The only geometric hypotheses on the target disks are disjoint interiors and disjointness from the image of the source domain.

theorem targetArea_of_exterior_area_bound {ι : Type*} [Countable ι]
    {f : ℂ → ℂ} {D : Set ℂ} (centers : ι → ℂ) (s : ι → ℝ) (R : ℝ)
    (hD : IsOpen D) (hf : DifferentiableOn ℂ f D) (hinj : InjOn f D)
    (hExterior : (closedBall (0 : ℂ) R)ᶜ ⊆ D)
    (hs : ∀ j, 0 ≤ s j)
    (hpair : Pairwise (Disjoint on fun j => ball (centers j) (s j)))
    (hdisj : ∀ j, Disjoint (f '' D) (ball (centers j) (s j)))
    (harea : ExteriorOmittedAreaBound f R) :
    Summable (fun j => s j ^ 2) ∧
    Integrable (fun z => ‖deriv f z‖ ^ 2) (volume.restrict (D ∩ ball 0 R)) ∧
    (∫ z in D ∩ ball 0 R, ‖deriv f z‖ ^ 2) +
      Real.pi * (∑' j, s j ^ 2) ≤ Real.pi * R ^ 2 := by
…

Mentions: OAI.CircleDomainRigidity.ExteriorOmittedAreaBound

theorem OAI.CircleDomainRigidity.integrable_norm_deriv_of_sq line 124

Source documentation

On a bounded measurable portion of a holomorphic domain, square integrability of the derivative implies integrability of its modulus.

theorem integrable_norm_deriv_of_sq {f : ℂ → ℂ} {D U : Set ℂ}
    (hD : IsOpen D) (hf : DifferentiableOn ℂ f D)
    (hU : MeasurableSet U) (hbU : IsBounded U) (hUD : U ⊆ D)
    (hsq : Integrable (fun z => ‖deriv f z‖ ^ 2) (volume.restrict U)) :
    Integrable (fun z => ‖deriv f z‖) (volume.restrict U) := by
…