OAI/Analysis/CircleDomains/Transfer/ModelHorizontalApproximation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Construct the actual continuous horizontal priority coordinate with any prescribed L2 error and prescribed neighborhoods of the source ends.

  1. theorem OAI.CircleDomainRigidity.CompactScalarModel.exists_horizontal_priority_approximation line 16