Blueprint Summary🔗

Overview

Total entries94completed: 94; deps incomplete: 0; sorries: 0; no proof: 0

Ready now0Entries with an actionable next formalization step.

Fully closed94Local code and prerequisite closure are both complete.

Actionable priorities0Entries ready now and already unlocking downstream work.

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

Missing informal coverage (4)

«roadmap:trace-and-determinant»(Theorem)
Associated lean decls (3)
«roadmap:finite-dim-universality»(Theorem)
Associated lean decls (1)
- UniversalApproximation.Leshno.leshno_dense
«roadmap:gaussian-layers»(Theorem)
Associated lean decls (1)
- OperatorRidgelet.exists_isCenteredGaussianLayers
«roadmap:polar-decomposition»(Theorem)
Associated lean decls (1)
- MeasureTheory.VectorMeasure.exists_withDensityᵥ_variation_eq

Entry index (94)

Definitions31completed: 31; deps incomplete: 0; sorries: 0; no proof: 0

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

Lemmas27completed: 27; deps incomplete: 0; sorries: 0; no proof: 0

Theorems15completed: 15; deps incomplete: 0; sorries: 0; no proof: 0

Corollaries8completed: 8; deps incomplete: 0; sorries: 0; no proof: 0

Definition Index (31)

«aux:trace-class-operators»(Definition)
Associated lean decls (9)
«aux:tempered-distributions»(Definition)
Associated lean decls (5)
«def:finite-network»(Definition)
Associated lean decls (1)
- OperatorRidgelet.finiteNetwork
«aux:sampling-data»(Definition)
Associated lean decls (11)
«aux:hilbert-schmidt»(Definition)
Associated lean decls (3)
«def:spectral-coefficient»(Definition)
Associated lean decls (4)
«def:integral-network»(Definition)
Associated lean decls (5)
«aux:torus»(Definition)
Associated lean decls (13)
«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:operator-neuron»(Definition)
Associated lean decls (6)
«def:spectral-space»(Definition)
Associated lean decls (5)
«aux:gaussian-parameter-networks»(Definition)
Associated lean decls (3)
«aux:dirichlet»(Definition)
Associated lean decls (13)
«aux:cylindrical»(Definition)
Associated lean decls (5)
«aux:tempered-activation»(Definition)
Associated lean decls (3)
«aux:relu-identities»(Definition)
Associated lean decls (4)
«def:ridgelet-analysis»(Definition)
Associated lean decls (3)
«aux:backprojection»(Definition)
Associated lean decls (4)
«aux:explicit-filters»(Definition)
Associated lean decls (6)
«def:regularized-synthesis»(Definition)
Associated lean decls (14)
«def:admissible-filter»(Definition)
Associated lean decls (5)
«aux:vector-valued»(Definition)
Associated lean decls (27)
«def:ray-regular»(Definition)
Associated lean decls (6)
«def:rademacher-complexity»(Definition)
Associated lean decls (8)
«aux:hermite»(Definition)
Associated lean decls (4)
«aux:finite-dim»(Definition)
Associated lean decls (8)
«aux:conventions»(Definition)
Associated lean decls (5)
«aux:operator-layer»(Definition)
Associated lean decls (10)

Theorem / Proposition / Lemma / Corollary Index (63)

Dependency insights

Statement-used entries76Entries reused in statement dependencies.

Most used in statements (76)

«aux:conventions»(Definition)

Reverse dependencies recorded in statement dependencies.

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

Reverse dependencies recorded in statement dependencies.

statement uses: 16proof uses: 0direct uses: 16downstream unlocks: 55
Associated lean decls (2)
- OperatorRidgelet.IsTraceClassCovariance
- OperatorRidgelet.IsCenteredGaussian
«def:admissible-filter»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 12proof uses: 0direct uses: 12downstream unlocks: 35
Associated lean decls (5)
«def:spectral-space»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 12proof uses: 0direct uses: 12downstream unlocks: 34
Associated lean decls (5)
«def:integral-network»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 11proof uses: 0direct uses: 11downstream unlocks: 40
Associated lean decls (5)
«lem:homogeneous-mixture»(Lemma)

Reverse dependencies recorded in statement dependencies.

statement uses: 11proof uses: 0direct uses: 11downstream unlocks: 31
Associated lean decls (6)
«def:ridgelet-analysis»(Definition)

Reverse dependencies recorded in statement dependencies.

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

Reverse dependencies recorded in statement dependencies.

statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 48
Associated lean decls (4)
«lem:coefficient-isometry»(Lemma)

Reverse dependencies recorded in statement dependencies.

statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 26
Associated lean decls (6)
«def:rademacher-complexity»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 21
Associated lean decls (8)
Show all 66 more statement-used entries
- «def:ray-regular»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 18
  Associated lean decls (6)
- «thm:B»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 18
  Associated lean decls (7)
- «aux:sampling-data»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 16
  Associated lean decls (11)
- «thm:lipschitz-barron»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 13
  Associated lean decls (3)
- «thm:A»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 12
  Associated lean decls (11)
- «def:spectral-coefficient»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 27
  Associated lean decls (4)
- «aux:frame-operator»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 17
  Associated lean decls (9)
- «thm:C»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 12
  Associated lean decls (18)
- «aux:operator-neuron»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 20
  Associated lean decls (6)
