BoundaryTrace.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Unique traces outside the countable band support

For a bounded real coordinate the interval band is the actual interval between the lower and upper boundary limits. A zero band budget forces these limits to agree and gives convergence from the physical domain. Square summability of the budgets makes all exceptions countable.

def OAI.CircleDomainRigidity.realBoundaryTrace line 20
theorem OAI.CircleDomainRigidity.tendsto_boundaryTrace_of_zero_band line 23
theorem OAI.CircleDomainRigidity.countable_band_support line 40

theorem OAI.CircleDomainRigidity.boundaryTrace_outside_countable_set line 46

Source documentation

The coordinate has a genuine limiting trace at every point of the dust except for a countable set explicitly given by its nonzero budget.

theorem boundaryTrace_outside_countable_set
    {X : Type*} [TopologicalSpace X] {G B : Set X} {f a : X → ℝ} {M : ℝ}
    (hM : ∀ y ∈ G, |f y| ≤ M) (hB : B ⊆ closure G)
    (ha : Summable (fun x => a x ^ 2))
    (hband : ∀ x ∈ B, limsup f (𝓝[G] x) - liminf f (𝓝[G] x) ≤ a x) :
    ∃ S : Set X, S.Countable ∧ ∀ x ∈ B \ S,
      Tendsto f (𝓝[G] x) (𝓝 (realBoundaryTrace G f x)) := by
…

Mentions: OAI.CircleDomainRigidity.realBoundaryTrace