OAI/Analysis/CircleDomains/Rigidity/TracePrimitiveContinuity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Joint continuity of finite primitives follows from the explicit finite variation bound. Uniformly small scalar tails then prove the continuity of the actual infinite masked scalar at a common point.

  1. theorem OAI.CircleDomainRigidity.finiteTracePrimitive_continuous line 13
  2. theorem OAI.CircleDomainRigidity.infinite_masked_scalar_continuousAt line 40