OAI/Analysis/Daugavet/ExactModuli.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ExactModuli.no_equivalent_auc line 16

   Source documentation

   The renorming obstruction is a consequence of the weak-neighborhood geometry, not merely of the vanishing inherited-norm one-sided modulus.

   theorem no_equivalent_auc (hinf : ¬ FiniteDimensional ℝ X) (hsp : UnitSliceProperty X)
       (N : Seminorm ℝ X) (hN : EquivalentNorm N) : ¬ AUC N := by
   …

   Mentions: OAI.ExactModuli.UnitSliceProperty, OAI.ExactModuli.EquivalentNorm, OAI.ExactModuli.AUC

2. theorem OAI.ExactModuli.exact_main line 42

   Distinct definitions of this name: ComparatorChallenges/DaugavetModuli.lean:72 (same statement text; different proof or body). Qualify references as OAI.ExactModuli.exact_main@path.