- «lem:fourier-slice»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 20
  Associated lean decls (5)
- «aux:tempered-activation»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 13
  Associated lean decls (3)
- «aux:gaussian-target»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 12
  Associated lean decls (13)
- «aux:operator-layer»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 6
  Associated lean decls (10)
- «lem:mixture-integration»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 33
  Associated lean decls (4)
- «def:finite-network»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 26
  Associated lean decls (1)
  - OperatorRidgelet.finiteNetwork
- «aux:trace-class-operators»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 14
  Associated lean decls (9)
- «aux:relu-identities»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 8
  Associated lean decls (4)
- «aux:cylindrical»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 7
  Associated lean decls (5)
- «lem:gaussian-decay»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 7
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_gaussian_decay_i
  - OperatorRidgelet.Paper.lem_gaussian_decay_ii
- «thm:E»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 7
  Associated lean decls (5)
- «aux:hilbert-schmidt»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 21
  Associated lean decls (3)
- «lem:spectral-unitary»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 20
  Associated lean decls (3)
- «lem:partial-fourier-l2»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 17
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_partial_fourier_l2
  - OperatorRidgelet.Paper.lem_partial_fourier_l2_uniqueness
- «aux:backprojection»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 15
  Associated lean decls (4)
- «aux:hermite»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 15
  Associated lean decls (4)
- «lem:coefficient-finite-order»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 13
  Associated lean decls (5)
- «aux:tempered-distributions»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 7
  Associated lean decls (5)
- «lem:ray-regular-examples»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 6
  Associated lean decls (5)
- «ex:operator-layer»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 3
  Associated lean decls (27)
- «lem:sobolev-tools»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 3
  Associated lean decls (9)
- «thm:tempered-reconstruction»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 3
  Associated lean decls (6)
- «lem:banach-rademacher-vanishing»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 16
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_banach_rademacher_vanishing_i
  - OperatorRidgelet.Paper.lem_banach_rademacher_vanishing_ii
- «lem:coefficient-adjoint»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 16
  Associated lean decls (3)
- «thm:general-rademacher»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 15
  Associated lean decls (1)
  - OperatorRidgelet.Paper.thm_general_rademacher
- «lem:spectral-target-basic»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 13
  Associated lean decls (3)
- «lem:gaussian-hinge»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 6
  Associated lean decls (3)
- «cor:vector-rates»(Corollary)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (5)
- «thm:vector-valued»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (35)
- «lem:rank-one-lift»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
  Associated lean decls (7)
- «aux:explicit-filters»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (6)
- «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: 49
  Associated lean decls (1)
  - OperatorRidgelet.exists_isCenteredGaussianLayers
- «thm:general-weights»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 19
  Associated lean decls (11)
- «roadmap:polar-decomposition»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 16
  Associated lean decls (1)
  - MeasureTheory.VectorMeasure.exists_withDensityᵥ_variation_eq
- «roadmap:trace-and-determinant»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 15
  Associated lean decls (3)
- «lem:two-coordinate-comparison»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 14
  Associated lean decls (1)
  - OperatorRidgelet.Paper.lem_two_coordinate_comparison
- «lem:hermite-totality»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 13
  Associated lean decls (6)
- «lem:weak-equals-strong»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 13
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_weak_equals_strong_i
  - OperatorRidgelet.Paper.lem_weak_equals_strong_ii
- «prop:coefficient-projection»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 13
  Associated lean decls (8)
- «aux:vector-valued»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
  Associated lean decls (27)
- «lem:hilbert-sampling»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
  Associated lean decls (3)
- «def:regularized-synthesis»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (14)
- «aux:gaussian-parameter-networks»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (3)
- «lem:gaussian-quadratic»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_gaussian_quadratic_i
  - OperatorRidgelet.Paper.lem_gaussian_quadratic_ii
- «lem:sobolev-pairing»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (5)
- «lem:weighted-duality»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (10)
- «aux:dirichlet»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (13)
- «aux:torus»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (13)
- «cor:two-stage-error»(Corollary)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - OperatorRidgelet.Paper.cor_two_stage_error_i
  - OperatorRidgelet.Paper.cor_two_stage_error_ii
