OAI/Analysis/LipschitzFree/Renorming.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Equivalent complete norms on real ℓ¹ with quantitative BAP obstructions

  1. theorem OAI.DiscreteFree.hasBAP_of_linearIsometryEquiv line 17
  2. theorem OAI.DiscreteFree.hasBAP_linearIsometryEquiv_iff line 27
  3. theorem OAI.DiscreteFree.real_l1_quantitative_renorming line 41

    Distinct definitions of this name: ComparatorChallenges/RealL1Renorming.lean:48 (same statement text; different proof or body). Qualify references as OAI.DiscreteFree.real_l1_quantitative_renorming@path.