rmuzzar / repulsive-curves-python Star 0 Code Issues Pull requests Python implementation of algorithms from the paper "Repulsive Curves" by Yu, Schumacher, and Crane. python curves simulation computational-geometry gradient-descent preconditioning geometric-computing sobolev-spaces Updated Apr 24, 2026 Python
abenenson / rellich-kondrachov Star 0 Code Issues Pull requests Lean 4 proof of Rellich–Kondrachov: the H¹ to L² Sobolev embedding is compact on compact Riemannian manifolds. theorem-proving formalization functional-analysis mathlib riemannian-geometry lean4 sobolev-spaces Updated May 14, 2026 Lean
Brsanch / sqg-lean-proofs Star 0 Code Issues Pull requests Lean 4 + mathlib formalization of the SQG shear-vorticity identity (D14 Theorem 1) theorem-proving partial-differential-equations formalization fluid-dynamics mathematical-physics mathlib harmonic-analysis regularity-theory sqg lean4 quasi-geostrophic sobolev-spaces Updated Jul 5, 2026 Lean
Brsanch / sqg-lean-proofs-fourier Star 0 Code Issues Pull requests Classical Fourier analysis in Lean 4: Littlewood–Paley, paraproducts, Kato–Ponce commutator, Sobolev embeddings for 𝕋². Upstream of sqg-lean-proofs and future NS/Euler/MHD formalizations. theorem-proving partial-differential-equations formalization fourier-analysis mathematical-physics mathlib harmonic-analysis lean4 sobolev-spaces littlewood-paley paraproducts kato-ponce Updated Jul 5, 2026 Lean