TransportedTerminalBranches.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Cluster oscillation of transported terminal branches

The finite model's actual inverse transports a real branch near a physical terminal. All its cluster values at the assigned complementary component come from the physical boundary. Thus the physical square-sum oscillation estimate survives uniformization without a boundary-extension hypothesis.

def OAI.CircleDomainRigidity.componentClusterValues line 25
Source documentation
Finite real cluster values approached from the domain at a component.
```
def componentClusterValues (V : Set Sphere) (p : Sphere) (v : Sphere → ℝ) : Set ℝ :=
…
```
Mentions: OAI.CircleDomainRigidity.Sphere
theorem OAI.CircleDomainRigidity.TerminalComponentAssignment.cluster_values_subset_boundary line 30
def OAI.CircleDomainRigidity.sphereRealFunction line 54
Source documentation
A real-coordinate function, with an arbitrary unused value at infinity.
```
def sphereRealFunction {Y : Type*} (w : (ℝ × ℝ) → Y) (p : Sphere) : Y :=
…
```
Mentions: OAI.CircleDomainRigidity.Sphere
theorem OAI.CircleDomainRigidity.continuousAt_sphereRealFunction line 57
theorem OAI.CircleDomainRigidity.sphere_branch_of_real_branch line 69
theorem OAI.CircleDomainRigidity.TerminalComponentAssignment.real_cluster_diameter_le line 84
theorem OAI.CircleDomainRigidity.TerminalComponentAssignment.transported_branch_eventually line 110
theorem OAI.CircleDomainRigidity.TerminalComponentAssignment.real_cluster_excess_le line 123
theorem OAI.CircleDomainRigidity.TerminalComponentAssignment.real_transported_branch_eventually line 143