Schwarz–Pick, Lipschitz form to Weyl's lemma for \bar∂
TheoremSchwarz–Pick, Lipschitz form#
A holomorphic self-map of the unit disc is a nonexpanding
map of the metric space TauCeti.PoincareDisc.
Together with
TauCeti.PoincareDisc.isometry_iff_exists_eq_unitDiscStandardAutomorphismIsometryEquiv this says
that a holomorphic self-map of the Poincaré disc is nonexpanding, and is an isometry precisely
when it is a disc automorphism.
TauCeti.PoincareDisc.lipschitzWith_one {F : TauCeti.PoincareDisc → TauCeti.PoincareDisc} {f : ℂ → ℂ}
(hf : DifferentiableOn ℂ f (Metric.ball 0 1))
(hrep :
∀ (z : TauCeti.PoincareDisc),
↑(TauCeti.PoincareDisc.toUnitDisc (F z)) = f ↑(TauCeti.PoincareDisc.toUnitDisc z)) :
LipschitzWith 1 F
Lean
Formalized in Tau Ceti as TauCeti.PoincareDisc.lipschitzWith_one.
Other forms
Schwarz--Pick for the Poincaré length. Formalized in Tau Ceti as TauCeti.hyperbolicLength_comp_le.
TauCeti.hyperbolicLength_comp_le {γ γ' : ℝ → ℂ} {a b : ℝ} {f : ℂ → ℂ}
(hf : DifferentiableOn ℂ f (Metric.ball 0 1))
(hmaps : Set.MapsTo f (Metric.ball 0 1) (Metric.ball 0 1)) (hγ : ContinuousOn γ (Set.uIcc a b))
(hderiv : ∀ t ∈ Set.uIoo a b, HasDerivAt γ (γ' t) t) (hγ' : ContinuousOn γ' (Set.uIcc a b))
(hmem : ∀ t ∈ Set.uIcc a b, ‖γ t‖ < 1) :
TauCeti.hyperbolicLength (f ∘ γ) a b ≤ TauCeti.hyperbolicLength γ a b
Schwarz--Pick, distance form. Formalized in Tau Ceti as TauCeti.hyperbolicDist_map_le.
TauCeti.hyperbolicDist_map_le {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f (Metric.ball 0 1))
(hmaps : Set.MapsTo f (Metric.ball 0 1) (Metric.ball 0 1)) {z w : ℂ} (hz : z ∈ Metric.ball 0 1)
(hw : w ∈ Metric.ball 0 1) : TauCeti.hyperbolicDist (f z) (f w) ≤ TauCeti.hyperbolicDist z w
Schwarz–Pick for the Poincaré metric. Formalized in Tau Ceti as TauCeti.PoincareDisc.dist_map_le.
TauCeti.PoincareDisc.dist_map_le {F : TauCeti.PoincareDisc → TauCeti.PoincareDisc} {f : ℂ → ℂ}
(hf : DifferentiableOn ℂ f (Metric.ball 0 1))
(hrep :
∀ (z : TauCeti.PoincareDisc),
↑(TauCeti.PoincareDisc.toUnitDisc (F z)) = f ↑(TauCeti.PoincareDisc.toUnitDisc z))
(z w : TauCeti.PoincareDisc) : dist (F z) (F w) ≤ dist z w
Sources
Uses 2
TheoremShimizu's inequality at two cusps#
Let D and D' be normalized cusp data of a discrete
Γ ≤ PSL(2, ℝ). If g ∈ Γ does not carry the cusp of D' to the cusp of D, then the height of
g • z above the cusp of D and the height of z above the cusp of D', each measured in the
scaling coordinate of its datum, have product at most D.width * D'.width.
This is Shimizu's lemma (Subgroup.im_smul_mul_im_le_abs_mul_of_upperRightHom_mem) for the
conjugate group σ Γ σ⁻¹, which contains the translation by D.width, applied to σ g σ'⁻¹,
which conjugates the translation by D'.width into it.
TauCeti.Subgroup.CuspDatum.im_scaling_smul_smul_mul_im_scaling_smul_le
{Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum)
[DiscreteTopology ↥Γ] (D' : Γ.CuspDatum) {g : ↥Γ} (hg : g • D'.cusp ≠ D.cusp)
(z : UpperHalfPlane) : (D.scaling • g • z).im * (D'.scaling • z).im ≤ D.width * D'.width
Lean
Formalized in Tau Ceti as TauCeti.Subgroup.CuspDatum.im_scaling_smul_smul_mul_im_scaling_smul_le.
Sources
Uses 1 · Used by 7
M_k(N, χ)TheoremThe Stieltjes--Perron vanishing theorem#
A Nevanlinna measure gives no mass to a compact
interval over which the imaginary part of the represented function is continuous up to the real
axis and vanishes there. Continuity is asked for on the closed rectangle of any positive height
d over the interval, as a function holomorphic near the interval supplies it.
TauCeti.measure_Icc_eq_zero_of_eq_nevanlinnaKernel_add {F : ℂ → ℂ} {mu : MeasureTheory.Measure ℝ}
{beta c : ℝ} [MeasureTheory.IsFiniteMeasure mu]
(hrep :
∀ z ∈ UpperHalfPlane.upperHalfPlaneSet,
F z = ↑beta * z + ∫ (x : ℝ), TauCeti.nevanlinnaKernel z x ∂mu + ↑c)
{a b d : ℝ} (hab : a < b) (hd : 0 < d)
(hcont : ContinuousOn (fun z => (F z).im) (Set.Icc a b ×ℂ Set.Icc 0 d))
(hzero : ∀ u ∈ Set.Icc a b, (F ↑u).im = 0) : mu (Set.Icc a b) = 0
Lean
Formalized in Tau Ceti as TauCeti.measure_Icc_eq_zero_of_eq_nevanlinnaKernel_add.
Sources
Uses 1
TheoremUniqueness in the Riemann mapping theorem, up to a disc automorphism#
If f and g are
holomorphic injections from an open set U onto the open unit disc, then there are u on the
unit circle and a in the unit disc such that
g z = u * (f z - a) / (1 - conj a * f z)
for every z ∈ U.
TauCeti.exists_eqOn_unitDiscStandardAutomorphismFormula_comp {U : Set ℂ} (hU : IsOpen U)
{f g : ℂ → ℂ} (hf : DifferentiableOn ℂ f U) (hg : DifferentiableOn ℂ g U) (hfi : Set.InjOn f U)
(hgi : Set.InjOn g U) (hfimage : f '' U = Metric.ball 0 1) (hgimage : g '' U = Metric.ball 0 1) :
∃ u a, Set.EqOn g (fun z => ↑u * ((f z - ↑a) / (1 - (starRingEnd ℂ) ↑a * f z))) U
Lean
Formalized in Tau Ceti as TauCeti.exists_eqOn_unitDiscStandardAutomorphismFormula_comp.
Sources
Uses 1 · Used by 1
TheoremWeyl's lemma for \bar∂#
A distributional solution with finite-dimensional complex coefficients agrees almost everywhere on its domain with a holomorphic function.
TauCeti.HasWeakConjWirtingerDerivOn.exists_differentiableOn_ae_eq.{u_1} {F : Type u_1}
[NormedAddCommGroup F] [NormedSpace ℂ F] {μ : MeasureTheory.Measure ℂ}
{Ω : TopologicalSpace.Opens ℂ} {u : ℂ → F} [FiniteDimensional ℂ F] [μ.IsAddHaarMeasure]
(h : TauCeti.HasWeakConjWirtingerDerivOn μ Ω u 0) :
∃ v, DifferentiableOn ℂ v ↑Ω ∧ u =ᵐ[μ.restrict ↑Ω] v
Lean
Formalized in Tau Ceti as TauCeti.HasWeakConjWirtingerDerivOn.exists_differentiableOn_ae_eq.
Sources
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.