- «ex:closed-form»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (11)
- «ex:gaussian-parameter»(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (8)
- «lem:measure-transport»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (5)
- «lem:qualitative-sampling»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - OperatorRidgelet.Paper.lem_qualitative_sampling
- «lem:standard-activation-class»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (17)
- «roadmap:finite-dim-universality»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - UniversalApproximation.Leshno.leshno_dense
- «thm:weak-sobolev-synthesis»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (5)

Metadata

Metadata audit

Missing owner94

Missing effort94

Untagged94

Missing owner (94)

«aux:backprojection»(Definition)

Missing owner metadata.
Associated lean decls (4)
«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:dirichlet»(Definition)

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

Missing owner metadata.
Associated lean decls (6)
«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-parameter-networks»(Definition)

Missing owner metadata.
Associated lean decls (3)
Show all 84 more entries missing owner
- «aux:gaussian-target»(Definition)
  
  Missing owner metadata.
  Associated lean decls (13)
- «aux:hermite»(Definition)
  
  Missing owner metadata.
  Associated lean decls (4)
- «aux:hilbert-schmidt»(Definition)
  
  Missing owner metadata.
  Associated lean decls (3)
- «aux:operator-layer»(Definition)
  
  Missing owner metadata.
  Associated lean decls (10)
- «aux:operator-neuron»(Definition)
  
  Missing owner metadata.
  Associated lean decls (6)
- «aux:relu-identities»(Definition)
  
  Missing owner metadata.
  Associated lean decls (4)
- «aux:sampling-data»(Definition)
  
  Missing owner metadata.
  Associated lean decls (11)
- «aux:tempered-activation»(Definition)
  
  Missing owner metadata.
  Associated lean decls (3)
- «aux:tempered-distributions»(Definition)
  
  Missing owner metadata.
  Associated lean decls (5)
- «aux:torus»(Definition)
  
  Missing owner metadata.
  Associated lean decls (13)
- «aux:trace-class-operators»(Definition)
  
  Missing owner metadata.
  Associated lean decls (9)
- «aux:vector-valued»(Definition)
  
  Missing owner metadata.
  Associated lean decls (27)
- «cor:coefficient-stability»(Corollary)
  
  Missing owner metadata.
  Associated lean decls (4)
- «cor:finite-backprojection»(Corollary)
  
  Missing owner metadata.
  Associated lean decls (6)
- «cor:operator-sampling»(Corollary)
  
  Missing owner metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.cor_operator_sampling_i
  - OperatorRidgelet.Paper.cor_operator_sampling_ii
- «cor:relu-admissible»(Corollary)
  
  Missing owner metadata.
  Associated lean decls (11)
- «cor:relu-discretization»(Corollary)
  
  Missing owner metadata.
  Associated lean decls (1)
  - OperatorRidgelet.Paper.cor_relu_discretization
- «cor:sampling-concentration»(Corollary)
  
  Missing owner metadata.
  Associated lean decls (1)
  - OperatorRidgelet.Paper.cor_sampling_concentration
- «cor:two-stage-error»(Corollary)
  
  Missing owner metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.cor_two_stage_error_i
  - OperatorRidgelet.Paper.cor_two_stage_error_ii
- «cor:vector-rates»(Corollary)
  
  Missing owner metadata.
  Associated lean decls (5)
- «def:admissible-filter»(Definition)
  
  Missing owner metadata.
  Associated lean decls (5)
- «def:finite-network»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - OperatorRidgelet.finiteNetwork
- «def:integral-network»(Definition)
  
  Missing owner metadata.
  Associated lean decls (5)
- «def:rademacher-complexity»(Definition)
  
  Missing owner metadata.
  Associated lean decls (8)
- «def:ray-regular»(Definition)
  
  Missing owner metadata.
  Associated lean decls (6)
- «def:regularized-synthesis»(Definition)
  
  Missing owner metadata.
  Associated lean decls (14)
- «def:ridgelet-analysis»(Definition)
  
  Missing owner metadata.
  Associated lean decls (3)
- «def:spectral-coefficient»(Definition)
  
  Missing owner metadata.
  Associated lean decls (4)
- «def:spectral-space»(Definition)
  
  Missing owner metadata.
  Associated lean decls (5)
- «ex:bandlimited-filter»(Proposition)
  
  Missing owner metadata.
  Associated lean decls (10)
- «ex:closed-form»(Proposition)
  
  Missing owner metadata.
  Associated lean decls (11)
- «ex:convolution»(Proposition)
  
  Missing owner metadata.
  Associated lean decls (13)
- «ex:core-elements»(Proposition)
  
  Missing owner metadata.
  Associated lean decls (5)
- «ex:dirichlet»(Proposition)
  
  Missing owner metadata.
  Associated lean decls (11)
- «ex:gaussian-parameter»(Proposition)
  
  Missing owner metadata.
  Associated lean decls (8)
- «ex:mexican-hat»(Proposition)
  
  Missing owner metadata.
  Associated lean decls (6)
- «ex:operator-layer»(Proposition)
  
  Missing owner metadata.
  Associated lean decls (27)
- «ex:standard-activations»(Proposition)
  
  Missing owner metadata.
  Associated lean decls (16)
- «lem:banach-rademacher-vanishing»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_banach_rademacher_vanishing_i
  - OperatorRidgelet.Paper.lem_banach_rademacher_vanishing_ii
- «lem:coefficient-adjoint»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (3)
- «lem:coefficient-finite-order»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (5)
- «lem:coefficient-isometry»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (6)
- «lem:fourier-slice»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (5)
- «lem:gaussian-decay»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_gaussian_decay_i
  - OperatorRidgelet.Paper.lem_gaussian_decay_ii
- «lem:gaussian-hinge»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (3)
- «lem:gaussian-quadratic»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_gaussian_quadratic_i
  - OperatorRidgelet.Paper.lem_gaussian_quadratic_ii
- «lem:hermite-totality»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (6)
- «lem:hilbert-sampling»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (3)
- «lem:homogeneous-mixture»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (6)
- «lem:hs-reduction»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - OperatorRidgelet.Paper.lem_hs_reduction
- «lem:measure-transport»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (5)
- «lem:mixture-character»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (4)
- «lem:mixture-integration»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (4)
- «lem:partial-fourier-l2»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_partial_fourier_l2
  - OperatorRidgelet.Paper.lem_partial_fourier_l2_uniqueness
- «lem:qualitative-sampling»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - OperatorRidgelet.Paper.lem_qualitative_sampling
- «lem:rank-one-lift»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (7)
- «lem:ray-regular-examples»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (5)
- «lem:sobolev-pairing»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (5)
- «lem:sobolev-tools»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (9)
- «lem:spectral-target-basic»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (3)
- «lem:spectral-unitary»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (3)
- «lem:standard-activation-class»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (17)
- «lem:two-coordinate-comparison»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - OperatorRidgelet.Paper.lem_two_coordinate_comparison
- «lem:weak-equals-strong»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_weak_equals_strong_i
  - OperatorRidgelet.Paper.lem_weak_equals_strong_ii
- «lem:weighted-duality»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (10)
- «prop:coefficient-projection»(Proposition)
  
  Missing owner metadata.
  Associated lean decls (8)
- «prop:dilation-obstruction»(Proposition)
  
  Missing owner metadata.
  Associated lean decls (5)
- «prop:nonbandpass-sobolev»(Proposition)
  
  Missing owner metadata.
  Associated lean decls (13)
- «prop:scalar-universality»(Proposition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.prop_scalar_universality_i
  - OperatorRidgelet.Paper.prop_scalar_universality_ii
- «roadmap:finite-dim-universality»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - UniversalApproximation.Leshno.leshno_dense
- «roadmap:gaussian-layers»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - OperatorRidgelet.exists_isCenteredGaussianLayers
- «roadmap:polar-decomposition»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - MeasureTheory.VectorMeasure.exists_withDensityᵥ_variation_eq
- «roadmap:trace-and-determinant»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (3)
- «thm:A»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (11)
- «thm:B»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (7)
- «thm:C»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (18)
- «thm:D»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (3)
- «thm:E»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (5)
- «thm:general-rademacher»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - OperatorRidgelet.Paper.thm_general_rademacher
- «thm:general-weights»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (11)
- «thm:lipschitz-barron»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (3)
- «thm:tempered-reconstruction»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (6)
- «thm:vector-valued»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (35)
- «thm:weak-sobolev-synthesis»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (5)

Missing effort (94)

«aux:backprojection»(Definition)

Missing effort metadata.
Associated lean decls (4)
«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:dirichlet»(Definition)

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

Missing effort metadata.
Associated lean decls (6)
«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-parameter-networks»(Definition)

Missing effort metadata.
Associated lean decls (3)
Show all 84 more entries missing effort
- «aux:gaussian-target»(Definition)
  
  Missing effort metadata.
  Associated lean decls (13)
- «aux:hermite»(Definition)
  
  Missing effort metadata.
  Associated lean decls (4)
- «aux:hilbert-schmidt»(Definition)
  
  Missing effort metadata.
  Associated lean decls (3)
- «aux:operator-layer»(Definition)
  
  Missing effort metadata.
  Associated lean decls (10)
- «aux:operator-neuron»(Definition)
  
  Missing effort metadata.
  Associated lean decls (6)
- «aux:relu-identities»(Definition)
  
  Missing effort metadata.
  Associated lean decls (4)
- «aux:sampling-data»(Definition)
  
  Missing effort metadata.
  Associated lean decls (11)
- «aux:tempered-activation»(Definition)
  
  Missing effort metadata.
  Associated lean decls (3)
- «aux:tempered-distributions»(Definition)
  
  Missing effort metadata.
  Associated lean decls (5)
- «aux:torus»(Definition)
  
  Missing effort metadata.
  Associated lean decls (13)
- «aux:trace-class-operators»(Definition)
  
  Missing effort metadata.
  Associated lean decls (9)
- «aux:vector-valued»(Definition)
  
  Missing effort metadata.
  Associated lean decls (27)
- «cor:coefficient-stability»(Corollary)
  
  Missing effort metadata.
  Associated lean decls (4)
- «cor:finite-backprojection»(Corollary)
  
  Missing effort metadata.
  Associated lean decls (6)
- «cor:operator-sampling»(Corollary)
  
  Missing effort metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.cor_operator_sampling_i
  - OperatorRidgelet.Paper.cor_operator_sampling_ii
- «cor:relu-admissible»(Corollary)
  
  Missing effort metadata.
  Associated lean decls (11)
- «cor:relu-discretization»(Corollary)
  
  Missing effort metadata.
  Associated lean decls (1)
  - OperatorRidgelet.Paper.cor_relu_discretization
- «cor:sampling-concentration»(Corollary)
  
  Missing effort metadata.
  Associated lean decls (1)
  - OperatorRidgelet.Paper.cor_sampling_concentration
- «cor:two-stage-error»(Corollary)
  
  Missing effort metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.cor_two_stage_error_i
  - OperatorRidgelet.Paper.cor_two_stage_error_ii
- «cor:vector-rates»(Corollary)
  
  Missing effort metadata.
  Associated lean decls (5)
- «def:admissible-filter»(Definition)
  
  Missing effort metadata.
  Associated lean decls (5)
- «def:finite-network»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - OperatorRidgelet.finiteNetwork
- «def:integral-network»(Definition)
  
  Missing effort metadata.
  Associated lean decls (5)
- «def:rademacher-complexity»(Definition)
  
  Missing effort metadata.
  Associated lean decls (8)
- «def:ray-regular»(Definition)
  
  Missing effort metadata.
  Associated lean decls (6)
- «def:regularized-synthesis»(Definition)
  
  Missing effort metadata.
  Associated lean decls (14)
- «def:ridgelet-analysis»(Definition)
  
  Missing effort metadata.
  Associated lean decls (3)
- «def:spectral-coefficient»(Definition)
  
  Missing effort metadata.
  Associated lean decls (4)
- «def:spectral-space»(Definition)
  
  Missing effort metadata.
  Associated lean decls (5)
- «ex:bandlimited-filter»(Proposition)
  
  Missing effort metadata.
  Associated lean decls (10)
- «ex:closed-form»(Proposition)
  
  Missing effort metadata.
  Associated lean decls (11)
- «ex:convolution»(Proposition)
  
  Missing effort metadata.
  Associated lean decls (13)
- «ex:core-elements»(Proposition)
  
  Missing effort metadata.
  Associated lean decls (5)
- «ex:dirichlet»(Proposition)
  
  Missing effort metadata.
  Associated lean decls (11)
- «ex:gaussian-parameter»(Proposition)
  
  Missing effort metadata.
  Associated lean decls (8)
- «ex:mexican-hat»(Proposition)
  
  Missing effort metadata.
  Associated lean decls (6)
- «ex:operator-layer»(Proposition)
  
  Missing effort metadata.
  Associated lean decls (27)
- «ex:standard-activations»(Proposition)
  
  Missing effort metadata.
  Associated lean decls (16)
- «lem:banach-rademacher-vanishing»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_banach_rademacher_vanishing_i
  - OperatorRidgelet.Paper.lem_banach_rademacher_vanishing_ii
- «lem:coefficient-adjoint»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (3)
- «lem:coefficient-finite-order»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (5)
- «lem:coefficient-isometry»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (6)
- «lem:fourier-slice»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (5)
- «lem:gaussian-decay»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_gaussian_decay_i
  - OperatorRidgelet.Paper.lem_gaussian_decay_ii
- «lem:gaussian-hinge»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (3)
- «lem:gaussian-quadratic»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_gaussian_quadratic_i
  - OperatorRidgelet.Paper.lem_gaussian_quadratic_ii
- «lem:hermite-totality»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (6)
- «lem:hilbert-sampling»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (3)
- «lem:homogeneous-mixture»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (6)
- «lem:hs-reduction»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - OperatorRidgelet.Paper.lem_hs_reduction
- «lem:measure-transport»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (5)
- «lem:mixture-character»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (4)
- «lem:mixture-integration»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (4)
- «lem:partial-fourier-l2»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_partial_fourier_l2
  - OperatorRidgelet.Paper.lem_partial_fourier_l2_uniqueness
- «lem:qualitative-sampling»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - OperatorRidgelet.Paper.lem_qualitative_sampling
- «lem:rank-one-lift»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (7)
- «lem:ray-regular-examples»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (5)
- «lem:sobolev-pairing»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (5)
- «lem:sobolev-tools»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (9)
- «lem:spectral-target-basic»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (3)
- «lem:spectral-unitary»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (3)
- «lem:standard-activation-class»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (17)
- «lem:two-coordinate-comparison»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - OperatorRidgelet.Paper.lem_two_coordinate_comparison
- «lem:weak-equals-strong»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_weak_equals_strong_i
  - OperatorRidgelet.Paper.lem_weak_equals_strong_ii
- «lem:weighted-duality»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (10)
- «prop:coefficient-projection»(Proposition)
  
  Missing effort metadata.
  Associated lean decls (8)
- «prop:dilation-obstruction»(Proposition)
  
  Missing effort metadata.
  Associated lean decls (5)
- «prop:nonbandpass-sobolev»(Proposition)
  
  Missing effort metadata.
  Associated lean decls (13)
- «prop:scalar-universality»(Proposition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.prop_scalar_universality_i
  - OperatorRidgelet.Paper.prop_scalar_universality_ii
- «roadmap:finite-dim-universality»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - UniversalApproximation.Leshno.leshno_dense
- «roadmap:gaussian-layers»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - OperatorRidgelet.exists_isCenteredGaussianLayers
- «roadmap:polar-decomposition»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - MeasureTheory.VectorMeasure.exists_withDensityᵥ_variation_eq
- «roadmap:trace-and-determinant»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (3)
- «thm:A»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (11)
- «thm:B»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (7)
- «thm:C»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (18)
- «thm:D»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (3)
- «thm:E»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (5)
- «thm:general-rademacher»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - OperatorRidgelet.Paper.thm_general_rademacher
- «thm:general-weights»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (11)
- «thm:lipschitz-barron»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (3)
- «thm:tempered-reconstruction»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (6)
- «thm:vector-valued»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (35)
- «thm:weak-sobolev-synthesis»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (5)

Untagged (94)

«aux:backprojection»(Definition)

Missing tag metadata.
Associated lean decls (4)
«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:dirichlet»(Definition)

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

Missing tag metadata.
Associated lean decls (6)
«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-parameter-networks»(Definition)

Missing tag metadata.
Associated lean decls (3)
Show all 84 more untagged entries
- «aux:gaussian-target»(Definition)
  
  Missing tag metadata.
  Associated lean decls (13)
- «aux:hermite»(Definition)
  
  Missing tag metadata.
  Associated lean decls (4)
- «aux:hilbert-schmidt»(Definition)
  
  Missing tag metadata.
  Associated lean decls (3)
- «aux:operator-layer»(Definition)
  
  Missing tag metadata.
  Associated lean decls (10)
- «aux:operator-neuron»(Definition)
  
  Missing tag metadata.
  Associated lean decls (6)
- «aux:relu-identities»(Definition)
  
  Missing tag metadata.
  Associated lean decls (4)
- «aux:sampling-data»(Definition)
  
  Missing tag metadata.
  Associated lean decls (11)
- «aux:tempered-activation»(Definition)
  
  Missing tag metadata.
  Associated lean decls (3)
- «aux:tempered-distributions»(Definition)
  
  Missing tag metadata.
  Associated lean decls (5)
- «aux:torus»(Definition)
  
  Missing tag metadata.
  Associated lean decls (13)
- «aux:trace-class-operators»(Definition)
  
  Missing tag metadata.
  Associated lean decls (9)
- «aux:vector-valued»(Definition)
  
  Missing tag metadata.
  Associated lean decls (27)
- «cor:coefficient-stability»(Corollary)
  
  Missing tag metadata.
  Associated lean decls (4)
- «cor:finite-backprojection»(Corollary)
  
  Missing tag metadata.
  Associated lean decls (6)
- «cor:operator-sampling»(Corollary)
  
  Missing tag metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.cor_operator_sampling_i
  - OperatorRidgelet.Paper.cor_operator_sampling_ii
- «cor:relu-admissible»(Corollary)
  
  Missing tag metadata.
  Associated lean decls (11)
- «cor:relu-discretization»(Corollary)
  
  Missing tag metadata.
  Associated lean decls (1)
  - OperatorRidgelet.Paper.cor_relu_discretization
- «cor:sampling-concentration»(Corollary)
  
  Missing tag metadata.
  Associated lean decls (1)
  - OperatorRidgelet.Paper.cor_sampling_concentration
- «cor:two-stage-error»(Corollary)
  
  Missing tag metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.cor_two_stage_error_i
  - OperatorRidgelet.Paper.cor_two_stage_error_ii
- «cor:vector-rates»(Corollary)
  
  Missing tag metadata.
  Associated lean decls (5)
- «def:admissible-filter»(Definition)
  
  Missing tag metadata.
  Associated lean decls (5)
- «def:finite-network»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - OperatorRidgelet.finiteNetwork
- «def:integral-network»(Definition)
  
  Missing tag metadata.
  Associated lean decls (5)
- «def:rademacher-complexity»(Definition)
  
  Missing tag metadata.
  Associated lean decls (8)
- «def:ray-regular»(Definition)
  
  Missing tag metadata.
  Associated lean decls (6)
- «def:regularized-synthesis»(Definition)
  
  Missing tag metadata.
  Associated lean decls (14)
- «def:ridgelet-analysis»(Definition)
  
  Missing tag metadata.
  Associated lean decls (3)
- «def:spectral-coefficient»(Definition)
  
  Missing tag metadata.
  Associated lean decls (4)
- «def:spectral-space»(Definition)
  
  Missing tag metadata.
  Associated lean decls (5)
- «ex:bandlimited-filter»(Proposition)
  
  Missing tag metadata.
  Associated lean decls (10)
- «ex:closed-form»(Proposition)
  
  Missing tag metadata.
  Associated lean decls (11)
- «ex:convolution»(Proposition)
  
  Missing tag metadata.
  Associated lean decls (13)
- «ex:core-elements»(Proposition)
  
  Missing tag metadata.
  Associated lean decls (5)
- «ex:dirichlet»(Proposition)
  
  Missing tag metadata.
  Associated lean decls (11)
- «ex:gaussian-parameter»(Proposition)
  
  Missing tag metadata.
  Associated lean decls (8)
- «ex:mexican-hat»(Proposition)
  
  Missing tag metadata.
  Associated lean decls (6)
- «ex:operator-layer»(Proposition)
  
  Missing tag metadata.
  Associated lean decls (27)
- «ex:standard-activations»(Proposition)
  
  Missing tag metadata.
  Associated lean decls (16)
- «lem:banach-rademacher-vanishing»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_banach_rademacher_vanishing_i
  - OperatorRidgelet.Paper.lem_banach_rademacher_vanishing_ii
- «lem:coefficient-adjoint»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (3)
- «lem:coefficient-finite-order»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (5)
- «lem:coefficient-isometry»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (6)
- «lem:fourier-slice»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (5)
- «lem:gaussian-decay»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_gaussian_decay_i
  - OperatorRidgelet.Paper.lem_gaussian_decay_ii
- «lem:gaussian-hinge»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (3)
- «lem:gaussian-quadratic»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_gaussian_quadratic_i
  - OperatorRidgelet.Paper.lem_gaussian_quadratic_ii
- «lem:hermite-totality»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (6)
- «lem:hilbert-sampling»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (3)
- «lem:homogeneous-mixture»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (6)
- «lem:hs-reduction»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - OperatorRidgelet.Paper.lem_hs_reduction
- «lem:measure-transport»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (5)
- «lem:mixture-character»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (4)
- «lem:mixture-integration»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (4)
- «lem:partial-fourier-l2»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_partial_fourier_l2
  - OperatorRidgelet.Paper.lem_partial_fourier_l2_uniqueness
- «lem:qualitative-sampling»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - OperatorRidgelet.Paper.lem_qualitative_sampling
- «lem:rank-one-lift»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (7)
- «lem:ray-regular-examples»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (5)
- «lem:sobolev-pairing»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (5)
- «lem:sobolev-tools»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (9)
- «lem:spectral-target-basic»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (3)
- «lem:spectral-unitary»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (3)
- «lem:standard-activation-class»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (17)
- «lem:two-coordinate-comparison»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - OperatorRidgelet.Paper.lem_two_coordinate_comparison
- «lem:weak-equals-strong»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_weak_equals_strong_i
  - OperatorRidgelet.Paper.lem_weak_equals_strong_ii
- «lem:weighted-duality»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (10)
- «prop:coefficient-projection»(Proposition)
  
  Missing tag metadata.
  Associated lean decls (8)
- «prop:dilation-obstruction»(Proposition)
  
  Missing tag metadata.
  Associated lean decls (5)
- «prop:nonbandpass-sobolev»(Proposition)
  
  Missing tag metadata.
  Associated lean decls (13)
- «prop:scalar-universality»(Proposition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - OperatorRidgelet.Paper.prop_scalar_universality_i
  - OperatorRidgelet.Paper.prop_scalar_universality_ii
- «roadmap:finite-dim-universality»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - UniversalApproximation.Leshno.leshno_dense
- «roadmap:gaussian-layers»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - OperatorRidgelet.exists_isCenteredGaussianLayers
- «roadmap:polar-decomposition»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - MeasureTheory.VectorMeasure.exists_withDensityᵥ_variation_eq
- «roadmap:trace-and-determinant»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (3)
- «thm:A»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (11)
- «thm:B»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (7)
- «thm:C»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (18)
- «thm:D»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (3)
- «thm:E»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (5)
- «thm:general-rademacher»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - OperatorRidgelet.Paper.thm_general_rademacher
- «thm:general-weights»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (11)
- «thm:lipschitz-barron»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (3)
- «thm:tempered-reconstruction»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (6)
- «thm:vector-valued»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (35)
- «thm:weak-sobolev-synthesis»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (5)

Structure and coverage

Fully closed94Local code and ancestor closure are both complete.

Heaviest prerequisites (85)

«ex:operator-layer»(Proposition)

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

total deps: 13statement deps: 13proof deps: 0direct uses: 3downstream unlocks: 3
Associated lean decls (27)
«thm:C»(Theorem)

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

total deps: 11statement deps: 11proof deps: 0direct uses: 6downstream unlocks: 12
Associated lean decls (18)
«thm:D»(Theorem)

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

total deps: 11statement deps: 11proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (3)
«ex:closed-form»(Proposition)

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

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

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

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

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

total deps: 8statement deps: 8proof deps: 0direct uses: 7downstream unlocks: 18
Associated lean decls (7)
«thm:E»(Theorem)

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

total deps: 8statement deps: 8proof deps: 0direct uses: 4downstream unlocks: 7
Associated lean decls (5)
«thm:vector-valued»(Theorem)

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

total deps: 8statement deps: 8proof deps: 0direct uses: 2downstream unlocks: 5
Associated lean decls (35)
«thm:general-weights»(Theorem)

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

total deps: 7statement deps: 7proof deps: 0direct uses: 1downstream unlocks: 19
Associated lean decls (11)
«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: 6
Associated lean decls (27)
Show all 75 more heaviest-prerequisite entries
- «ex:convolution»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 6statement deps: 6proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (13)
- «cor:relu-admissible»(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)
- «cor:vector-rates»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 5statement deps: 5proof deps: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (5)
- «def:regularized-synthesis»(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)
- «ex:core-elements»(Proposition)
  
  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 (5)
- «ex:dirichlet»(Proposition)
  
  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)
- «lem:coefficient-finite-order»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 5statement deps: 5proof deps: 0direct uses: 3downstream unlocks: 13
  Associated lean decls (5)
- «prop:coefficient-projection»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 5statement deps: 5proof deps: 0direct uses: 1downstream unlocks: 13
  Associated lean decls (8)
- «thm:tempered-reconstruction»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 5statement deps: 5proof deps: 0direct uses: 3downstream unlocks: 3
  Associated lean decls (6)
- «aux:backprojection»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 4statement deps: 4proof deps: 0direct uses: 3downstream unlocks: 15
  Associated lean decls (4)
- «cor:finite-backprojection»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (6)
- «cor:relu-discretization»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - OperatorRidgelet.Paper.cor_relu_discretization
- «ex:gaussian-parameter»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (8)
- «ex:standard-activations»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (16)
- «lem:rank-one-lift»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 4statement deps: 4proof deps: 0direct uses: 2downstream unlocks: 3
  Associated lean decls (7)
- «lem:weak-equals-strong»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 13
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_weak_equals_strong_i
  - OperatorRidgelet.Paper.lem_weak_equals_strong_ii
- «prop:nonbandpass-sobolev»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (13)
- «prop:scalar-universality»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - OperatorRidgelet.Paper.prop_scalar_universality_i
  - OperatorRidgelet.Paper.prop_scalar_universality_ii
- «thm:general-rademacher»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 4statement deps: 4proof deps: 0direct uses: 2downstream unlocks: 15
  Associated lean decls (1)
  - OperatorRidgelet.Paper.thm_general_rademacher
- «thm:weak-sobolev-synthesis»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (5)
- «aux:gaussian-parameter-networks»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (3)
- «aux:gaussian-target»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 5downstream unlocks: 12
  Associated lean decls (13)
- «aux:hermite»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 3downstream unlocks: 15
  Associated lean decls (4)
- «aux:operator-layer»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 5downstream unlocks: 6
  Associated lean decls (10)
- «aux:operator-neuron»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 5downstream unlocks: 20
  Associated lean decls (6)
- «cor:coefficient-stability»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (4)
- «cor:operator-sampling»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - OperatorRidgelet.Paper.cor_operator_sampling_i
  - OperatorRidgelet.Paper.cor_operator_sampling_ii
- «def:ray-regular»(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 (6)
- «def:ridgelet-analysis»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 9downstream unlocks: 43
  Associated lean decls (3)
- «def:spectral-coefficient»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 6downstream unlocks: 27
  Associated lean decls (4)
- «ex:bandlimited-filter»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (10)
- «ex:mexican-hat»(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (6)
- «lem:gaussian-decay»(Lemma)
  
  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 (2)
  - OperatorRidgelet.Paper.lem_gaussian_decay_i
  - OperatorRidgelet.Paper.lem_gaussian_decay_ii
- «lem:homogeneous-mixture»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 11downstream unlocks: 31
  Associated lean decls (6)
- «lem:measure-transport»(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 (5)
- «lem:mixture-character»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (4)
- «lem:qualitative-sampling»(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_qualitative_sampling
- «lem:ray-regular-examples»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 3downstream unlocks: 6
  Associated lean decls (5)
- «lem:standard-activation-class»(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 (17)
- «thm:lipschitz-barron»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 7downstream unlocks: 13
  Associated lean decls (3)
- «aux:dirichlet»(Definition)
  
  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 (13)
- «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: 17
  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: 48
  Associated lean decls (4)
- «aux:sampling-data»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 7downstream unlocks: 16
  Associated lean decls (11)
- «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: 13
  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: 14
  Associated lean decls (9)
- «cor:sampling-concentration»(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_sampling_concentration
- «cor:two-stage-error»(Corollary)
  
  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.cor_two_stage_error_i
  - OperatorRidgelet.Paper.cor_two_stage_error_ii
- «def:rademacher-complexity»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 7downstream unlocks: 21
  Associated lean decls (8)
- «def:spectral-space»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 12downstream unlocks: 34
  Associated lean decls (5)
- «lem:coefficient-adjoint»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 16
  Associated lean decls (3)
- «lem:coefficient-isometry»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 7downstream unlocks: 26
  Associated lean decls (6)
- «lem:fourier-slice»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 5downstream unlocks: 20
  Associated lean decls (5)
- «lem:gaussian-hinge»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 6
  Associated lean decls (3)
- «lem:gaussian-quadratic»(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 (2)
  - OperatorRidgelet.Paper.lem_gaussian_quadratic_i
  - OperatorRidgelet.Paper.lem_gaussian_quadratic_ii
- «lem:hermite-totality»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 13
  Associated lean decls (6)
- «lem:hs-reduction»(Lemma)
  
  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.lem_hs_reduction
- «lem:spectral-unitary»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 20
  Associated lean decls (3)
- «lem:weighted-duality»(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)
- «prop:dilation-obstruction»(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)
- «aux:explicit-filters»(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 (6)
- «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: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)
- «aux:torus»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (13)
- «def:admissible-filter»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 12downstream unlocks: 35
  Associated lean decls (5)
- «lem:banach-rademacher-vanishing»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 16
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_banach_rademacher_vanishing_i
  - OperatorRidgelet.Paper.lem_banach_rademacher_vanishing_ii
- «lem:hilbert-sampling»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 6
  Associated lean decls (3)
- «lem:mixture-integration»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 33
  Associated lean decls (4)
- «lem:partial-fourier-l2»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 17
  Associated lean decls (2)
  - OperatorRidgelet.Paper.lem_partial_fourier_l2
  - OperatorRidgelet.Paper.lem_partial_fourier_l2_uniqueness
- «lem:sobolev-pairing»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (5)
- «lem:sobolev-tools»(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:spectral-target-basic»(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 (3)
- «lem:two-coordinate-comparison»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 14
  Associated lean decls (1)
  - OperatorRidgelet.Paper.lem_two_coordinate_comparison
- «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: 49
  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: 15
  Associated lean decls (3)

No prerequisites (9)

«aux:centered-gaussian»(Definition)
Associated lean decls (2)
- OperatorRidgelet.IsTraceClassCovariance
- OperatorRidgelet.IsCenteredGaussian
«roadmap:finite-dim-universality»(Theorem)
Associated lean decls (1)
- UniversalApproximation.Leshno.leshno_dense
«aux:conventions»(Definition)
Associated lean decls (5)
«aux:relu-identities»(Definition)
Associated lean decls (4)
«roadmap:polar-decomposition»(Theorem)
Associated lean decls (1)
- MeasureTheory.VectorMeasure.exists_withDensityᵥ_variation_eq
«aux:cylindrical»(Definition)
Associated lean decls (5)
«def:integral-network»(Definition)
Associated lean decls (5)
«aux:hilbert-schmidt»(Definition)
Associated lean decls (3)
«def:finite-network»(Definition)
Associated lean decls (1)
- OperatorRidgelet.finiteNetwork

No dependents (18)