FiniteModelCoordinates.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Coordinates on the actual finite circle model

The circle domain, its smooth inverse and the target coordinates are constructed from the finite metric completion. Every measurable piece of a source mask has exactly the same Dirichlet energy on its image.

theorem OAI.CircleDomainRigidity.FiniteTransfer.openCompletedRegion_subset_completedRegion line 23
theorem OAI.CircleDomainRigidity.FiniteTransfer.finite_metric_model_with_coordinates line 29

theorem OAI.CircleDomainRigidity.FiniteTransfer.finite_metric_model_with_masked_fillings line 64

Source documentation

The source regions are the actual mask interiors of the completion. No extra source coordinates or smoothness assumptions are introduced.

theorem finite_metric_model_with_masked_fillings
    (hcompact : SmoothCompactMetricSphereUniformization) (hfinite : FiniteJordanModelUniformization)
    {I : Type*} [Finite I] (T : I → ℂ ≃ₜ ℂ)
    (hdisj : Pairwise (Disjoint on fun i => closure (jordanInterior (T i))))
    {K Ω : Set (ℝ × ℝ)} (hKQ : sphericalCore K ⊆ openCompletedRegion T)
    (hQΩ : realChartDomain (completedRegion T) ⊆ Ω)
    (g : (ℝ × ℝ) → PlanarMetric) (hg : ContDiff ℝ ∞ g) (hPD : ∀ z, (g z).PosDef)
    (hfar : ∃ R : ℝ, 0 < R ∧ ∀ z ∉ Metric.closedBall 0 R, g z = sphericalMetricFactor z • 1)
    (hcore : ∀ᶠ z in 𝓝ˢ K, g z = sphericalMetricFactor z • 1)
    {J : Type*} {n : ℕ} {D : J → Set (ℝ × ℝ)} {M : Fin n → Set (ℝ × ℝ)}
    {v F : Fin n → (ℝ × ℝ) → UnitAddCircle}
    (hF : IsMaskedFilledCircleFamily D Ω M v F) :
…