Infinite-dimensional operator ridgelet transform

Blueprint Summary🔗

Overview

Total entries78completed: 78; deps incomplete: 0; sorries: 0; no proof: 0

Ready now0Entries with an actionable next formalization step.

Fully closed78Local code and prerequisite closure are both complete.

Actionable priorities0Entries ready now and already unlocking downstream work.

Missing informal coverage3Entries with Lean code but missing an informal statement or proof block.

Missing informal coverage (3)

«roadmap:trace-and-determinant»(Theorem)
Associated lean decls (2)
- OperatorRidgelet.traceOf_eq_traceAlong
- OperatorRidgelet.fredholmDet_eq_fredholmDetAlong
«roadmap:gaussian-layers»(Theorem)
Associated lean decls (1)
- OperatorRidgelet.exists_isCenteredGaussianLayers
«roadmap:polar-decomposition»(Theorem)
Associated lean decls (4)

Entry index (78)

Definitions22completed: 22; deps incomplete: 0; sorries: 0; no proof: 0

Propositions3completed: 3; deps incomplete: 0; sorries: 0; no proof: 0

Lemmas24completed: 24; deps incomplete: 0; sorries: 0; no proof: 0

Theorems13completed: 13; deps incomplete: 0; sorries: 0; no proof: 0

Corollaries7completed: 7; deps incomplete: 0; sorries: 0; no proof: 0

Examples9completed: 9; deps incomplete: 0; sorries: 0; no proof: 0

Definition Index (22)

«aux:trace-class-operators»(Definition)
Associated lean decls (9)
«aux:tempered-distributions»(Definition)
Associated lean decls (5)
«def:3.7»(Definition)
Associated lean decls (4)
«def:3.10»(Definition)
Associated lean decls (5)
«def:2.1»(Definition)
Associated lean decls (1)
- OperatorRidgelet.finiteNetwork
«aux:sampling-data»(Definition)
Associated lean decls (9)
«def:6.1»(Definition)
Associated lean decls (8)
«def:2.2»(Definition)
Associated lean decls (5)
«aux:gaussian-mixture»(Definition)
Associated lean decls (4)
«aux:centered-gaussian»(Definition)
Associated lean decls (2)
- OperatorRidgelet.IsTraceClassCovariance
- OperatorRidgelet.IsCenteredGaussian
«aux:gaussian-target»(Definition)
Associated lean decls (13)
«aux:frame-operator»(Definition)
Associated lean decls (9)
«aux:cylindrical»(Definition)
Associated lean decls (5)
«def:3.4»(Definition)
Associated lean decls (3)
«aux:tempered-activation»(Definition)
Associated lean decls (3)
«aux:relu-identities»(Definition)
Associated lean decls (4)
«def:4.2»(Definition)
Associated lean decls (6)
«aux:vector-valued»(Definition)
Associated lean decls (27)
«def:5.3»(Definition)
Associated lean decls (14)
«aux:finite-dim»(Definition)
Associated lean decls (8)
«aux:conventions»(Definition)
Associated lean decls (5)
«def:3.3»(Definition)
Associated lean decls (5)

Theorem / Proposition / Lemma / Corollary / Example Index (56)

