OAI/Analysis/CircleDomains/Probability/GatePenaltyDensity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compactly many forbidden gate hits admit a bounded penalty density in a safe relatively compact domain region. Adding it preserves finite energy and leaves the original density unchanged outside that region.

  1. theorem OAI.CircleDomainRigidity.exists_gate_penalty_density line 25