OAI/Geometry/RCD/Harmonic/CompactRecoveryCoefficient.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform compact-test recovery preserves the original mixed pairing

  1. theorem OAI.RegularPointCoordinates.compact_recovery_coefficient line 15