«lem:6.7»(Lemma)
Associated lean decls (1)
- OperatorRidgelet.Paper.lem_6_7
«roadmap:trace-and-determinant»(Theorem)
Associated lean decls (2)
- OperatorRidgelet.traceOf_eq_traceAlong
- OperatorRidgelet.fredholmDet_eq_fredholmDetAlong
«lem:4.4»(Lemma)
Associated lean decls (5)
«lem:7.1»(Lemma)
Associated lean decls (2)
- OperatorRidgelet.Paper.lem_7_1_i
- OperatorRidgelet.Paper.lem_7_1_ii
«cor:C.2»(Corollary)
Associated lean decls (2)
- OperatorRidgelet.Paper.cor_C_2_i
- OperatorRidgelet.Paper.cor_C_2_ii
«lem:4.1»(Lemma)
Associated lean decls (3)
«lem:5.8»(Lemma)
Associated lean decls (9)
«lem:6.4»(Lemma)
Associated lean decls (1)
- OperatorRidgelet.Paper.lem_6_4
«ex:5.6»(Example)
Associated lean decls (16)
«thm:4.8»(Theorem)
Associated lean decls (18)
«prop:5.12»(Proposition)
Associated lean decls (13)
«thm:6.5»(Theorem)
Associated lean decls (3)
«lem:5.9»(Lemma)
Associated lean decls (5)
«lem:3.1»(Lemma)
Associated lean decls (4)
«thm:5.10»(Theorem)
Associated lean decls (5)
«cor:6.10»(Corollary)
Associated lean decls (5)
«lem:5.1»(Lemma)
Associated lean decls (10)
«lem:A.1»(Lemma)
Associated lean decls (4)
«lem:3.12»(Lemma)
Associated lean decls (2)
- OperatorRidgelet.Paper.lem_3_12_i
- OperatorRidgelet.Paper.lem_3_12_ii
«ex:3.15»(Example)
Associated lean decls (14)
«cor:C.1»(Corollary)
Associated lean decls (1)
- OperatorRidgelet.Paper.cor_C_1
«ex:7.4»(Example)
Associated lean decls (11)
«ex:7.2»(Example)
Associated lean decls (11)
«thm:3.14»(Theorem)
Associated lean decls (7)
«lem:4.3»(Lemma)
Associated lean decls (5)
«lem:6.9»(Lemma)
Associated lean decls (3)
«lem:3.9»(Lemma)
Associated lean decls (6)
«prop:B.1»(Proposition)
Associated lean decls (9)
«lem:3.6»(Lemma)
Associated lean decls (2)
- OperatorRidgelet.Paper.lem_3_6
- OperatorRidgelet.Paper.lem_3_6_uniqueness
«roadmap:gaussian-layers»(Theorem)
Associated lean decls (1)
- OperatorRidgelet.exists_isCenteredGaussianLayers
«thm:5.4»(Theorem)
Associated lean decls (6)
«roadmap:polar-decomposition»(Theorem)
Associated lean decls (4)
«thm:6.8»(Theorem)
Associated lean decls (3)
«lem:6.2»(Lemma)
Associated lean decls (2)
- OperatorRidgelet.Paper.lem_6_2_i
- OperatorRidgelet.Paper.lem_6_2_ii
«ex:7.9»(Example)
Associated lean decls (24)
«lem:3.11»(Lemma)
Associated lean decls (3)
«lem:4.6»(Lemma)
Associated lean decls (2)
- OperatorRidgelet.Paper.lem_4_6_i
- OperatorRidgelet.Paper.lem_4_6_ii
«cor:4.9»(Corollary)
Associated lean decls (4)
«lem:3.5»(Lemma)
Associated lean decls (5)
«cor:5.5»(Corollary)
Associated lean decls (11)
«thm:6.6»(Theorem)
Associated lean decls (5)
«lem:5.2»(Lemma)
Associated lean decls (17)
«ex:3.16»(Example)
Associated lean decls (8)
«cor:D.2»(Corollary)
Associated lean decls (6)
«lem:4.7»(Lemma)
Associated lean decls (10)
«ex:7.6»(Example)
Associated lean decls (37)
«ex:7.8»(Example)
Associated lean decls (26)
«prop:D.3»(Proposition)
Associated lean decls (5)
«ex:3.13»(Example)
Associated lean decls (5)
«lem:3.8»(Lemma)
Associated lean decls (6)
«cor:7.5»(Corollary)
Associated lean decls (1)
- OperatorRidgelet.Paper.cor_7_5
«thm:6.3»(Theorem)
Associated lean decls (1)
- OperatorRidgelet.Paper.thm_6_3
«lem:7.3»(Lemma)
Associated lean decls (3)
«thm:4.5»(Theorem)
Associated lean decls (11)
«lem:3.2»(Lemma)
Associated lean decls (6)
«thm:4.11»(Theorem)
Associated lean decls (35)

Dependency insights

Statement-used entries37Entries reused in statement dependencies.

Proof-used entries34Entries reused in proof-only dependencies.

Most used in statements (37)

«aux:conventions»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 16proof uses: 0direct uses: 16downstream unlocks: 52
Associated lean decls (5)
«aux:centered-gaussian»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 14proof uses: 0direct uses: 14downstream unlocks: 48
Associated lean decls (2)
- OperatorRidgelet.IsTraceClassCovariance
- OperatorRidgelet.IsCenteredGaussian
«def:3.3»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 11proof uses: 0direct uses: 11downstream unlocks: 32
Associated lean decls (5)
«def:3.10»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 11proof uses: 0direct uses: 11downstream unlocks: 27
Associated lean decls (5)
«def:3.4»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 8proof uses: 0direct uses: 8downstream unlocks: 36
Associated lean decls (3)
«aux:gaussian-mixture»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 41
Associated lean decls (4)
«def:2.2»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 29
Associated lean decls (5)
«def:6.1»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 18
Associated lean decls (8)
«def:4.2»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 17
Associated lean decls (6)
«def:3.7»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 24
Associated lean decls (4)
Show all 27 more statement-used entries
- «aux:frame-operator»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 16
  Associated lean decls (9)
- «aux:sampling-data»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 13
  Associated lean decls (9)
- «aux:tempered-activation»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 12
  Associated lean decls (3)
- «aux:trace-class-operators»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 9
  Associated lean decls (9)
- «aux:gaussian-target»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 7
  Associated lean decls (13)
- «aux:cylindrical»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 6
  Associated lean decls (5)
- «thm:3.14»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 4direct uses: 7downstream unlocks: 17
  Associated lean decls (7)
- «lem:3.9»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 1direct uses: 4downstream unlocks: 14
  Associated lean decls (6)
- «thm:4.5»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 4direct uses: 7downstream unlocks: 11
  Associated lean decls (11)
- «thm:6.5»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 3direct uses: 6downstream unlocks: 10
  Associated lean decls (3)
- «aux:tempered-distributions»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 7
  Associated lean decls (5)
- «aux:relu-identities»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 6
  Associated lean decls (4)
- «roadmap:polar-decomposition»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 30
  Associated lean decls (4)
- «def:2.1»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 19
  Associated lean decls (1)
  - OperatorRidgelet.finiteNetwork
- «lem:4.7»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 1direct uses: 3downstream unlocks: 13
  Associated lean decls (10)
- «thm:4.8»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 4direct uses: 6downstream unlocks: 11
  Associated lean decls (18)
- «thm:6.6»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 2direct uses: 4downstream unlocks: 6
  Associated lean decls (5)
- «thm:5.4»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 1direct uses: 3downstream unlocks: 3
  Associated lean decls (6)
- «ex:7.6»(Example)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 2direct uses: 4downstream unlocks: 2
  Associated lean decls (37)
- «aux:finite-dim»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (8)
- «roadmap:gaussian-layers»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 42
  Associated lean decls (1)
  - OperatorRidgelet.exists_isCenteredGaussianLayers
