OAI/Geometry/RCD/Harmonic/CompactMixedTransfer.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Strong local harmonic recovery transfers a compact-test mixed pairing

  1. theorem OAI.RegularPointCoordinates.gamma_sub_right line 13

    Distinct definitions of this name: OAI/Geometry/RCD/Sobolev/QuadraticGradientComparison.lean:24 (different declaration text). Qualify references as OAI.RegularPointCoordinates.gamma_sub_right@path.

  2. theorem OAI.RegularPointCoordinates.compact_mixed_transfer line 20