OAI/Analysis/CircleDomains/Transfer/ScalarModelPostcomposition.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Postcomposition of actual scalar models. The scalar witnesses and their zero complementary gradients follow from the published chain rule and null-set preservation. The topological data are transported explicitly.

  1. theorem OAI.CircleDomainRigidity.extendAtInfinity_postcompose line 15
  2. theorem OAI.CircleDomainRigidity.physicalPlaneDomain_homeomorph_image line 20
  3. def OAI.CircleDomainRigidity.CompactScalarModel.postcomposeWithScalarTransport line 34
  4. def OAI.CircleDomainRigidity.CompactScalarModel.postcompose line 123
  5. theorem OAI.CircleDomainRigidity.CompactScalarModel.postcompose_coefficient line 137