- «lem:3.2»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 10direct uses: 11downstream unlocks: 28
  Associated lean decls (6)
- «lem:3.6»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 2direct uses: 3downstream unlocks: 15
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_3_6
  - OperatorRidgelet.Paper.lem_3_6_uniqueness
- «roadmap:trace-and-determinant»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 10
  Associated lean decls (2)
  - OperatorRidgelet.traceOf_eq_traceAlong
  - OperatorRidgelet.fredholmDet_eq_fredholmDetAlong
- «aux:vector-valued»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 5
  Associated lean decls (27)
- «def:5.3»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (14)
- «thm:5.10»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (5)

Most used in proofs (34)

«lem:3.2»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 10statement uses: 1direct uses: 11downstream unlocks: 28
Associated lean decls (6)
«lem:3.8»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 6statement uses: 0direct uses: 6downstream unlocks: 23
Associated lean decls (6)
«lem:3.1»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 4statement uses: 0direct uses: 4downstream unlocks: 31
Associated lean decls (4)
«lem:3.5»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 4statement uses: 0direct uses: 4downstream unlocks: 18
Associated lean decls (5)
«thm:3.14»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 4statement uses: 3direct uses: 7downstream unlocks: 17
Associated lean decls (7)
«thm:4.5»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 4statement uses: 3direct uses: 7downstream unlocks: 11
Associated lean decls (11)
«thm:4.8»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 4statement uses: 2direct uses: 6downstream unlocks: 11
Associated lean decls (18)
«lem:3.12»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 4statement uses: 0direct uses: 4downstream unlocks: 7
Associated lean decls (2)
- OperatorRidgelet.Paper.lem_3_12_i
- OperatorRidgelet.Paper.lem_3_12_ii
«lem:4.3»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 3statement uses: 0direct uses: 3downstream unlocks: 12
Associated lean decls (5)
«thm:6.5»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 3statement uses: 3direct uses: 6downstream unlocks: 10
Associated lean decls (3)
Show all 24 more proof-used entries
- «lem:4.4»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 3statement uses: 0direct uses: 3downstream unlocks: 5
  Associated lean decls (5)
- «lem:5.8»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 3statement uses: 0direct uses: 3downstream unlocks: 3
  Associated lean decls (9)
- «lem:3.11»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 18
  Associated lean decls (3)
- «lem:3.6»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 2statement uses: 1direct uses: 3downstream unlocks: 15
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_3_6
  - OperatorRidgelet.Paper.lem_3_6_uniqueness
- «lem:6.2»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 13
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_6_2_i
  - OperatorRidgelet.Paper.lem_6_2_ii
- «lem:4.1»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 12
  Associated lean decls (3)
- «thm:6.3»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 12
  Associated lean decls (1)
  - OperatorRidgelet.Paper.thm_6_3
- «thm:6.6»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 2statement uses: 2direct uses: 4downstream unlocks: 6
  Associated lean decls (5)
- «lem:7.3»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (3)
- «thm:4.11»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 4
  Associated lean decls (35)
- «ex:7.6»(Example)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 2statement uses: 2direct uses: 4downstream unlocks: 2
  Associated lean decls (37)
- «lem:3.9»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 3direct uses: 4downstream unlocks: 14
  Associated lean decls (6)
- «lem:4.7»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 2direct uses: 3downstream unlocks: 13
  Associated lean decls (10)
- «lem:4.6»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 12
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_4_6_i
  - OperatorRidgelet.Paper.lem_4_6_ii
- «lem:6.4»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 11
  Associated lean decls (1)
  - OperatorRidgelet.Paper.lem_6_4
- «lem:6.9»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (3)
- «thm:5.4»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 2direct uses: 3downstream unlocks: 3
  Associated lean decls (6)
- «cor:6.10»(Corollary)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (5)
- «lem:5.1»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (10)
- «lem:5.9»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (5)
- «ex:7.4»(Example)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (11)
- «lem:5.2»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (17)
- «lem:6.7»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - OperatorRidgelet.Paper.lem_6_7
- «lem:7.1»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_7_1_i
  - OperatorRidgelet.Paper.lem_7_1_ii

Metadata

Metadata audit

Missing owner78

Missing effort78

Untagged78

Missing owner (78)

«aux:centered-gaussian»(Definition)

Missing owner metadata.
Associated lean decls (2)
- OperatorRidgelet.IsTraceClassCovariance
- OperatorRidgelet.IsCenteredGaussian
«aux:conventions»(Definition)

Missing owner metadata.
Associated lean decls (5)
«aux:cylindrical»(Definition)

Missing owner metadata.
Associated lean decls (5)
«aux:finite-dim»(Definition)

Missing owner metadata.
Associated lean decls (8)
«aux:frame-operator»(Definition)

Missing owner metadata.
Associated lean decls (9)
«aux:gaussian-mixture»(Definition)

Missing owner metadata.
Associated lean decls (4)
«aux:gaussian-target»(Definition)

Missing owner metadata.
Associated lean decls (13)
«aux:relu-identities»(Definition)

Missing owner metadata.
Associated lean decls (4)
«aux:sampling-data»(Definition)

Missing owner metadata.
Associated lean decls (9)
«aux:tempered-activation»(Definition)

Missing owner metadata.
Associated lean decls (3)
Show all 68 more entries missing owner
- «aux:tempered-distributions»(Definition)
  
  Missing owner metadata.
  Associated lean decls (5)
- «aux:trace-class-operators»(Definition)
  
  Missing owner metadata.
  Associated lean decls (9)
- «aux:vector-valued»(Definition)
  
  Missing owner metadata.
  Associated lean decls (27)
