OAI/Analysis/CircleDomains/Transfer/ModelRealTerminals.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Actual boundary oscillation control for the preserved real barriers of a mixed model.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.ModelRealSubfamily.terminal_value line 20
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.ModelRealSubfamily.terminal_oscillation line 37