SmoothFiniteTransfer.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Analytic assembly after the finite disks are selected

A frequently small wedge integral and the eventual collar conditions select one common width, one smooth filled coordinate family, and one core-preserving metric. This is the analytic part of finite transfer; the geometric disk and period constructions are separate inputs here.

theorem OAI.CircleDomainRigidity.FiniteTransfer.IsFilledCoordinateFamily.eventuallyEq_near_set line 22
theorem OAI.CircleDomainRigidity.FiniteTransfer.cutoffStaircase_eventuallyEq_original line 32

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_filled_family_and_metric_at_good_width line 43

Source documentation

Choose the same late width for the collar fillings and energy budget. The output coordinates and metric agree with the originals near the core.

theorem exists_filled_family_and_metric_at_good_width
    {I : Type*} [Fintype I] {n : ℕ}
    (D : I → Set (ℝ × ℝ)) (hD : ∀ i, IsOpen (D i))
    {Ω Q K U : Set (ℝ × ℝ)} (hΩ : IsOpen Ω) (hQ : IsCompact Q) (hQΩ : Q ⊆ Ω)
    (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U)
    (hKD : ∀ x ∈ K, ∀ i, x ∉ D i)
    (v : ℝ → Fin n → (ℝ × ℝ) → ℝ) (u : Fin n → (ℝ × ℝ) → ℝ)
    (hretain : ∀ δ, ∀ᶠ x in 𝓝ˢ K, ∀ i, v δ i x = u i x)
    {h : ℝ} (hh : 0 < h)
    (hfill : ∀ᶠ δ : ℝ in 𝓝[>] 0, ∃ F : Fin n → (ℝ × ℝ) → ℝ,
      IsFilledCoordinateFamily D Ω (v δ) F)
    (hvi : ∀ k, IntegrableOn
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.IsFilledCoordinateFamily