- «cor:4.9»(Corollary)
  
  Missing owner metadata.
  Associated lean decls (4)
- «cor:5.5»(Corollary)
  
  Missing owner metadata.
  Associated lean decls (11)
- «cor:6.10»(Corollary)
  
  Missing owner metadata.
  Associated lean decls (5)
- «cor:7.5»(Corollary)
  
  Missing owner metadata.
  Associated lean decls (1)
  - OperatorRidgelet.Paper.cor_7_5
- «cor:C.1»(Corollary)
  
  Missing owner metadata.
  Associated lean decls (1)
  - OperatorRidgelet.Paper.cor_C_1
- «cor:C.2»(Corollary)
  
  Missing owner metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.cor_C_2_i
  - OperatorRidgelet.Paper.cor_C_2_ii
- «cor:D.2»(Corollary)
  
  Missing owner metadata.
  Associated lean decls (6)
- «def:2.1»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - OperatorRidgelet.finiteNetwork
- «def:2.2»(Definition)
  
  Missing owner metadata.
  Associated lean decls (5)
- «def:3.10»(Definition)
  
  Missing owner metadata.
  Associated lean decls (5)
- «def:3.3»(Definition)
  
  Missing owner metadata.
  Associated lean decls (5)
- «def:3.4»(Definition)
  
  Missing owner metadata.
  Associated lean decls (3)
- «def:3.7»(Definition)
  
  Missing owner metadata.
  Associated lean decls (4)
- «def:4.2»(Definition)
  
  Missing owner metadata.
  Associated lean decls (6)
- «def:5.3»(Definition)
  
  Missing owner metadata.
  Associated lean decls (14)
- «def:6.1»(Definition)
  
  Missing owner metadata.
  Associated lean decls (8)
- «ex:3.13»(Example)
  
  Missing owner metadata.
  Associated lean decls (5)
- «ex:3.15»(Example)
  
  Missing owner metadata.
  Associated lean decls (14)
- «ex:3.16»(Example)
  
  Missing owner metadata.
  Associated lean decls (8)
- «ex:5.6»(Example)
  
  Missing owner metadata.
  Associated lean decls (16)
- «ex:7.2»(Example)
  
  Missing owner metadata.
  Associated lean decls (11)
- «ex:7.4»(Example)
  
  Missing owner metadata.
  Associated lean decls (11)
- «ex:7.6»(Example)
  
  Missing owner metadata.
  Associated lean decls (37)
- «ex:7.8»(Example)
  
  Missing owner metadata.
  Associated lean decls (26)
- «ex:7.9»(Example)
  
  Missing owner metadata.
  Associated lean decls (24)
- «lem:3.11»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (3)
- «lem:3.12»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_3_12_i
  - OperatorRidgelet.Paper.lem_3_12_ii
- «lem:3.1»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (4)
- «lem:3.2»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (6)
- «lem:3.5»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (5)
- «lem:3.6»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_3_6
  - OperatorRidgelet.Paper.lem_3_6_uniqueness
- «lem:3.8»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (6)
- «lem:3.9»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (6)
- «lem:4.1»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (3)
- «lem:4.3»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (5)
- «lem:4.4»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (5)
- «lem:4.6»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_4_6_i
  - OperatorRidgelet.Paper.lem_4_6_ii
- «lem:4.7»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (10)
- «lem:5.1»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (10)
- «lem:5.2»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (17)
- «lem:5.8»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (9)
- «lem:5.9»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (5)
- «lem:6.2»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_6_2_i
  - OperatorRidgelet.Paper.lem_6_2_ii
- «lem:6.4»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - OperatorRidgelet.Paper.lem_6_4
- «lem:6.7»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - OperatorRidgelet.Paper.lem_6_7
- «lem:6.9»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (3)
- «lem:7.1»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_7_1_i
  - OperatorRidgelet.Paper.lem_7_1_ii
- «lem:7.3»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (3)
- «lem:A.1»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (4)
- «prop:5.12»(Proposition)
  
  Missing owner metadata.
  Associated lean decls (13)
- «prop:B.1»(Proposition)
  
  Missing owner metadata.
  Associated lean decls (9)
- «prop:D.3»(Proposition)
  
  Missing owner metadata.
  Associated lean decls (5)
- «roadmap:gaussian-layers»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - OperatorRidgelet.exists_isCenteredGaussianLayers
- «roadmap:polar-decomposition»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (4)
- «roadmap:trace-and-determinant»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - OperatorRidgelet.traceOf_eq_traceAlong
  - OperatorRidgelet.fredholmDet_eq_fredholmDetAlong
- «thm:3.14»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (7)
- «thm:4.11»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (35)
- «thm:4.5»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (11)
- «thm:4.8»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (18)
- «thm:5.10»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (5)
- «thm:5.4»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (6)
- «thm:6.3»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - OperatorRidgelet.Paper.thm_6_3
- «thm:6.5»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (3)
- «thm:6.6»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (5)
- «thm:6.8»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (3)

Missing effort (78)

«aux:centered-gaussian»(Definition)

Missing effort metadata.
Associated lean decls (2)
- OperatorRidgelet.IsTraceClassCovariance
- OperatorRidgelet.IsCenteredGaussian
«aux:conventions»(Definition)

Missing effort metadata.
Associated lean decls (5)
«aux:cylindrical»(Definition)

Missing effort metadata.
Associated lean decls (5)
«aux:finite-dim»(Definition)

Missing effort metadata.
Associated lean decls (8)
«aux:frame-operator»(Definition)

