Multilinear interpolation

Blueprint Summary🔗

Overview
Total entries76completed: 53; deps incomplete: 6; sorries: 15; no proof: 0
Ready now15Entries with an actionable next formalization step.
Fully closed53Local code and prerequisite closure are both complete.
Actionable priorities6Entries ready now and already unlocking downstream work.
Current blockers15Missing external or incomplete Lean declarations.
Missing informal coverage50Entries with Lean code but missing an informal statement or proof block.
Actionable priorities (6)
Current blockers (15)
Missing informal coverage (50)
Entry index (76)
Definitions29completed: 20; deps incomplete: 1; sorries: 6; no proof: 0
Theorems47completed: 33; deps incomplete: 5; sorries: 9; no proof: 0
Lean-only entries9
Informal-only entries2
Definition Index (29)
Theorem / Proposition / Lemma / Corollary Index (47)
Dependency insights
Statement-used entries20Entries reused in statement dependencies.
Proof-used entries47Entries reused in proof-only dependencies.
Most used in statements (20)
  • EQuasinorm(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 50proof uses: 10direct uses: 60downstream unlocks: 60
    Associated lean decls (1)
  • «EQuasinorm.Couple»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 22proof uses: 1direct uses: 23downstream unlocks: 23
    Associated lean decls (1)
  • «Modulus.IsDecomposable»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 17proof uses: 0direct uses: 17downstream unlocks: 17
    Associated lean decls (1)
    • Modulus.IsDecomposable
  • «EQuasinorm.kNorm»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 11proof uses: 5direct uses: 16downstream unlocks: 28
    Associated lean decls (1)
  • «EQuasinorm.discretePhiFunctional»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 11proof uses: 7direct uses: 18downstream unlocks: 25
    Associated lean decls (1)
  • MultisubadditiveMap(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 11proof uses: 0direct uses: 11downstream unlocks: 11
    Associated lean decls (1)
  • «EQuasinorm.instMin»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 8proof uses: 1direct uses: 9downstream unlocks: 10
    Associated lean decls (1)
  • «EQuasinorm.jNorm»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 7proof uses: 6direct uses: 13downstream unlocks: 25
    Associated lean decls (1)
  • jInfNorm(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 11
    Associated lean decls (1)
  • «EQuasinorm.kMethod»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 7proof uses: 1direct uses: 8downstream unlocks: 10
    Associated lean decls (1)
  • Show all 10 more statement-used entries
    • «EQuasinorm.discreteKMethod»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 10
      Associated lean decls (1)
    • ESeminorm(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 6
      Associated lean decls (1)
    • Ω(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 6
      Associated lean decls (1)
    • boundaryError(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 4proof uses: 1direct uses: 5downstream unlocks: 10
      Associated lean decls (1)
    • «MultisubadditiveMap.IsBoundedForOn»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 1direct uses: 3downstream unlocks: 8
      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)
    • «EQuasinorm.eLorentz»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 1direct uses: 2downstream 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)
    • «EQuasinorm.ofModulus»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
      Associated lean decls (1)
Most used in proofs (47)
Metadata
Metadata audit
Missing owner76
Missing effort76
Untagged76
Missing owner (76)
Missing effort (76)
Untagged (76)
Structure and coverage
Informal-only2Statements with no associated Lean code yet.
Ready to formalize15Entries with an actionable next formalization step.
Formalized, ancestors open6Local Lean work is done, but prerequisite closure is still open.
Fully closed53Local code and ancestor closure are both complete.
Blocked or incomplete2Entries not covered by the highlighted readiness buckets above.
Heaviest prerequisites (69)
No prerequisites (7)
No dependents (19)