Multilinear interpolation

Blueprint Summary🔗

Overview
Total entries43completed: 23; deps incomplete: 0; sorries: 18; no proof: 0
Ready now18Entries with an actionable next formalization step.
Fully closed23Local code and prerequisite closure are both complete.
Actionable priorities7Entries ready now and already unlocking downstream work.
Current blockers18Missing external or incomplete Lean declarations.
Missing informal coverage12Entries with Lean code but missing an informal statement or proof block.
Actionable priorities (7)
Current blockers (18)
Missing informal coverage (12)
Entry index (43)
Definitions26completed: 16; deps incomplete: 0; sorries: 8; no proof: 0
Theorems17completed: 7; deps incomplete: 0; sorries: 10; no proof: 0
Informal-only entries2
Definition Index (26)
Theorem / Proposition / Lemma / Corollary Index (17)
Dependency insights
Statement-used entries15Entries reused in statement dependencies.
Proof-used entries14Entries reused in proof-only dependencies.
Most used in statements (15)
  • EQuasinorm(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 22proof uses: 4direct uses: 26downstream unlocks: 37
    Associated lean decls (1)
  • MultisubadditiveMap(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 9proof uses: 0direct uses: 9downstream unlocks: 9
    Associated lean decls (1)
  • «EQuasinorm.Couple»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 8proof uses: 1direct uses: 9downstream unlocks: 10
    Associated lean decls (1)
  • ESeminorm(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 6
    Associated lean decls (1)
  • Ω(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 4
    Associated lean decls (1)
  • «EQuasinorm.kNorm»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 3proof uses: 3direct uses: 6downstream unlocks: 10
    Associated lean decls (1)
  • «MultisubadditiveMap.IsBoundedFor»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 2proof uses: 1direct uses: 3downstream unlocks: 6
    Associated lean decls (1)
  • «EQuasinorm.discreteKMethod»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
    Associated lean decls (1)
  • «EQuasinorm.kMethod»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
    Associated lean decls (1)
  • «EQuasinorm.pow»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
    Associated lean decls (1)
  • Show all 5 more statement-used entries
    • «EQuasinorm.jNorm»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 2direct uses: 3downstream unlocks: 4
      Associated lean decls (1)
    • «EQuasinorm.eLorentz»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 2
      Associated lean decls (1)
    • jInfNorm(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
      Associated lean decls (1)
    • «EQuasinorm.aokiRolewicz»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
      Associated lean decls (1)
    • «EQuasinorm.eLorentzCouple»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
      Associated lean decls (1)
Most used in proofs (14)
Metadata
Metadata audit
Missing owner43
Missing effort43
Untagged43
Missing owner (43)
Missing effort (43)
Untagged (43)
Structure and coverage
Informal-only2Statements with no associated Lean code yet.
Ready to formalize18Entries with an actionable next formalization step.
Fully closed23Local code and ancestor closure are both complete.
Blocked or incomplete2Entries not covered by the highlighted readiness buckets above.
Heaviest prerequisites (37)
No prerequisites (6)
No dependents (20)