OAI/Geometry/RCD/Harmonic/ScaledHarmonicValueConvergence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Scalar multiplication of the actual local Sobolev value convergence

  1. theorem OAI.RegularPointCoordinates.sobolev_linear_value_convergence_smul line 14