OAI/Analysis/CircleDomains/Probability/FiniteLevelNullImage.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A zero weighted trace on a compact locally connected finite-length level has null scalar image. The weight and all oscillations come from the actual smooth approximations, not from a null-image hypothesis.

  1. theorem OAI.CircleDomainRigidity.finite_level_null_image_of_approximation line 15