OAI/Analysis/StructuralCrouzeix/Model.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Intrinsic domains, optimal similarities and matrix-valued boundary representations.

  1. def OAI.StructuralCrouzeix.RegularAnalyticBoundaryAt line 20

    Also declared: ComparatorChallenges/StructuralCrouzeix.lean:141 (same declaration text).

  2. structure OAI.StructuralCrouzeix.IsAdmissible line 24

    Also declared: ComparatorChallenges/StructuralCrouzeix.lean:145 (same declaration text).

  3. def OAI.StructuralCrouzeix.IsMinimizing line 32

    Also declared: ComparatorChallenges/StructuralCrouzeix.lean:153 (same declaration text).

  4. def OAI.StructuralCrouzeix.StrictlyFeasible line 38

    Also declared: ComparatorChallenges/StructuralCrouzeix.lean:159 (same declaration text).

  5. def OAI.StructuralCrouzeix.analyticSupNorm line 44

    Also declared: ComparatorChallenges/StructuralCrouzeix.lean:165 (same declaration text).

  6. def OAI.StructuralCrouzeix.boundaryPoint line 48

    Also declared: ComparatorChallenges/StructuralCrouzeix.lean:169 (same declaration text).

  7. def OAI.StructuralCrouzeix.FullEndpoint line 51

    Also declared: ComparatorChallenges/StructuralCrouzeix.lean:172 (same declaration text).