Missing effort metadata.
Associated lean decls (9)
«aux:gaussian-mixture»(Definition)

Missing effort metadata.
Associated lean decls (4)
«aux:gaussian-target»(Definition)

Missing effort metadata.
Associated lean decls (13)
«aux:relu-identities»(Definition)

Missing effort metadata.
Associated lean decls (4)
«aux:sampling-data»(Definition)

Missing effort metadata.
Associated lean decls (9)
«aux:tempered-activation»(Definition)

Missing effort metadata.
Associated lean decls (3)
Show all 68 more entries missing effort
- «aux:tempered-distributions»(Definition)
  
  Missing effort metadata.
  Associated lean decls (5)
- «aux:trace-class-operators»(Definition)
  
  Missing effort metadata.
  Associated lean decls (9)
- «aux:vector-valued»(Definition)
  
  Missing effort metadata.
  Associated lean decls (27)
- «cor:4.9»(Corollary)
  
  Missing effort metadata.
  Associated lean decls (4)
- «cor:5.5»(Corollary)
  
  Missing effort metadata.
  Associated lean decls (11)
- «cor:6.10»(Corollary)
  
  Missing effort metadata.
  Associated lean decls (5)
- «cor:7.5»(Corollary)
  
  Missing effort metadata.
  Associated lean decls (1)
  - OperatorRidgelet.Paper.cor_7_5
- «cor:C.1»(Corollary)
  
  Missing effort metadata.
  Associated lean decls (1)
  - OperatorRidgelet.Paper.cor_C_1
- «cor:C.2»(Corollary)
  
  Missing effort metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.cor_C_2_i
  - OperatorRidgelet.Paper.cor_C_2_ii
- «cor:D.2»(Corollary)
  
  Missing effort metadata.
  Associated lean decls (6)
- «def:2.1»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - OperatorRidgelet.finiteNetwork
- «def:2.2»(Definition)
  
  Missing effort metadata.
  Associated lean decls (5)
- «def:3.10»(Definition)
  
  Missing effort metadata.
  Associated lean decls (5)
- «def:3.3»(Definition)
  
  Missing effort metadata.
  Associated lean decls (5)
- «def:3.4»(Definition)
  
  Missing effort metadata.
  Associated lean decls (3)
- «def:3.7»(Definition)
  
  Missing effort metadata.
  Associated lean decls (4)
- «def:4.2»(Definition)
  
  Missing effort metadata.
  Associated lean decls (6)
- «def:5.3»(Definition)
  
  Missing effort metadata.
  Associated lean decls (14)
- «def:6.1»(Definition)
  
  Missing effort metadata.
  Associated lean decls (8)
- «ex:3.13»(Example)
  
  Missing effort metadata.
  Associated lean decls (5)
- «ex:3.15»(Example)
  
  Missing effort metadata.
  Associated lean decls (14)
- «ex:3.16»(Example)
  
  Missing effort metadata.
  Associated lean decls (8)
- «ex:5.6»(Example)
  
  Missing effort metadata.
  Associated lean decls (16)
- «ex:7.2»(Example)
  
  Missing effort metadata.
  Associated lean decls (11)
- «ex:7.4»(Example)
  
  Missing effort metadata.
  Associated lean decls (11)
- «ex:7.6»(Example)
  
  Missing effort metadata.
  Associated lean decls (37)
- «ex:7.8»(Example)
  
  Missing effort metadata.
  Associated lean decls (26)
- «ex:7.9»(Example)
  
  Missing effort metadata.
  Associated lean decls (24)
- «lem:3.11»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (3)
- «lem:3.12»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_3_12_i
  - OperatorRidgelet.Paper.lem_3_12_ii
- «lem:3.1»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (4)
- «lem:3.2»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (6)
- «lem:3.5»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (5)
- «lem:3.6»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_3_6
  - OperatorRidgelet.Paper.lem_3_6_uniqueness
- «lem:3.8»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (6)
- «lem:3.9»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (6)
- «lem:4.1»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (3)
- «lem:4.3»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (5)
- «lem:4.4»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (5)
- «lem:4.6»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_4_6_i
  - OperatorRidgelet.Paper.lem_4_6_ii
- «lem:4.7»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (10)
- «lem:5.1»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (10)
- «lem:5.2»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (17)
- «lem:5.8»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (9)
- «lem:5.9»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (5)
- «lem:6.2»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_6_2_i
  - OperatorRidgelet.Paper.lem_6_2_ii
- «lem:6.4»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - OperatorRidgelet.Paper.lem_6_4
- «lem:6.7»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - OperatorRidgelet.Paper.lem_6_7
- «lem:6.9»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (3)
- «lem:7.1»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_7_1_i
  - OperatorRidgelet.Paper.lem_7_1_ii
- «lem:7.3»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (3)
- «lem:A.1»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (4)
- «prop:5.12»(Proposition)
  
  Missing effort metadata.
  Associated lean decls (13)
- «prop:B.1»(Proposition)
  
  Missing effort metadata.
  Associated lean decls (9)
- «prop:D.3»(Proposition)
  
  Missing effort metadata.
  Associated lean decls (5)
- «roadmap:gaussian-layers»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - OperatorRidgelet.exists_isCenteredGaussianLayers
- «roadmap:polar-decomposition»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (4)
- «roadmap:trace-and-determinant»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - OperatorRidgelet.traceOf_eq_traceAlong
  - OperatorRidgelet.fredholmDet_eq_fredholmDetAlong
