OAI/Analysis/LipschitzFree/RenormingModel.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Quantitative renorming of real ℓ¹ with fixed vector-space operations

  1. def OAI.DiscreteFree.HasBAP line 18

    Also declared: ComparatorChallenges/DiscreteLipschitzFree.lean:132 (same declaration text), ComparatorChallenges/RealL1Renorming.lean:19 (same declaration text).

  2. def OAI.DiscreteFree.blockBound line 23

    Distinct definitions of this name: ComparatorChallenges/DiscreteLipschitzFree.lean:137 (same declaration text), ComparatorChallenges/RealL1Renorming.lean:24 (same statement text; different proof or body). Qualify references as OAI.DiscreteFree.blockBound@path.

  3. def OAI.DiscreteFree.RealL1 line 33

    Also declared: ComparatorChallenges/RealL1Renorming.lean:28 (same declaration text).

  4. instance OAI.DiscreteFree.(instance at line 35) line 35
  5. instance OAI.DiscreteFree.(instance at line 38) line 38
  6. def OAI.DiscreteFree.RealL1RenormingStatement line 41

    Also declared: ComparatorChallenges/RealL1Renorming.lean:36 (same declaration text).