OAI/Analysis/CircleDomains/Probability/LawRealBandTagNull.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Application of the local tag proof to a physical path law. The inverse-chart bound and the finite payment measure are constructed from the quotient neighborhood, the differential energy and the law's density.

  1. theorem OAI.CircleDomainRigidity.ae_parameter_real_band_tag_null_trace line 23