- «thm:3.14»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (7)
- «thm:4.11»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (35)
- «thm:4.5»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (11)
- «thm:4.8»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (18)
- «thm:5.10»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (5)
- «thm:5.4»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (6)
- «thm:6.3»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - OperatorRidgelet.Paper.thm_6_3
- «thm:6.5»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (3)
- «thm:6.6»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (5)
- «thm:6.8»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (3)

Untagged (78)

«aux:centered-gaussian»(Definition)

Missing tag metadata.
Associated lean decls (2)
- OperatorRidgelet.IsTraceClassCovariance
- OperatorRidgelet.IsCenteredGaussian
«aux:conventions»(Definition)

Missing tag metadata.
Associated lean decls (5)
«aux:cylindrical»(Definition)

Missing tag metadata.
Associated lean decls (5)
«aux:finite-dim»(Definition)

Missing tag metadata.
Associated lean decls (8)
«aux:frame-operator»(Definition)

Missing tag metadata.
Associated lean decls (9)
«aux:gaussian-mixture»(Definition)

Missing tag metadata.
Associated lean decls (4)
«aux:gaussian-target»(Definition)

Missing tag metadata.
Associated lean decls (13)
«aux:relu-identities»(Definition)

Missing tag metadata.
Associated lean decls (4)
«aux:sampling-data»(Definition)

Missing tag metadata.
Associated lean decls (9)
«aux:tempered-activation»(Definition)

Missing tag metadata.
Associated lean decls (3)
Show all 68 more untagged entries
- «aux:tempered-distributions»(Definition)
  
  Missing tag metadata.
  Associated lean decls (5)
- «aux:trace-class-operators»(Definition)
  
  Missing tag metadata.
  Associated lean decls (9)
- «aux:vector-valued»(Definition)
  
  Missing tag metadata.
  Associated lean decls (27)
- «cor:4.9»(Corollary)
  
  Missing tag metadata.
  Associated lean decls (4)
- «cor:5.5»(Corollary)
  
  Missing tag metadata.
  Associated lean decls (11)
- «cor:6.10»(Corollary)
  
  Missing tag metadata.
  Associated lean decls (5)
- «cor:7.5»(Corollary)
  
  Missing tag metadata.
  Associated lean decls (1)
  - OperatorRidgelet.Paper.cor_7_5
- «cor:C.1»(Corollary)
  
  Missing tag metadata.
  Associated lean decls (1)
  - OperatorRidgelet.Paper.cor_C_1
- «cor:C.2»(Corollary)
  
  Missing tag metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.cor_C_2_i
  - OperatorRidgelet.Paper.cor_C_2_ii
- «cor:D.2»(Corollary)
  
  Missing tag metadata.
  Associated lean decls (6)
- «def:2.1»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - OperatorRidgelet.finiteNetwork
- «def:2.2»(Definition)
  
  Missing tag metadata.
  Associated lean decls (5)
- «def:3.10»(Definition)
  
  Missing tag metadata.
  Associated lean decls (5)
- «def:3.3»(Definition)
  
  Missing tag metadata.
  Associated lean decls (5)
- «def:3.4»(Definition)
  
  Missing tag metadata.
  Associated lean decls (3)
- «def:3.7»(Definition)
  
  Missing tag metadata.
  Associated lean decls (4)
- «def:4.2»(Definition)
  
  Missing tag metadata.
  Associated lean decls (6)
- «def:5.3»(Definition)
  
  Missing tag metadata.
  Associated lean decls (14)
- «def:6.1»(Definition)
  
  Missing tag metadata.
  Associated lean decls (8)
- «ex:3.13»(Example)
  
  Missing tag metadata.
  Associated lean decls (5)
- «ex:3.15»(Example)
  
  Missing tag metadata.
  Associated lean decls (14)
- «ex:3.16»(Example)
  
  Missing tag metadata.
  Associated lean decls (8)
- «ex:5.6»(Example)
  
  Missing tag metadata.
  Associated lean decls (16)
- «ex:7.2»(Example)
  
  Missing tag metadata.
  Associated lean decls (11)
- «ex:7.4»(Example)
  
  Missing tag metadata.
  Associated lean decls (11)
- «ex:7.6»(Example)
  
  Missing tag metadata.
  Associated lean decls (37)
- «ex:7.8»(Example)
  
  Missing tag metadata.
  Associated lean decls (26)
- «ex:7.9»(Example)
  
  Missing tag metadata.
  Associated lean decls (24)
- «lem:3.11»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (3)
- «lem:3.12»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_3_12_i
  - OperatorRidgelet.Paper.lem_3_12_ii
- «lem:3.1»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (4)
- «lem:3.2»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (6)
- «lem:3.5»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (5)
- «lem:3.6»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_3_6
  - OperatorRidgelet.Paper.lem_3_6_uniqueness
- «lem:3.8»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (6)
- «lem:3.9»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (6)
- «lem:4.1»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (3)
- «lem:4.3»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (5)
- «lem:4.4»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (5)
- «lem:4.6»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_4_6_i
  - OperatorRidgelet.Paper.lem_4_6_ii
- «lem:4.7»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (10)
- «lem:5.1»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (10)
- «lem:5.2»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (17)
- «lem:5.8»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (9)
- «lem:5.9»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (5)
- «lem:6.2»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_6_2_i
  - OperatorRidgelet.Paper.lem_6_2_ii
- «lem:6.4»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - OperatorRidgelet.Paper.lem_6_4
- «lem:6.7»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - OperatorRidgelet.Paper.lem_6_7
- «lem:6.9»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (3)
- «lem:7.1»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_7_1_i
  - OperatorRidgelet.Paper.lem_7_1_ii
