OAI/Analysis/CircleDomains/Topology/ModelCompactTransport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Compact target scalars have finite source L2 norm even when their values do not descend across the source dust. This permits transport of the actual vertical error, which need not be constant on holes.

  1. theorem OAI.CircleDomainRigidity.CompactScalarModel.source_bounded_over_compact_target line 19
  2. theorem OAI.CircleDomainRigidity.CompactScalarModel.compact_target_pullback_memLp line 40
  3. theorem OAI.CircleDomainRigidity.CompactScalarModel.compact_target_pullback_energy line 75