OAI/Analysis/CircleDomains/Modulus/WeightedScalarTests.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Compact planar tests are legitimate dual tests for spherical L² after dividing by the explicit positive stereographic area density.

  1. def OAI.CircleDomainRigidity.weightedScalarTest line 13
  2. theorem OAI.CircleDomainRigidity.weightedScalarTest_continuous line 15
  3. theorem OAI.CircleDomainRigidity.weightedScalarTest_compact line 19
  4. theorem OAI.CircleDomainRigidity.weightedScalarTest_memLp line 24
  5. theorem OAI.CircleDomainRigidity.integral_weightedScalarTest line 28
  6. theorem OAI.CircleDomainRigidity.tendsto_pairings_with_memLp_test line 41
  7. theorem OAI.CircleDomainRigidity.tendsto_planar_pairings_of_spherical line 52