- «lem:7.3»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (3)
- «lem:A.1»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (4)
- «prop:5.12»(Proposition)
  
  Missing tag metadata.
  Associated lean decls (13)
- «prop:B.1»(Proposition)
  
  Missing tag metadata.
  Associated lean decls (9)
- «prop:D.3»(Proposition)
  
  Missing tag metadata.
  Associated lean decls (5)
- «roadmap:gaussian-layers»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - OperatorRidgelet.exists_isCenteredGaussianLayers
- «roadmap:polar-decomposition»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (4)
- «roadmap:trace-and-determinant»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - OperatorRidgelet.traceOf_eq_traceAlong
  - OperatorRidgelet.fredholmDet_eq_fredholmDetAlong
- «thm:3.14»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (7)
- «thm:4.11»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (35)
- «thm:4.5»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (11)
- «thm:4.8»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (18)
- «thm:5.10»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (5)
- «thm:5.4»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (6)
- «thm:6.3»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - OperatorRidgelet.Paper.thm_6_3
- «thm:6.5»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (3)
- «thm:6.6»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (5)
- «thm:6.8»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (3)

Structure and coverage

Fully closed78Local code and ancestor closure are both complete.

Heaviest prerequisites (72)

«ex:7.6»(Example)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 13statement deps: 6proof deps: 7direct uses: 4downstream unlocks: 2
Associated lean decls (37)
«thm:6.8»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 10statement deps: 4proof deps: 6direct uses: 0downstream unlocks: 0
Associated lean decls (3)
«ex:7.2»(Example)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 9statement deps: 2proof deps: 7direct uses: 0downstream unlocks: 0
Associated lean decls (11)
«thm:4.8»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 9statement deps: 4proof deps: 6direct uses: 6downstream unlocks: 11
Associated lean decls (18)
«thm:4.11»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 8statement deps: 4proof deps: 4direct uses: 2downstream unlocks: 4
Associated lean decls (35)
«thm:4.5»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 8statement deps: 4proof deps: 4direct uses: 7downstream unlocks: 11
Associated lean decls (11)
«thm:6.6»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 8statement deps: 4proof deps: 4direct uses: 4downstream unlocks: 6
Associated lean decls (5)
«thm:3.14»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 7statement deps: 3proof deps: 4direct uses: 7downstream unlocks: 17
Associated lean decls (7)
«prop:B.1»(Proposition)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 6statement deps: 3proof deps: 3direct uses: 0downstream unlocks: 0
Associated lean decls (9)
«aux:vector-valued»(Definition)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 6statement deps: 6proof deps: 0direct uses: 1downstream unlocks: 5
Associated lean decls (27)
Show all 62 more heaviest-prerequisite entries
- «cor:6.10»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 5statement deps: 2proof deps: 3direct uses: 1downstream unlocks: 3
  Associated lean decls (5)
- «thm:5.4»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 5statement deps: 2proof deps: 3direct uses: 3downstream unlocks: 3
  Associated lean decls (6)
- «lem:4.3»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 5statement deps: 3proof deps: 2direct uses: 3downstream unlocks: 12
  Associated lean decls (5)
- «ex:7.4»(Example)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 5statement deps: 4proof deps: 1direct uses: 1downstream unlocks: 1
  Associated lean decls (11)
- «cor:5.5»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (11)
- «def:5.3»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 5statement deps: 5proof deps: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (14)
- «cor:7.5»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 4statement deps: 2proof deps: 2direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - OperatorRidgelet.Paper.cor_7_5
- «cor:D.2»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 4statement deps: 2proof deps: 2direct uses: 0downstream unlocks: 0
  Associated lean decls (6)
- «thm:5.10»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 4statement deps: 2proof deps: 2direct uses: 1downstream unlocks: 1
  Associated lean decls (5)
- «ex:7.8»(Example)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 4statement deps: 4proof deps: 1direct uses: 0downstream unlocks: 0
  Associated lean decls (26)
- «ex:5.6»(Example)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 4statement deps: 3proof deps: 1direct uses: 0downstream unlocks: 0
  Associated lean decls (16)
- «prop:5.12»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 4statement deps: 3proof deps: 1direct uses: 0downstream unlocks: 0
  Associated lean decls (13)
- «lem:4.6»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 12
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_4_6_i
  - OperatorRidgelet.Paper.lem_4_6_ii
- «lem:3.9»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 2proof deps: 2direct uses: 4downstream unlocks: 14
  Associated lean decls (6)
- «cor:4.9»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 1proof deps: 2direct uses: 0downstream unlocks: 0
  Associated lean decls (4)
- «lem:4.4»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 1proof deps: 2direct uses: 3downstream unlocks: 5
  Associated lean decls (5)
- «lem:5.2»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 1proof deps: 2direct uses: 1downstream unlocks: 1
  Associated lean decls (17)
- «lem:A.1»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 1proof deps: 2direct uses: 0downstream unlocks: 0
  Associated lean decls (4)
- «thm:6.5»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 1proof deps: 2direct uses: 6downstream unlocks: 10
  Associated lean decls (3)
- «ex:7.9»(Example)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 1direct uses: 0downstream unlocks: 0
  Associated lean decls (24)
- «ex:3.13»(Example)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 2proof deps: 1direct uses: 0downstream unlocks: 0
  Associated lean decls (5)
- «lem:3.12»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 2proof deps: 1direct uses: 4downstream unlocks: 7
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_3_12_i
  - OperatorRidgelet.Paper.lem_3_12_ii
- «lem:3.2»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 2proof deps: 1direct uses: 11downstream unlocks: 28
  Associated lean decls (6)
