lean liquid::droplet:液体张量实验 源码

液体张量实验 有关Peter Scholze的同名博客文章:请参阅 。 该项目的目的是将Scholze-Clausen, 定理9.4形式化。 该声明 该语句可以在找到 theorem first_target [BD.suitable c'] (r r' : R≥ 0 ) [fact ( 0 < r)] [fact ( 0 < r')] [fact (r < r')] [fact (r' ≤ 1 )] : ∀ m : N, ∃ (k : R≥ 0 ) [fact ( 1 ≤ k)], ∃ c0 : R≥ 0 , ∀ (S : Type ) [fintype S], ∀ (V : NormedGroup) [normed_with_aut r V],​ (Mbar_system V S r r' BD c').is_bounded_exact k m c0