Zulip Chat Archive

Stream: condensed mathematics

Topic: statement


Johan Commelin (May 31 2021 at 14:49):

I just pushed a new file src/statement.lean that contains only

-- some imports

variables (BD : breen_deligne.package)
variables (c_ :   0)
variables (r r' : 0)
variables [fact (0 < r)] [fact (0 < r')] [fact (r < r')] [fact (r < 1)] [fact (r' < 1)]
variables [BD.data.very_suitable r r' c_] [ (i : ), fact (0 < c_ i)]

include BD c_ r'

def first_target_stmt : Prop :=
   m : ,
   (k K : 0) [fact (1  k)],
   c₀ : 0,
   (S : Type) [fintype S],
   (V : SemiNormedGroup.{0}) [normed_with_aut r V],
    ((BD.data.system c_ r V r').obj (op $ of r' (Mbar r' S))).is_weak_bounded_exact k K m c₀

Johan Commelin (May 31 2021 at 14:50):

The file src/liquid.lean now also contains

example (r r' : 0)
  [fact (0 < r)] [fact (0 < r')] [fact (r < r')] [fact (r < 1)] [fact (r' < 1)]
  [BD.data.very_suitable r r' c_] [ (i : ), fact (0 < c_ i)] :
  first_target_stmt BD c_ r r' :=
first_target BD c_ r r'

Johan Commelin (May 31 2021 at 14:51):

One of our goals can now be to make sure that (i) the project keeps compiling sorry-free, as it does now, and (ii) src/statement.lean imports as few lines of code as possible.

Johan Commelin (May 31 2021 at 14:51):

Working on (ii) will probably require splitting some files into pieces.

Johan Commelin (May 31 2021 at 14:53):

The imports currently are:

import pseudo_normed_group.system_of_complexes
import Mbar.pseudo_normed_group
import breen_deligne.homotopy

Last updated: Dec 20 2023 at 11:08 UTC