- «thm:6.3»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 2proof deps: 1direct uses: 2downstream unlocks: 12
  Associated lean decls (1)
  - OperatorRidgelet.Paper.thm_6_3
- «aux:gaussian-target»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 4downstream unlocks: 7
  Associated lean decls (13)
- «def:3.4»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 8downstream unlocks: 36
  Associated lean decls (3)
- «def:3.7»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 6downstream unlocks: 24
  Associated lean decls (4)
- «def:4.2»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 7downstream unlocks: 17
  Associated lean decls (6)
- «def:6.1»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 7downstream unlocks: 18
  Associated lean decls (8)
- «lem:4.7»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 3downstream unlocks: 13
  Associated lean decls (10)
- «lem:6.7»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - OperatorRidgelet.Paper.lem_6_7
- «lem:3.11»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 1proof deps: 1direct uses: 2downstream unlocks: 18
  Associated lean decls (3)
- «lem:3.8»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 1proof deps: 1direct uses: 6downstream unlocks: 23
  Associated lean decls (6)
- «aux:frame-operator»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 6downstream unlocks: 16
  Associated lean decls (9)
- «aux:gaussian-mixture»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 7downstream unlocks: 41
  Associated lean decls (4)
- «aux:tempered-activation»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 5downstream unlocks: 12
  Associated lean decls (3)
- «aux:trace-class-operators»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 4downstream unlocks: 9
  Associated lean decls (9)
- «cor:C.1»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - OperatorRidgelet.Paper.cor_C_1
- «cor:C.2»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - OperatorRidgelet.Paper.cor_C_2_i
  - OperatorRidgelet.Paper.cor_C_2_ii
- «def:3.10»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 11downstream unlocks: 27
  Associated lean decls (5)
- «ex:3.15»(Example)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (14)
- «ex:3.16»(Example)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (8)
- «lem:3.5»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 4downstream unlocks: 18
  Associated lean decls (5)
- «lem:5.1»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (10)
- «lem:7.1»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_7_1_i
  - OperatorRidgelet.Paper.lem_7_1_ii
- «lem:7.3»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (3)
- «prop:D.3»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (5)
- «lem:5.9»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 2
  Associated lean decls (5)
- «aux:finite-dim»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (8)
- «aux:sampling-data»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 6downstream unlocks: 13
  Associated lean decls (9)
- «aux:tempered-distributions»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 7
  Associated lean decls (5)
- «def:2.2»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 7downstream unlocks: 29
  Associated lean decls (5)
- «def:3.3»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 11downstream unlocks: 32
  Associated lean decls (5)
- «lem:3.1»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 31
  Associated lean decls (4)
- «lem:3.6»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 15
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_3_6
  - OperatorRidgelet.Paper.lem_3_6_uniqueness
- «lem:4.1»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 12
  Associated lean decls (3)
- «lem:5.8»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 3
  Associated lean decls (9)
- «lem:6.2»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 13
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_6_2_i
  - OperatorRidgelet.Paper.lem_6_2_ii
- «lem:6.4»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 11
  Associated lean decls (1)
  - OperatorRidgelet.Paper.lem_6_4
- «lem:6.9»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (3)
- «roadmap:gaussian-layers»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 42
  Associated lean decls (1)
  - OperatorRidgelet.exists_isCenteredGaussianLayers
- «roadmap:trace-and-determinant»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 10
  Associated lean decls (2)
  - OperatorRidgelet.traceOf_eq_traceAlong
  - OperatorRidgelet.fredholmDet_eq_fredholmDetAlong

No prerequisites (6)

«aux:centered-gaussian»(Definition)
Associated lean decls (2)
- OperatorRidgelet.IsTraceClassCovariance
- OperatorRidgelet.IsCenteredGaussian
«aux:cylindrical»(Definition)
Associated lean decls (5)
«aux:relu-identities»(Definition)
Associated lean decls (4)
«aux:conventions»(Definition)
Associated lean decls (5)
«roadmap:polar-decomposition»(Theorem)
Associated lean decls (4)
«def:2.1»(Definition)
Associated lean decls (1)
- OperatorRidgelet.finiteNetwork

No dependents (18)

«ex:5.6»(Example)
Associated lean decls (16)
«prop:5.12»(Proposition)
Associated lean decls (13)
«ex:7.2»(Example)
Associated lean decls (11)
«prop:B.1»(Proposition)
Associated lean decls (9)
«thm:6.8»(Theorem)
Associated lean decls (3)
«ex:7.9»(Example)
Associated lean decls (24)
«cor:5.5»(Corollary)
Associated lean decls (11)
«ex:3.16»(Example)
Associated lean decls (8)
«cor:D.2»(Corollary)
Associated lean decls (6)
«cor:7.5»(Corollary)
Associated lean decls (1)
- OperatorRidgelet.Paper.cor_7_5
Show all 8 more entries without dependents
- «ex:3.13»(Example)
  Associated lean decls (5)
- «prop:D.3»(Proposition)
  Associated lean decls (5)
- «ex:7.8»(Example)
  Associated lean decls (26)
- «cor:4.9»(Corollary)
  Associated lean decls (4)
- «cor:C.1»(Corollary)
  Associated lean decls (1)
  - OperatorRidgelet.Paper.cor_C_1
- «ex:3.15»(Example)
  Associated lean decls (14)
- «lem:A.1»(Lemma)
  Associated lean decls (4)
- «cor:C.2»(Corollary)
  Associated lean decls (2)
  - OperatorRidgelet.Paper.cor_C_2_i
  - OperatorRidgelet.Paper.cor_C_2_ii