Lean Ridgelet Blueprint

Blueprint Summary🔗

Overview

Total entries308completed: 277; deps incomplete: 0; sorries: 8; no proof: 19

Ready now8Entries whose next formalization step is currently unblocked.

Fully closed277Local code and prerequisite closure are both complete.

Actionable priorities6Entries ready now and already unlocking downstream work.

Current blockers8Missing external or incomplete Lean declarations.

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

Ready next (6)

measure_valued_synthesis_detail(Definition)

Ready for statement work.

stage: statementstatement: ready to formalizedirect uses: 2downstream unlocks: 3
l1_lizorkin_spaces(Definition)

Ready for statement work.

stage: statementstatement: ready to formalizedirect uses: 2downstream unlocks: 2
measure_valued_synthesis(Definition)

Ready for statement work.

stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 2
ha_bochner_preliminaries(Lemma)

Ready for proof work.

stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 1proof: ready to formalize
ha_l2_integral_detail(Theorem)

Ready for proof work.

stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 1proof: ready to formalize
normalized_finite_width_approximation(Theorem)

Ready for proof work.

stage: proofstatement: formalizeddirect uses: 1downstream unlocks: 1proof: Lean code incomplete
Associated lean decls (1)
- LeanRidgelet.l2_theorem_five_normalized_finite_width_approximation

Current blockers (8)

fs_symmetric_hyperbolic(Definition)

Declaration with sorry: LeanRidgelet.fs_hyperbolicHelgasonInversion [theorem/lemma; contains sorry; in proof; refs: unknown]
normalized_finite_width_approximation(Theorem)

Declaration with sorry: LeanRidgelet.l2_theorem_five_normalized_finite_width_approximation [theorem/lemma; contains sorry; in proof; refs: unknown]
ha_quadratic_nonzero_detail(Theorem)

Declaration with sorry: LeanRidgelet.exists_quadraticAdmissiblePair [theorem/lemma; contains sorry; in proof; refs: unknown]
fs_symmetric_spd(Definition)

Declaration with sorry: LeanRidgelet.fs_spdHelgasonInversion [theorem/lemma; contains sorry; in proof; refs: unknown]
exact_finite_null_relations(Proposition)

Declaration with sorry: LeanRidgelet.l2_proposition_two_exact_finite_null_relations [theorem/lemma; contains sorry; in proof; refs: unknown]
fs_target_svd_jacobian(Lemma)

Declaration with sorry: LeanRidgelet.fs_svdJacobian [theorem/lemma; contains sorry; in proof; refs: unknown]
discretizable_ridgelet_null_elements(Corollary)

Declaration with sorry: LeanRidgelet.l2_corollary_one_discretizable_ridgelet_null_elements [theorem/lemma; contains sorry; in proof; refs: unknown]
null_space_encoding_and_perturbations(Theorem)

Declaration with sorry: LeanRidgelet.l2_theorem_four_encoding_and_perturbative_readout [theorem/lemma; contains sorry; in proof; refs: unknown]

Missing informal coverage (225)

Entry index (308)

Definitions64completed: 58; deps incomplete: 0; sorries: 2; no proof: 0

Propositions17completed: 14; deps incomplete: 0; sorries: 1; no proof: 2

Lemmas50completed: 45; deps incomplete: 0; sorries: 1; no proof: 4

Theorems172completed: 158; deps incomplete: 0; sorries: 3; no proof: 11

Corollaries5completed: 2; deps incomplete: 0; sorries: 1; no proof: 2

Informal-only entries23

Definition Index (64)

l1_fourier_away_from_origin(Definition)
Associated lean decls (2)
- MeasureTheory.PolynomiallyBounded
- LeanRidgelet.HasFourierAwayFromOrigin
canonical_solution_and_projection(Definition)
Associated lean decls (4)
l1_weak_ridgelet(Definition)
Associated lean decls (1)
- LeanRidgelet.weakRidgeletTransform
fs_gconv_network(Definition)
Associated lean decls (7)
fiber_space(Definition)
Associated lean decls (6)
ha_induced_representations(Definition)
Associated lean decls (3)
fs_finite_field_network(Definition)
Associated lean decls (3)
ha_intertwiner_operators(Definition)
Associated lean decls (2)
- LeanRidgelet.JointEquivariantMachine
- LeanRidgelet.JointEquivariantRidgelet
fs_symmetric_hyperbolic(Definition)
Associated lean decls (21)
angular_fourier_convention(Definition)
Associated lean decls (3)
ha_ridgelet_transform(Definition)
Associated lean decls (1)
- LeanRidgelet.JointEquivariantRidgelet
l1_radon_backprojection(Definition)
Associated lean decls (3)
mathlib_lizorkin_space(Definition)
Associated lean decls (9)
parameter_space_and_unitary_transform(Definition)
Associated lean decls (4)
activation_fiber_functional(Definition)
Associated lean decls (5)
measure_valued_synthesis_detail(Definition)
l1_ridgelet_transforms(Definition)
Associated lean decls (4)
ha_affine_homogeneous_quasiregular_detail(Definition)
Associated lean decls (29)
measure_valued_synthesis(Definition)
ha_joint_equivariance_detail(Definition)
Associated lean decls (2)
- LeanRidgelet.IsJointEquivariant
- LeanRidgelet.IsEquivariant
l1_parameter_space(Definition)
Associated lean decls (4)
activation_space_detail(Definition)
Associated lean decls (2)
- LeanRidgelet.ActivationSpace
- LeanRidgelet.activationDistribution
ha_unitary_representation_detail(Definition)
Associated lean decls (4)
coefficient_vector(Definition)
Associated lean decls (1)
- LeanRidgelet.fiberCoefficient
activation_space(Definition)
Associated lean decls (2)
- LeanRidgelet.ActivationSpace
- LeanRidgelet.activationDistribution
fourier_dilation_unitary(Definition)
Associated lean decls (3)
network_synthesis(Definition)
Associated lean decls (4)
ha_unitary_irreducibility(Definition)
Associated lean decls (3)
fs_symmetric_network(Definition)
Associated lean decls (5)
ridgelet_operator(Definition)
Associated lean decls (8)
fs_symmetric_spd(Definition)
Associated lean decls (16)
normalized_network_right_inverse(Definition)
Associated lean decls (1)
- LeanRidgelet.normalizedNetworkRightInverse
ha_joint_machine(Definition)
Associated lean decls (1)
- LeanRidgelet.JointEquivariantMachine
ha_affine_representations(Definition)
Associated lean decls (4)
ha_joint_equivariance(Definition)
Associated lean decls (1)
- LeanRidgelet.IsJointEquivariant
activation_normalization(Definition)
Associated lean decls (1)
- LeanRidgelet.activationNormalization
fourier_dilation_coordinate(Definition)
Associated lean decls (2)
- LeanRidgelet.frequencyDilation
- LeanRidgelet.fourierDilationCoordinate
hilbert_space_synthesis(Definition)
Associated lean decls (5)
adjoint_ridgelet_function(Definition)
Associated lean decls (4)
fs_pairing(Definition)
Associated lean decls (1)
- LeanRidgelet.fourierSlicePairing
ha_affine_lift_detail(Definition)
Associated lean decls (22)
canonical_parameter_projection(Definition)
Associated lean decls (1)
- LeanRidgelet.networkVisibleProjection
ha_depth_two_machine(Definition)
Associated lean decls (5)
ridgelet_transform_and_pairing(Definition)
Associated lean decls (10)
ha_quadratic_feature(Definition)
Associated lean decls (16)
ha_appendix_depth_two(Definition)
fourier_dilation_core(Definition)
Associated lean decls (5)
activation_riesz_representer(Definition)
Associated lean decls (1)
- LeanRidgelet.activationRieszRepresenter
activation_functional(Definition)
Associated lean decls (5)
pointwise_coordinate_transform(Definition)
Associated lean decls (4)
japanese_bracket(Definition)
Associated lean decls (1)
- LeanRidgelet.japaneseBracketPow
ha_l2_operator_bridge_detail(Definition)
Associated lean decls (4)
l1_standard_activations(Definition)
Associated lean decls (3)
fs_dplane_transform(Definition)
Associated lean decls (6)
mathlib_radon_transform(Definition)
Associated lean decls (3)
fs_pairing_detail(Definition)
Associated lean decls (1)
- LeanRidgelet.fourierSlicePairing
coefficient_space(Definition)
Associated lean decls (4)
abstract_synthesis_and_reconstruction(Definition)
Associated lean decls (2)
- LeanRidgelet.unitarySynthesis
- LeanRidgelet.unitaryRidgelet
l1_admissibility(Definition)
Associated lean decls (5)
ha_fully_connected_feature(Definition)
Associated lean decls (2)
- LeanRidgelet.deepFullyConnectedFeature
- LeanRidgelet.deepFullyConnectedFeature_endpoint_equivariant
parameter_space(Definition)
Associated lean decls (2)
- LeanRidgelet.ParameterSpace
- LeanRidgelet.parameterCoordinateEquiv
l1_lizorkin_spaces(Definition)
inverse_fourier_dilation_core(Definition)
Associated lean decls (1)
- LeanRidgelet.inverseFourierDilationTransformCore
ha_induced_l2_detail(Definition)
Associated lean decls (16)

Theorem / Proposition / Lemma / Corollary Index (244)

Dependency insights

Statement-used entries215Entries reused in statement dependencies.

Most used in statements (215)

l1_fourier_away_from_origin(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 23
Associated lean decls (2)
- MeasureTheory.PolynomiallyBounded
- LeanRidgelet.HasFourierAwayFromOrigin
l1_ridgelet_transforms(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 23
Associated lean decls (4)
l1_admissibility(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 14
Associated lean decls (5)
mathlib_polar_coordinates(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 21
Associated lean decls (15)
ha_joint_equivariance(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 18
Associated lean decls (1)
- LeanRidgelet.IsJointEquivariant
fs_reconstruction_euclidean(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 15
Associated lean decls (2)
- LeanRidgelet.fs_inversionIntegral_euclidean
- LeanRidgelet.fs_reconstruction_euclidean
mathlib_unitary_conjugation(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 15
Associated lean decls (14)
fs_dplane_transform(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 11
Associated lean decls (6)
mathlib_radon_transform(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 49
Associated lean decls (3)
mathlib_affine_haar(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 36
Associated lean decls (6)
Show all 205 more statement-used entries
- ha_affine_jacobian_detail(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 30
  Associated lean decls (11)
- mathlib_dplane_transform(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 24
  Associated lean decls (23)
- mathlib_symmetric_space_defs(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 18
  Associated lean decls (15)
- mathlib_helgason_inversion(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 10
  Associated lean decls (9)
- l1_parameter_space(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 35
  Associated lean decls (4)
- mathlib_lizorkin_space(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 25
  Associated lean decls (9)
- mathlib_bochner_integral_l2(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 18
  Associated lean decls (4)
- l1_radon_backprojection(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 15
  Associated lean decls (3)
- mathlib_l2_duality(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 14
  Associated lean decls (7)
- abstract_reconstruction(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 12
  Associated lean decls (4)
- ha_affine_mackey_detail(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 8
  Associated lean decls (18)
- ha_quadratic_transfer_detail(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 7
  Associated lean decls (5)
- l1_standard_activations(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 7
  Associated lean decls (3)
- mathlib_matrix_polar(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 7
  Associated lean decls (11)
- ha_quadratic_shear_detail(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 6
  Associated lean decls (19)
- ha_induced_l2_detail(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 39
  Associated lean decls (16)
- ha_joint_equivariance_constructors(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 39
  Associated lean decls (5)
- ha_bochner_intertwining_detail(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 38
  Associated lean decls (17)
- mathlib_radon_l1_theory(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 33
  Associated lean decls (6)
- mathlib_fourier_slice(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 32
  Associated lean decls (1)
  - MeasureTheory.fourier_slice_radonTransform
- ha_unitary_irreducibility(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 30
  Associated lean decls (3)
- ha_intertwiner_operators(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 23
  Associated lean decls (2)
  - LeanRidgelet.JointEquivariantMachine
  - LeanRidgelet.JointEquivariantRidgelet
- mathlib_fourier_plancherel(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 22
  Associated lean decls (7)
- ha_reconstruction_detail(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 21
  Associated lean decls (5)
- mathlib_orthogonal_group(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 18
  Associated lean decls (21)
- ha_quadratic_detail(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 15
  Associated lean decls (27)
- ha_affine_irreducibility(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 13
  Associated lean decls (19)
- ha_induced_representations(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 13
  Associated lean decls (3)
- mathlib_sphere_invariant_measure(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 13
  Associated lean decls (15)
- ha_quadratic_relative_measure_detail(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 11
  Associated lean decls (24)
- l1_reconstruction_moment_layer(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 10
  Associated lean decls (4)
- ha_joint_machine(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 9
  Associated lean decls (1)
  - LeanRidgelet.JointEquivariantMachine
- fs_dplane_stiefel_codim_one(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 8
  Associated lean decls (5)
- ha_quadratic_parameter_factor_detail(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 7
  Associated lean decls (13)
- l1_lambda_multiplier(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 7
  Associated lean decls (11)
- ha_l2_operator_bridge_detail(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 6
  Associated lean decls (4)
- l1_fourier_expression(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 6
  Associated lean decls (4)
- fs_dplane_stiefel(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 5
  Associated lean decls (9)
- fs_scheme_detail(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 5
  Associated lean decls (9)
- ha_main_reconstruction(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 5
  Associated lean decls (3)
- mathlib_hyperbolic_ball(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 5
  Associated lean decls (16)
- l1_truncated_power_fourier(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 4
  Associated lean decls (1)
  - LeanRidgelet.l1_truncatedPower_hasFourierAwayFromOrigin
- mathlib_corner_det(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 4
  Associated lean decls (23)
- mathlib_hyperbolic_mobius(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 4
  Associated lean decls (21)
- mathlib_lp_indicator(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 4
  Associated lean decls (12)
- fs_symmetric_reconstruction(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 3
  Associated lean decls (5)
- l1_parseval_plancherel(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 3
  Associated lean decls (2)
  - LeanRidgelet.l1_plancherel_identity
  - LeanRidgelet.l1_parseval_relation
- mathlib_spd_model(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 3
  Associated lean decls (23)
- ha_unitary_representation_detail(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 41
  Associated lean decls (4)
- mathlib_iterated_fubini(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 24
  Associated lean decls (2)
  - MeasureTheory.integral_integral_integral_swap_left
  - MeasureTheory.integral_integral_integral_swap_right
- fs_pairing(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 21
  Associated lean decls (1)
  - LeanRidgelet.fourierSlicePairing
- fs_method(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 20
  Associated lean decls (8)
- ha_schur_lemma(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 20
  Associated lean decls (3)
- abstract_synthesis_and_reconstruction(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 16
  Associated lean decls (2)
  - LeanRidgelet.unitarySynthesis
  - LeanRidgelet.unitaryRidgelet
- mathlib_group_convolution_continuity(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 16
  Associated lean decls (1)
  - MeasureTheory.continuous_integral_compact_mul_right
- mathlib_hilbert_symbol(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 16
  Associated lean decls (11)
- coefficient_space(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 14
  Associated lean decls (4)
- pointwise_coordinate_transform(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 14
  Associated lean decls (4)
- activation_space(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 12
  Associated lean decls (2)
  - LeanRidgelet.ActivationSpace
  - LeanRidgelet.activationDistribution
- concrete_unitary_transform(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 11
  Associated lean decls (6)
- mathlib_schwartz_aux(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 11
  Associated lean decls (6)
- activation_functional(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 10
  Associated lean decls (5)
- mathlib_hilbert_schmidt_kernel(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 10
  Associated lean decls (22)
- ha_deep_cascade_detail(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 9
  Associated lean decls (10)
- ha_quadratic_reconstruction_detail(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 9
  Associated lean decls (20)
- mathlib_prod_shear(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 9
  Associated lean decls (9)
- ha_ridgelet_transform(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 8
  Associated lean decls (1)
  - LeanRidgelet.JointEquivariantRidgelet
- ridgelet_transform_and_pairing(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 8
  Associated lean decls (10)
- fs_pairing_detail(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 7
  Associated lean decls (1)
  - LeanRidgelet.fourierSlicePairing
- mathlib_stiefel_codim_one(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 7
  Associated lean decls (5)
- ha_deep_feature(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 6
  Associated lean decls (5)
- l1_pairing_extension(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 6
  Associated lean decls (1)
  - LeanRidgelet.hasFourierAwayFromOrigin_pairing_extension
- mathlib_fourier_inversion_ae(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 6
  Associated lean decls (1)
  - MeasureTheory.Integrable.fourierInv_fourier_ae_eq
- abstract_solution_geometry(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (11)
- fs_symmetric_network(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (5)
- mathlib_units_haar(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (26)
- fourier_expressions(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 4
  Associated lean decls (4)
- l1_plancherel_lintegral(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 4
  Associated lean decls (4)
- mathlib_semidirect_haar(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 4
  Associated lean decls (12)
- canonical_solution_and_projection(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
  Associated lean decls (4)
- ha_quadratic_sobolev_space_detail(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
  Associated lean decls (23)
- l1_construction_admissible(Corollary)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
  Associated lean decls (3)
- l1_reconstruction(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
  Associated lean decls (1)
  - LeanRidgelet.l1_reconstruction_formula
- mathlib_diagonal_scaling(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
  Associated lean decls (7)
- mathlib_polynomial_growth(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
  Associated lean decls (8)
- measure_valued_synthesis_detail(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
- concrete_null_space_and_general_solution(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (6)
- fs_euclidean_detail(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (13)
- fs_finite_field_network(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (3)
- fs_symmetric_inversion(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (3)
- ha_depth_two_machine(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (5)
- l1_balancing_theorem(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (3)
- l1_dual_operator(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (1)
  - LeanRidgelet.l1_dualRidgeletTransform_pairing
- l1_lizorkin_quotient_invariance(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (1)
  - LeanRidgelet.l1_hasFourierAwayFromOrigin_add_polynomial
- l1_lizorkin_spaces(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
- mathlib_hyperbolic_helgason_fourier(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (11)
- mathlib_hyperbolic_mobius_measure(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (21)
- mathlib_svd(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (6)
- ridgelet_simple_tensor(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (2)
  - LeanRidgelet.ridgeletOperator_apply_ae
  - LeanRidgelet.fourierDilationTransform_ridgeletOperator_apply_ae
- ha_joint_equivariance_detail(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 40
  Associated lean decls (2)
  - LeanRidgelet.IsJointEquivariant
  - LeanRidgelet.IsEquivariant
- mathlib_quasi_invariant_integral(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 39
  Associated lean decls (2)
  - MeasureTheory.integral_eq_integral_smul_comp_smul_of_map_eq_withDensity
  - NNReal.smul_inv_sqrt_smul
- ha_reconstruction_commutant(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 22
  Associated lean decls (3)
- ha_schur_detail(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 22
  Associated lean decls (10)
- mathlib_dirichlet_integral(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 17
  Associated lean decls (7)
- ha_affine_representations(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 14
  Associated lean decls (4)
- weighted_dilation_identity(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 13
  Associated lean decls (1)
  - LeanRidgelet.integral_fourierDilationCoordinate_mul
- ha_quadratic_measure_detail(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 12
  Associated lean decls (13)
- mathlib_relatively_invariant_density(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 12
  Associated lean decls (2)
  - MeasureTheory.Measure.map_withDensity_of_map_eq_smul
  - MeasureTheory.Measure.map_restrict_of_map_eq_smul
- mathlib_symmetric_congruence_det(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 12
  Associated lean decls (10)
- parameter_space_and_unitary_transform(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 12
  Associated lean decls (4)
- mathlib_horocycle_radon(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 11
  Associated lean decls (6)
- mathlib_constant_density_preimage(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 10
  Associated lean decls (3)
- mathlib_fourier_affine(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 10
  Associated lean decls (6)
- mathlib_lp_unimodular_multiplier(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 10
  Associated lean decls (6)
- mathlib_polish_units(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 10
  Associated lean decls (1)
  - Units.instPolishSpaceOfNormedRing
- fs_dplane_fractional(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 9
  Associated lean decls (1)
  - LeanRidgelet.fs_fourier_dPlaneTransform_fractional
- fs_dplane_polar_codim_one(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 9
  Associated lean decls (2)
  - LeanRidgelet.norm_smul_coe_sphere
  - LeanRidgelet.fs_matrixPolarIntegration_codim_one
- ha_affine_frequency_detail(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 9
  Associated lean decls (14)
- mathlib_affine_semidirect(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 9
  Associated lean decls (20)
- mathlib_const_density_strong_continuity(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 9
  Associated lean decls (1)
  - UnitaryRepresentation.isStronglyContinuous_of_const_density
- mathlib_general_linear_orbit(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 9
  Associated lean decls (5)
- mathlib_unitary_character(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 9
  Associated lean decls (7)
- ha_quadratic_composite_detail(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 8
  Associated lean decls (8)
- mathlib_haar_prod_assoc(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 8
  Associated lean decls (5)
- mathlib_weighted_l1_smoothing(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 7
  Associated lean decls (11)
- ha_machine_intertwines(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
  Associated lean decls (4)
- ha_ridgelet_intertwines(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
  Associated lean decls (4)
- hilbert_space_synthesis(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
  Associated lean decls (5)
- l1_reconstruction_section(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
  Associated lean decls (9)
- adjoint_ridgelet_function(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 5
  Associated lean decls (4)
- angular_plancherel(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 5
  Associated lean decls (4)
- bounded_synthesis(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 5
  Associated lean decls (4)
- l1_gelfand_shilov_pairing(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 5
  Associated lean decls (3)
- l1_spectral_pairing(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 5
  Associated lean decls (6)
- mathlib_cholesky_diag(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 5
  Associated lean decls (10)
- mathlib_parametric_iterated_deriv(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 5
  Associated lean decls (15)
- concrete_adjoint(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (3)
- ha_parametric_deriv_measurable_detail(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (15)
- l1_truncation_limit(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (10)
- mathlib_lp_functor(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (14)
- relu_operator_theory(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (3)
- abstract_basis_expansion(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (6)
- fs_gconv_network(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (7)
- ha_affine_homogeneous_l2_detail(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (21)
- ha_fully_connected_detail(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (12)
- l1_fourier_slice_angular(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - LeanRidgelet.angularFourier_slice_radonTransform
- l1_lizorkin_moment_vanishing(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (2)
  - LeanRidgelet.integral_pow_mul_angularFourier1D_eq_zero
  - LeanRidgelet.integral_polynomial_mul_angularFourier1D_eq_zero
- l1_weak_ridgelet(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - LeanRidgelet.weakRidgeletTransform
- mathlib_haar_automorphism(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (2)
  - MeasureTheory.exists_map_continuousMulEquiv_haar_eq_smul_haar
  - MeasureTheory.exists_map_continuousMulEquiv_haar_restrict_eq_smul_haar_restrict
- mathlib_linear_surjection_haar(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (2)
  - MeasureTheory.map_snd_restrict_prod_le
  - LinearMap.exists_map_restrict_addHaar_le_smul_addHaar
- mathlib_orthogonal_complexification(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (11)
- mathlib_unitary_lp(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (12)
- mathlib_young_convolution(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (4)
- fs_gconv_reconstruction(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (5)
- ha_affine_classical_comparison_detail(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (14)
- ha_affine_homogeneous_quasiregular_detail(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (29)
- ha_deep_ridgelet(Corollary)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (2)
  - LeanRidgelet.deepRidgelet_reconstruction_formula
  - LeanRidgelet.deepRidgelet_normalized_rightInverse
- ha_fully_connected_feature(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (2)
  - LeanRidgelet.deepFullyConnectedFeature
  - LeanRidgelet.deepFullyConnectedFeature_endpoint_equivariant
- ha_fully_connected_l2_representation_detail(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (9)
- l1_bump_ridgelet_construction(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (8)
- mathlib_cyclic_fourier(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (10)
- mathlib_fourier_character_multiplier(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (12)
- mathlib_gaussian_schwartz(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (6)
- mathlib_general_linear_haar(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (18)
- mathlib_homogeneous_section_cocycle(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (14)
- mathlib_integrated_unitary_representation(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (13)
- mathlib_lipschitz_discretization(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (4)
- mathlib_lp_compact_multiplier(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (10)
- mathlib_lp_integrable_dense(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - MeasureTheory.Lp.dense_setOf_integrable
- mathlib_radon_schwartz_section(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (5)
- measure_valued_synthesis(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
- classical_ridgelet_agreement(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (6)
- classical_synthesis_agreement(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (4)
- fourier_dilation_core(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (5)
- fourier_dilation_unitary(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (3)
- fs_dplane_affine(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (10)
- fs_dplane_detail(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (3)
- fs_dplane_similitude(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (6)
- fs_finite_field_detail(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - LeanRidgelet.fs_finiteField_sum_slice
  - LeanRidgelet.fs_finiteField_synthesis_ridgelet
- fs_finite_field_steps(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (3)
- fs_gconv_projection_structural(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (5)
- fs_radon_classical(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - LeanRidgelet.fs_ae_ne_zero
  - LeanRidgelet.fs_radon_reconstruction_codim_one
- general_solution_kernel_translate(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - LeanRidgelet.networkSolution_iff_kernel_translate
- ha_affine_group_haar_detail(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (9)
- ha_affine_section_induction_detail(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (59)
- ha_bochner_preliminaries(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
- ha_classical_reconstruction(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (5)
- ha_group_convolution_detail(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (9)
- ha_group_convolution_reconstruction(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (3)
- ha_l2_integral_detail(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
- ha_quadratic_finite_width_detail(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (4)
- ha_quadratic_sobolev_carrier_detail(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (34)
- ha_vector_affine_irreducibility(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (3)
- l1_L2_extension(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - LeanRidgelet.l1_ridgeletTransform_L2_extension
- l1_fourier_data_convolution(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (6)
- l1_l2_duality_steps(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (7)
- l1_reconstruction_radon(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - LeanRidgelet.l1_reconstruction_formula_radon
  - LeanRidgelet.l1_radon_filtered_backprojection
- l1_truncated_power_admissible(Proposition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (8)
- mathlib_temperate_growth_rpow(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - Function.norm_iteratedFDerivWithin_rpow_le
  - Function.HasTemperateGrowth.rpow_of_le
- minimum_norm_solution(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - LeanRidgelet.normalizedNetworkRightInverse_unique_minimal
- normalized_finite_width_approximation(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - LeanRidgelet.l2_theorem_five_normalized_finite_width_approximation
- normalized_finite_width_null_approximation(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
- null_ridgelet_coefficients(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - LeanRidgelet.activationFiberFunctional_fiberCoefficient_eq_zero_of_mem_ker
- pointwise_null_space(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - LeanRidgelet.mem_ker_networkSynthesis_iff
  - LeanRidgelet.mem_ker_networkSynthesis_iff_fourierDilation
- ridgelet_series(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - LeanRidgelet.hasSum_ridgeletOperator_fiberCoefficient

Metadata

Metadata audit

Missing owner308

Missing effort308

Untagged308

Missing owner (308)

abstract_basis_expansion(Theorem)

Missing owner metadata.
Associated lean decls (6)
abstract_reconstruction(Theorem)

Missing owner metadata.
Associated lean decls (4)
abstract_solution_geometry(Theorem)

Missing owner metadata.
Associated lean decls (11)
abstract_synthesis_and_reconstruction(Definition)

Missing owner metadata.
Associated lean decls (2)
- LeanRidgelet.unitarySynthesis
- LeanRidgelet.unitaryRidgelet
activation_distributional_fourier_formulas(Theorem)

Missing owner metadata.
activation_fiber_dual_bound(Theorem)

Missing owner metadata.
Associated lean decls (2)
- LeanRidgelet.norm_activationFiberFunctional_le
- LeanRidgelet.activationFiberDualMap
activation_fiber_functional(Definition)

Missing owner metadata.
Associated lean decls (5)
activation_functional(Definition)

Missing owner metadata.
Associated lean decls (5)
activation_hilbert_structure(Proposition)

Missing owner metadata.
Associated lean decls (1)
- LeanRidgelet.l2_proposition_one_activation_hilbert_structure
activation_hilbert_structure_detail(Proposition)

Missing owner metadata.
Associated lean decls (2)
- LeanRidgelet.activationCoordinateEquiv
- LeanRidgelet.activationDistribution_injective
Show all 298 more entries missing owner
- activation_normalization(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.activationNormalization
- activation_normalization_positive(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.activationNormalization_pos
- activation_riesz_representer(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.activationRieszRepresenter
- activation_sobolev_inclusion(Theorem)
  
  Missing owner metadata.
- activation_space(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.ActivationSpace
  - LeanRidgelet.activationDistribution
- activation_space_detail(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.ActivationSpace
  - LeanRidgelet.activationDistribution
- adjoint_ridgelet_function(Definition)
  
  Missing owner metadata.
  Associated lean decls (4)
- adjoint_synthesis(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.adjoint_networkSynthesis
  - LeanRidgelet.networkSynthesis_comp_adjoint
- angular_fourier_convention(Definition)
  
  Missing owner metadata.
  Associated lean decls (3)
- angular_plancherel(Theorem)
  
  Missing owner metadata.
  Associated lean decls (4)
- bounded_network_synthesis(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.norm_networkSynthesis_le
  - LeanRidgelet.norm_networkSynthesis_apply_le
- bounded_synthesis(Theorem)
  
  Missing owner metadata.
  Associated lean decls (4)
- canonical_parameter_projection(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.networkVisibleProjection
- canonical_parameter_projection_properties(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.isIdempotentElem_networkVisibleProjection
  - LeanRidgelet.isSelfAdjoint_networkVisibleProjection
- canonical_parameter_projection_range_kernel(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.ker_networkVisibleProjection
  - LeanRidgelet.range_networkVisibleProjection
- canonical_solution_and_projection(Definition)
  
  Missing owner metadata.
  Associated lean decls (4)
- classical_ridgelet_agreement(Theorem)
  
  Missing owner metadata.
  Associated lean decls (6)
- classical_synthesis_agreement(Theorem)
  
  Missing owner metadata.
  Associated lean decls (4)
- coefficient_space(Definition)
  
  Missing owner metadata.
  Associated lean decls (4)
- coefficient_vector(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.fiberCoefficient
- concrete_adjoint(Lemma)
  
  Missing owner metadata.
  Associated lean decls (3)
- concrete_null_space_and_general_solution(Theorem)
  
  Missing owner metadata.
  Associated lean decls (6)
- concrete_reconstruction(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.l2_theorem_two_reconstruction
  - LeanRidgelet.networkSynthesis_comp_ridgeletOperator
- concrete_unitary_transform(Proposition)
  
  Missing owner metadata.
  Associated lean decls (6)
- core_transform_agrees_with_unitary(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.fourierDilationTransform_parameterSchwartzRealization
  - LeanRidgelet.fourierDilationTransform_parameterSchwartzRealization_apply_ae
- discretizable_ridgelet_null_elements(Corollary)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.l2_corollary_one_discretizable_ridgelet_null_elements
- discretizable_ridgelet_null_elements_detail(Corollary)
  
  Missing owner metadata.
- encoding_and_perturbative_readout(Theorem)
  
  Missing owner metadata.
- exact_finite_null_relations(Proposition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.l2_proposition_two_exact_finite_null_relations
- exact_finite_null_relations_detail(Proposition)
  
  Missing owner metadata.
- fiber_inner_product(Proposition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.fiberInner_self_eq_zero
  - LeanRidgelet.denseRange_fiberCore_coe
- fiber_space(Definition)
  
  Missing owner metadata.
  Associated lean decls (6)
- fourier_dilation_coordinate(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.frequencyDilation
  - LeanRidgelet.fourierDilationCoordinate
- fourier_dilation_core(Definition)
  
  Missing owner metadata.
  Associated lean decls (5)
- fourier_dilation_core_plancherel(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.fourierDilationTransformCore_norm_sq
  - LeanRidgelet.integral_fiberBaseNormSq_fourierDilationTransformFiberCore
- fourier_dilation_inverse(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.inverseFourierDilationTransform_apply_fourierDilationTransform
- fourier_dilation_unitary(Definition)
  
  Missing owner metadata.
  Associated lean decls (3)
- fourier_expressions(Lemma)
  
  Missing owner metadata.
  Associated lean decls (4)
- fourier_expressions_detail(Lemma)
  
  Missing owner metadata.
- fs_dplane_affine(Theorem)
  
  Missing owner metadata.
  Associated lean decls (10)
- fs_dplane_codim_one_detail(Theorem)
  
  Missing owner metadata.
  Associated lean decls (11)
- fs_dplane_detail(Theorem)
  
  Missing owner metadata.
  Associated lean decls (3)
- fs_dplane_fractional(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.fs_fourier_dPlaneTransform_fractional
- fs_dplane_inversion(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.fs_dPlaneInversion
- fs_dplane_polar_codim_one(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.norm_smul_coe_sphere
  - LeanRidgelet.fs_matrixPolarIntegration_codim_one
- fs_dplane_rubin(Theorem)
  
  Missing owner metadata.
- fs_dplane_similitude(Theorem)
  
  Missing owner metadata.
  Associated lean decls (6)
- fs_dplane_stiefel(Theorem)
  
  Missing owner metadata.
  Associated lean decls (9)
- fs_dplane_stiefel_codim_one(Theorem)
  
  Missing owner metadata.
  Associated lean decls (5)
- fs_dplane_transform(Definition)
  
  Missing owner metadata.
  Associated lean decls (6)
- fs_euclidean_agreement(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.fs_separationOfVariables_euclideanRidgeletTransform
  - LeanRidgelet.fs_admissibilityConstant_eq_fourierSlicePairing
- fs_euclidean_detail(Theorem)
  
  Missing owner metadata.
  Associated lean decls (13)
- fs_finite_field_detail(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.fs_finiteField_sum_slice
  - LeanRidgelet.fs_finiteField_synthesis_ridgelet
- fs_finite_field_mean_zero(Lemma)
  
  Missing owner metadata.
  Associated lean decls (4)
- fs_finite_field_network(Definition)
  
  Missing owner metadata.
  Associated lean decls (3)
- fs_finite_field_reconstruction(Theorem)
  
  Missing owner metadata.
  Associated lean decls (3)
- fs_finite_field_steps(Theorem)
  
  Missing owner metadata.
  Associated lean decls (3)
- fs_fourier_formula_classical(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.fs_fourierFormula_irieFunahashi
- fs_gconv_detail(Theorem)
  
  Missing owner metadata.
  Associated lean decls (3)
- fs_gconv_network(Definition)
  
  Missing owner metadata.
  Associated lean decls (7)
- fs_gconv_projection_structural(Theorem)
  
  Missing owner metadata.
  Associated lean decls (5)
- fs_gconv_reconstruction(Theorem)
  
  Missing owner metadata.
  Associated lean decls (5)
- fs_method(Theorem)
  
  Missing owner metadata.
  Associated lean decls (8)
- fs_pairing(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.fourierSlicePairing
- fs_pairing_algebra(Lemma)
  
  Missing owner metadata.
  Associated lean decls (4)
- fs_pairing_detail(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.fourierSlicePairing
- fs_radon_classical(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.fs_ae_ne_zero
  - LeanRidgelet.fs_radon_reconstruction_codim_one
- fs_reconstruction_euclidean(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.fs_inversionIntegral_euclidean
  - LeanRidgelet.fs_reconstruction_euclidean
- fs_scheme_detail(Theorem)
  
  Missing owner metadata.
  Associated lean decls (9)
- fs_symmetric_detail(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.horosphericalWeight_zero
  - LeanRidgelet.fs_symmetric_reconstruction_of_inversion
- fs_symmetric_hyperbolic(Definition)
  
  Missing owner metadata.
  Associated lean decls (21)
- fs_symmetric_inversion(Theorem)
  
  Missing owner metadata.
  Associated lean decls (3)
- fs_symmetric_network(Definition)
  
  Missing owner metadata.
  Associated lean decls (5)
- fs_symmetric_reconstruction(Theorem)
  
  Missing owner metadata.
  Associated lean decls (5)
- fs_symmetric_spd(Definition)
  
  Missing owner metadata.
  Associated lean decls (16)
- fs_target_fractional_derivative(Theorem)
  
  Missing owner metadata.
  Associated lean decls (7)
- fs_target_svd_jacobian(Lemma)
  
  Missing owner metadata.
  Associated lean decls (4)
- gaussian_activation(Proposition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.gaussianActivation
  - LeanRidgelet.gaussianActivation_ne_zero
- general_solution_kernel_translate(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.networkSolution_iff_kernel_translate
- ha_adjoint_reconstruction_detail(Theorem)
  
  Missing owner metadata.
  Associated lean decls (9)
- ha_affine_appendix(Theorem)
  
  Missing owner metadata.
- ha_affine_classical_comparison_detail(Theorem)
  
  Missing owner metadata.
  Associated lean decls (14)
- ha_affine_frequency_detail(Theorem)
  
  Missing owner metadata.
  Associated lean decls (14)
- ha_affine_group_haar_detail(Theorem)
  
  Missing owner metadata.
  Associated lean decls (9)
- ha_affine_homogeneous_l2_detail(Theorem)
  
  Missing owner metadata.
  Associated lean decls (21)
- ha_affine_homogeneous_quasiregular_detail(Definition)
  
  Missing owner metadata.
  Associated lean decls (29)
- ha_affine_irreducibility(Theorem)
  
  Missing owner metadata.
  Associated lean decls (19)
- ha_affine_jacobian_detail(Theorem)
  
  Missing owner metadata.
  Associated lean decls (11)
- ha_affine_lift_detail(Definition)
  
  Missing owner metadata.
  Associated lean decls (22)
- ha_affine_mackey_detail(Theorem)
  
  Missing owner metadata.
  Associated lean decls (18)
- ha_affine_representations(Definition)
  
  Missing owner metadata.
  Associated lean decls (4)
- ha_affine_section_induction_detail(Theorem)
  
  Missing owner metadata.
  Associated lean decls (59)
- ha_appendix_depth_two(Definition)
  
  Missing owner metadata.
- ha_architecture_detail(Theorem)
  
  Missing owner metadata.
- ha_bochner_intertwining_detail(Lemma)
  
  Missing owner metadata.
  Associated lean decls (17)
- ha_bochner_measurability_detail(Lemma)
  
  Missing owner metadata.
  Associated lean decls (11)
- ha_bochner_preliminaries(Lemma)
  
  Missing owner metadata.
- ha_boundedness_criteria(Lemma)
  
  Missing owner metadata.
- ha_classical_equivariance(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.IsEquivariant
  - LeanRidgelet.IsEquivariant.isJointEquivariant_of_fixed
- ha_classical_reconstruction(Theorem)
  
  Missing owner metadata.
  Associated lean decls (5)
- ha_deep_cascade_detail(Lemma)
  
  Missing owner metadata.
  Associated lean decls (10)
- ha_deep_feature(Lemma)
  
  Missing owner metadata.
  Associated lean decls (5)
- ha_deep_ridgelet(Corollary)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.deepRidgelet_reconstruction_formula
  - LeanRidgelet.deepRidgelet_normalized_rightInverse
- ha_depth_two_machine(Definition)
  
  Missing owner metadata.
  Associated lean decls (5)
- ha_fully_connected_detail(Lemma)
  
  Missing owner metadata.
  Associated lean decls (12)
- ha_fully_connected_feature(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.deepFullyConnectedFeature
  - LeanRidgelet.deepFullyConnectedFeature_endpoint_equivariant
- ha_fully_connected_l2_representation_detail(Lemma)
  
  Missing owner metadata.
  Associated lean decls (9)
- ha_group_convolution_detail(Theorem)
  
  Missing owner metadata.
  Associated lean decls (9)
- ha_group_convolution_reconstruction(Theorem)
  
  Missing owner metadata.
  Associated lean decls (3)
- ha_group_convolution_reduction(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.groupConvolutionalSynthesis_eq_orbit
  - LeanRidgelet.groupConvolutionalRidgelet_eq_base
- ha_induced_l2_detail(Definition)
  
  Missing owner metadata.
  Associated lean decls (16)
- ha_induced_representations(Definition)
  
  Missing owner metadata.
  Associated lean decls (3)
- ha_induced_unitarity(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.invariantLpUnitaryRepresentation
  - LeanRidgelet.quasiInvariantLpUnitaryRepresentation
- ha_intertwiner_operators(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.JointEquivariantMachine
  - LeanRidgelet.JointEquivariantRidgelet
- ha_joint_equivariance(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.IsJointEquivariant
- ha_joint_equivariance_constructors(Lemma)
  
  Missing owner metadata.
  Associated lean decls (5)
- ha_joint_equivariance_detail(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.IsJointEquivariant
  - LeanRidgelet.IsEquivariant
- ha_joint_machine(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.JointEquivariantMachine
- ha_l2_integral_detail(Theorem)
  
  Missing owner metadata.
- ha_l2_operator_bridge_detail(Definition)
  
  Missing owner metadata.
  Associated lean decls (4)
- ha_machine_intertwines(Lemma)
  
  Missing owner metadata.
  Associated lean decls (4)
- ha_main_reconstruction(Theorem)
  
  Missing owner metadata.
  Associated lean decls (3)
- ha_normalized_right_inverse(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.ha_normalizedRidgelet_rightInverse
- ha_orbit_feature(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.orbitFeature
  - LeanRidgelet.isJointEquivariant_orbitFeature
- ha_parametric_deriv_measurable_detail(Lemma)
  
  Missing owner metadata.
  Associated lean decls (15)
- ha_quadratic_composite_detail(Theorem)
  
  Missing owner metadata.
  Associated lean decls (8)
- ha_quadratic_detail(Lemma)
  
  Missing owner metadata.
  Associated lean decls (27)
- ha_quadratic_feature(Definition)
  
  Missing owner metadata.
  Associated lean decls (16)
- ha_quadratic_finite_width_detail(Theorem)
  
  Missing owner metadata.
  Associated lean decls (4)
- ha_quadratic_measure_detail(Theorem)
  
  Missing owner metadata.
  Associated lean decls (13)
- ha_quadratic_nonzero_detail(Theorem)
  
  Missing owner metadata.
  Associated lean decls (23)
- ha_quadratic_parameter_factor_detail(Lemma)
  
  Missing owner metadata.
  Associated lean decls (13)
- ha_quadratic_reconstruction_detail(Theorem)
  
  Missing owner metadata.
  Associated lean decls (20)
- ha_quadratic_relative_measure_detail(Theorem)
  
  Missing owner metadata.
  Associated lean decls (24)
- ha_quadratic_second_difference_detail(Theorem)
  
  Missing owner metadata.
  Associated lean decls (35)
- ha_quadratic_shear_detail(Lemma)
  
  Missing owner metadata.
  Associated lean decls (19)
- ha_quadratic_sobolev_carrier_detail(Lemma)
  
  Missing owner metadata.
  Associated lean decls (34)
- ha_quadratic_sobolev_fourier_detail(Lemma)
  
  Missing owner metadata.
  Associated lean decls (3)
- ha_quadratic_sobolev_space_detail(Lemma)
  
  Missing owner metadata.
  Associated lean decls (23)
- ha_quadratic_transfer_detail(Lemma)
  
  Missing owner metadata.
  Associated lean decls (5)
- ha_reconstruction_commutant(Lemma)
  
  Missing owner metadata.
  Associated lean decls (3)
- ha_reconstruction_detail(Theorem)
  
  Missing owner metadata.
  Associated lean decls (5)
- ha_ridgelet_intertwines(Lemma)
  
  Missing owner metadata.
  Associated lean decls (4)
- ha_ridgelet_transform(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.JointEquivariantRidgelet
- ha_schur_detail(Theorem)
  
  Missing owner metadata.
  Associated lean decls (10)
- ha_schur_lemma(Theorem)
  
  Missing owner metadata.
  Associated lean decls (3)
- ha_tensor_irreducibility(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.fullyConnectedLpUnitaryRepresentation_isTopologicallyIrreducible_of
- ha_uniform_discretization(Theorem)
  
  Missing owner metadata.
- ha_unitary_irreducibility(Definition)
  
  Missing owner metadata.
  Associated lean decls (3)
- ha_unitary_representation_detail(Definition)
  
  Missing owner metadata.
  Associated lean decls (4)
- ha_vector_affine_irreducibility(Lemma)
  
  Missing owner metadata.
  Associated lean decls (3)
- hilbert_space_synthesis(Definition)
  
  Missing owner metadata.
  Associated lean decls (5)
- inverse_fourier_dilation_core(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.inverseFourierDilationTransformCore
- japanese_bracket(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.japaneseBracketPow
- l1_L2_extension(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.l1_ridgeletTransform_L2_extension
- l1_activation_classes(Proposition)
  
  Missing owner metadata.
- l1_admissibility(Definition)
  
  Missing owner metadata.
  Associated lean decls (5)
- l1_admissibility_examples(Proposition)
  
  Missing owner metadata.
  Associated lean decls (3)
- l1_balancing_distributional_rows(Theorem)
  
  Missing owner metadata.
- l1_balancing_theorem(Theorem)
  
  Missing owner metadata.
  Associated lean decls (3)
- l1_bump_ridgelet_construction(Lemma)
  
  Missing owner metadata.
  Associated lean decls (8)
- l1_construction_admissible(Corollary)
  
  Missing owner metadata.
  Associated lean decls (3)
- l1_continuity_L1_Linfty(Proposition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.norm_euclideanRidgeletTransform_zero_le
  - LeanRidgelet.l1_ridgeletTransform_bounded_L1_Linfty
- l1_dual_operator(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.l1_dualRidgeletTransform_pairing
- l1_fourier_away_from_origin(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - MeasureTheory.PolynomiallyBounded
  - LeanRidgelet.HasFourierAwayFromOrigin
- l1_fourier_data_convolution(Lemma)
  
  Missing owner metadata.
  Associated lean decls (6)
- l1_fourier_expression(Theorem)
  
  Missing owner metadata.
  Associated lean decls (4)
- l1_fourier_slice_angular(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.angularFourier_slice_radonTransform
- l1_fractional_laplacian_intertwining(Corollary)
  
  Missing owner metadata.
- l1_gelfand_shilov_pairing(Lemma)
  
  Missing owner metadata.
  Associated lean decls (3)
- l1_l2_duality_steps(Lemma)
  
  Missing owner metadata.
  Associated lean decls (7)
- l1_lambda_multiplier(Theorem)
  
  Missing owner metadata.
  Associated lean decls (11)
- l1_lizorkin_moment_vanishing(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.integral_pow_mul_angularFourier1D_eq_zero
  - LeanRidgelet.integral_polynomial_mul_angularFourier1D_eq_zero
- l1_lizorkin_quotient_invariance(Proposition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.l1_hasFourierAwayFromOrigin_add_polynomial
- l1_lizorkin_spaces(Definition)
  
  Missing owner metadata.
- l1_pairing_extension(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.hasFourierAwayFromOrigin_pairing_extension
- l1_parameter_space(Definition)
  
  Missing owner metadata.
  Associated lean decls (4)
- l1_parseval_plancherel(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.l1_plancherel_identity
  - LeanRidgelet.l1_parseval_relation
- l1_plancherel_lintegral(Lemma)
  
  Missing owner metadata.
  Associated lean decls (4)
- l1_radon_backprojection(Definition)
  
  Missing owner metadata.
  Associated lean decls (3)
- l1_reconstruction(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.l1_reconstruction_formula
- l1_reconstruction_L2(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.l1_reconstruction_formula_L2
- l1_reconstruction_moment_layer(Lemma)
  
  Missing owner metadata.
  Associated lean decls (4)
- l1_reconstruction_radon(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.l1_reconstruction_formula_radon
  - LeanRidgelet.l1_radon_filtered_backprojection
- l1_reconstruction_section(Lemma)
  
  Missing owner metadata.
  Associated lean decls (9)
- l1_relu_universality(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.l1_relu_network_universal_approximation
- l1_ridgelet_transforms(Definition)
  
  Missing owner metadata.
  Associated lean decls (4)
- l1_spectral_pairing(Lemma)
  
  Missing owner metadata.
  Associated lean decls (6)
- l1_standard_activations(Definition)
  
  Missing owner metadata.
  Associated lean decls (3)
- l1_structure_theorem(Theorem)
  
  Missing owner metadata.
  Associated lean decls (4)
- l1_truncated_power_admissible(Proposition)
  
  Missing owner metadata.
  Associated lean decls (8)
- l1_truncated_power_fourier(Proposition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.l1_truncatedPower_hasFourierAwayFromOrigin
- l1_truncation_limit(Lemma)
  
  Missing owner metadata.
  Associated lean decls (10)
- l1_weak_ridgelet(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.weakRidgeletTransform
- mathlib_affine_haar(Theorem)
  
  Missing owner metadata.
  Associated lean decls (6)
- mathlib_affine_semidirect(Theorem)
  
  Missing owner metadata.
  Associated lean decls (20)
- mathlib_bochner_integral_l2(Theorem)
  
  Missing owner metadata.
  Associated lean decls (4)
- mathlib_cholesky_diag(Theorem)
  
  Missing owner metadata.
  Associated lean decls (10)
- mathlib_const_density_strong_continuity(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - UnitaryRepresentation.isStronglyContinuous_of_const_density
- mathlib_constant_density_preimage(Theorem)
  
  Missing owner metadata.
  Associated lean decls (3)
- mathlib_corner_det(Theorem)
  
  Missing owner metadata.
  Associated lean decls (23)
- mathlib_cyclic_fourier(Theorem)
  
  Missing owner metadata.
  Associated lean decls (10)
- mathlib_diagonal_scaling(Theorem)
  
  Missing owner metadata.
  Associated lean decls (7)
- mathlib_dirichlet_integral(Theorem)
  
  Missing owner metadata.
  Associated lean decls (7)
- mathlib_dplane_transform(Theorem)
  
  Missing owner metadata.
  Associated lean decls (23)
- mathlib_fourier_affine(Theorem)
  
  Missing owner metadata.
  Associated lean decls (6)
- mathlib_fourier_character_multiplier(Theorem)
  
  Missing owner metadata.
  Associated lean decls (12)
- mathlib_fourier_inversion_ae(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - MeasureTheory.Integrable.fourierInv_fourier_ae_eq
- mathlib_fourier_plancherel(Theorem)
  
  Missing owner metadata.
  Associated lean decls (7)
- mathlib_fourier_slice(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - MeasureTheory.fourier_slice_radonTransform
- mathlib_gaussian_schwartz(Theorem)
  
  Missing owner metadata.
  Associated lean decls (6)
- mathlib_general_linear_haar(Theorem)
  
  Missing owner metadata.
  Associated lean decls (18)
- mathlib_general_linear_orbit(Theorem)
  
  Missing owner metadata.
  Associated lean decls (5)
- mathlib_group_convolution_continuity(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - MeasureTheory.continuous_integral_compact_mul_right
- mathlib_haar_automorphism(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - MeasureTheory.exists_map_continuousMulEquiv_haar_eq_smul_haar
  - MeasureTheory.exists_map_continuousMulEquiv_haar_restrict_eq_smul_haar_restrict
- mathlib_haar_prod_assoc(Theorem)
  
  Missing owner metadata.
  Associated lean decls (5)
- mathlib_helgason_inversion(Theorem)
  
  Missing owner metadata.
  Associated lean decls (9)
- mathlib_hilbert_schmidt_kernel(Theorem)
  
  Missing owner metadata.
  Associated lean decls (22)
- mathlib_hilbert_symbol(Theorem)
  
  Missing owner metadata.
  Associated lean decls (11)
- mathlib_homogeneous_section_cocycle(Theorem)
  
  Missing owner metadata.
  Associated lean decls (14)
- mathlib_horocycle_radon(Theorem)
  
  Missing owner metadata.
  Associated lean decls (6)
- mathlib_hyperbolic_ball(Theorem)
  
  Missing owner metadata.
  Associated lean decls (16)
- mathlib_hyperbolic_boundary_mobius(Theorem)
  
  Missing owner metadata.
  Associated lean decls (19)
- mathlib_hyperbolic_helgason_fourier(Theorem)
  
  Missing owner metadata.
  Associated lean decls (11)
- mathlib_hyperbolic_mobius(Theorem)
  
  Missing owner metadata.
  Associated lean decls (21)
- mathlib_hyperbolic_mobius_measure(Theorem)
  
  Missing owner metadata.
  Associated lean decls (21)
- mathlib_integrated_unitary_representation(Theorem)
  
  Missing owner metadata.
  Associated lean decls (13)
- mathlib_iterated_fubini(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - MeasureTheory.integral_integral_integral_swap_left
  - MeasureTheory.integral_integral_integral_swap_right
- mathlib_l2_duality(Theorem)
  
  Missing owner metadata.
  Associated lean decls (7)
- mathlib_linear_surjection_haar(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - MeasureTheory.map_snd_restrict_prod_le
  - LinearMap.exists_map_restrict_addHaar_le_smul_addHaar
- mathlib_lipschitz_discretization(Theorem)
  
  Missing owner metadata.
  Associated lean decls (4)
- mathlib_lizorkin_space(Definition)
  
  Missing owner metadata.
  Associated lean decls (9)
- mathlib_lp_compact_multiplier(Theorem)
  
  Missing owner metadata.
  Associated lean decls (10)
- mathlib_lp_functor(Theorem)
  
  Missing owner metadata.
  Associated lean decls (14)
- mathlib_lp_indicator(Theorem)
  
  Missing owner metadata.
  Associated lean decls (12)
- mathlib_lp_integrable_dense(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - MeasureTheory.Lp.dense_setOf_integrable
- mathlib_lp_operator_of_pointwise(Theorem)
  
  Missing owner metadata.
  Associated lean decls (6)
- mathlib_lp_unimodular_multiplier(Theorem)
  
  Missing owner metadata.
  Associated lean decls (6)
- mathlib_matrix_polar(Theorem)
  
  Missing owner metadata.
  Associated lean decls (11)
- mathlib_orthogonal_complexification(Theorem)
  
  Missing owner metadata.
  Associated lean decls (11)
- mathlib_orthogonal_group(Theorem)
  
  Missing owner metadata.
  Associated lean decls (21)
- mathlib_parametric_iterated_deriv(Theorem)
  
  Missing owner metadata.
  Associated lean decls (15)
- mathlib_polar_coordinates(Theorem)
  
  Missing owner metadata.
  Associated lean decls (15)
- mathlib_polish_units(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Units.instPolishSpaceOfNormedRing
- mathlib_polynomial_growth(Theorem)
  
  Missing owner metadata.
  Associated lean decls (8)
- mathlib_prod_shear(Theorem)
  
  Missing owner metadata.
  Associated lean decls (9)
- mathlib_quasi_invariant_integral(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - MeasureTheory.integral_eq_integral_smul_comp_smul_of_map_eq_withDensity
  - NNReal.smul_inv_sqrt_smul
- mathlib_radon_l1_theory(Theorem)
  
  Missing owner metadata.
  Associated lean decls (6)
- mathlib_radon_schwartz_section(Theorem)
  
  Missing owner metadata.
  Associated lean decls (5)
- mathlib_radon_transform(Definition)
  
  Missing owner metadata.
  Associated lean decls (3)
- mathlib_relatively_invariant_density(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - MeasureTheory.Measure.map_withDensity_of_map_eq_smul
  - MeasureTheory.Measure.map_restrict_of_map_eq_smul
- mathlib_schwartz_aux(Theorem)
  
  Missing owner metadata.
  Associated lean decls (6)
- mathlib_semidirect_haar(Theorem)
  
  Missing owner metadata.
  Associated lean decls (12)
- mathlib_spd_boundary(Theorem)
  
  Missing owner metadata.
  Associated lean decls (6)
- mathlib_spd_cfunction(Theorem)
  
  Missing owner metadata.
  Associated lean decls (31)
- mathlib_spd_model(Theorem)
  
  Missing owner metadata.
  Associated lean decls (23)
- mathlib_sphere_invariant_measure(Theorem)
  
  Missing owner metadata.
  Associated lean decls (15)
- mathlib_stiefel_codim_one(Theorem)
  
  Missing owner metadata.
  Associated lean decls (5)
- mathlib_svd(Theorem)
  
  Missing owner metadata.
  Associated lean decls (6)
- mathlib_symmetric_cocycle(Theorem)
  
  Missing owner metadata.
  Associated lean decls (7)
- mathlib_symmetric_congruence_det(Theorem)
  
  Missing owner metadata.
  Associated lean decls (10)
- mathlib_symmetric_space_defs(Theorem)
  
  Missing owner metadata.
  Associated lean decls (15)
- mathlib_temperate_growth_rpow(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - Function.norm_iteratedFDerivWithin_rpow_le
  - Function.HasTemperateGrowth.rpow_of_le
- mathlib_unitary_character(Theorem)
  
  Missing owner metadata.
  Associated lean decls (7)
- mathlib_unitary_conjugation(Theorem)
  
  Missing owner metadata.
  Associated lean decls (14)
- mathlib_unitary_lp(Theorem)
  
  Missing owner metadata.
  Associated lean decls (12)
- mathlib_units_haar(Theorem)
  
  Missing owner metadata.
  Associated lean decls (26)
- mathlib_weighted_l1_smoothing(Theorem)
  
  Missing owner metadata.
  Associated lean decls (11)
- mathlib_weighted_sobolev_one_dim(Theorem)
  
  Missing owner metadata.
  Associated lean decls (8)
- mathlib_young_convolution(Theorem)
  
  Missing owner metadata.
  Associated lean decls (4)
- measure_valued_synthesis(Definition)
  
  Missing owner metadata.
- measure_valued_synthesis_detail(Definition)
  
  Missing owner metadata.
- minimum_norm_solution(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.normalizedNetworkRightInverse_unique_minimal
- network_synthesis(Definition)
  
  Missing owner metadata.
  Associated lean decls (4)
- normalized_finite_width_approximation(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.l2_theorem_five_normalized_finite_width_approximation
- normalized_finite_width_null_approximation(Theorem)
  
  Missing owner metadata.
- normalized_network_right_inverse(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.normalizedNetworkRightInverse
- normalized_network_right_inverse_spec(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.normalizedNetworkRightInverse_rightInverse
  - LeanRidgelet.surjective_networkSynthesis
- null_ridgelet_coefficients(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.activationFiberFunctional_fiberCoefficient_eq_zero_of_mem_ker
- null_space_encoding_and_perturbations(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.l2_theorem_four_encoding_and_perturbative_readout
- null_space_structure(Theorem)
  
  Missing owner metadata.
  Associated lean decls (4)
- parameter_space(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.ParameterSpace
  - LeanRidgelet.parameterCoordinateEquiv
- parameter_space_and_unitary_transform(Definition)
  
  Missing owner metadata.
  Associated lean decls (4)
- pointwise_coordinate_transform(Definition)
  
  Missing owner metadata.
  Associated lean decls (4)
- pointwise_null_space(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.mem_ker_networkSynthesis_iff
  - LeanRidgelet.mem_ker_networkSynthesis_iff_fourierDilation
- relu_activation(Proposition)
  
  Missing owner metadata.
  Associated lean decls (5)
- relu_operator_theory(Proposition)
  
  Missing owner metadata.
  Associated lean decls (3)
- ridgelet_operator(Definition)
  
  Missing owner metadata.
  Associated lean decls (8)
- ridgelet_reconstruction(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.networkSynthesis_comp_ridgeletOperator
- ridgelet_series(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.hasSum_ridgeletOperator_fiberCoefficient
- ridgelet_simple_tensor(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.ridgeletOperator_apply_ae
  - LeanRidgelet.fourierDilationTransform_ridgeletOperator_apply_ae
- ridgelet_transform_and_pairing(Definition)
  
  Missing owner metadata.
  Associated lean decls (10)
- standard_activation_riesz_resolvents(Theorem)
  
  Missing owner metadata.
- tanh_activation(Proposition)
  
  Missing owner metadata.
  Associated lean decls (5)
- tanh_operator_theory(Proposition)
  
  Missing owner metadata.
  Associated lean decls (3)
- truncated_monte_carlo_quadrature(Lemma)
  
  Missing owner metadata.
- weighted_dilation_change_of_variables(Lemma)
  
  Missing owner metadata.
  Associated lean decls (2)
  - LeanRidgelet.integral_fourierDilationCoordinate_mul
  - LeanRidgelet.integrable_fourierDilationCoordinate_mul
- weighted_dilation_identity(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanRidgelet.integral_fourierDilationCoordinate_mul

Missing effort (308)

abstract_basis_expansion(Theorem)

Missing effort metadata.
Associated lean decls (6)
abstract_reconstruction(Theorem)

Missing effort metadata.
Associated lean decls (4)
abstract_solution_geometry(Theorem)

Missing effort metadata.
Associated lean decls (11)
abstract_synthesis_and_reconstruction(Definition)

Missing effort metadata.
Associated lean decls (2)
- LeanRidgelet.unitarySynthesis
- LeanRidgelet.unitaryRidgelet
activation_distributional_fourier_formulas(Theorem)

Missing effort metadata.
activation_fiber_dual_bound(Theorem)

Missing effort metadata.
Associated lean decls (2)
- LeanRidgelet.norm_activationFiberFunctional_le
- LeanRidgelet.activationFiberDualMap
activation_fiber_functional(Definition)

Missing effort metadata.
Associated lean decls (5)
activation_functional(Definition)

Missing effort metadata.
Associated lean decls (5)
activation_hilbert_structure(Proposition)

Missing effort metadata.
Associated lean decls (1)
- LeanRidgelet.l2_proposition_one_activation_hilbert_structure
activation_hilbert_structure_detail(Proposition)

Missing effort metadata.
Associated lean decls (2)
- LeanRidgelet.activationCoordinateEquiv
- LeanRidgelet.activationDistribution_injective
Show all 298 more entries missing effort
- activation_normalization(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.activationNormalization
- activation_normalization_positive(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.activationNormalization_pos
- activation_riesz_representer(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.activationRieszRepresenter
- activation_sobolev_inclusion(Theorem)
  
  Missing effort metadata.
- activation_space(Definition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.ActivationSpace
  - LeanRidgelet.activationDistribution
- activation_space_detail(Definition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.ActivationSpace
  - LeanRidgelet.activationDistribution
- adjoint_ridgelet_function(Definition)
  
  Missing effort metadata.
  Associated lean decls (4)
- adjoint_synthesis(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.adjoint_networkSynthesis
  - LeanRidgelet.networkSynthesis_comp_adjoint
- angular_fourier_convention(Definition)
  
  Missing effort metadata.
  Associated lean decls (3)
- angular_plancherel(Theorem)
  
  Missing effort metadata.
  Associated lean decls (4)
- bounded_network_synthesis(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.norm_networkSynthesis_le
  - LeanRidgelet.norm_networkSynthesis_apply_le
- bounded_synthesis(Theorem)
  
  Missing effort metadata.
  Associated lean decls (4)
- canonical_parameter_projection(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.networkVisibleProjection
- canonical_parameter_projection_properties(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.isIdempotentElem_networkVisibleProjection
  - LeanRidgelet.isSelfAdjoint_networkVisibleProjection
- canonical_parameter_projection_range_kernel(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.ker_networkVisibleProjection
  - LeanRidgelet.range_networkVisibleProjection
- canonical_solution_and_projection(Definition)
  
  Missing effort metadata.
  Associated lean decls (4)
- classical_ridgelet_agreement(Theorem)
  
  Missing effort metadata.
  Associated lean decls (6)
- classical_synthesis_agreement(Theorem)
  
  Missing effort metadata.
  Associated lean decls (4)
- coefficient_space(Definition)
  
  Missing effort metadata.
  Associated lean decls (4)
- coefficient_vector(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.fiberCoefficient
- concrete_adjoint(Lemma)
  
  Missing effort metadata.
  Associated lean decls (3)
- concrete_null_space_and_general_solution(Theorem)
  
  Missing effort metadata.
  Associated lean decls (6)
- concrete_reconstruction(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.l2_theorem_two_reconstruction
  - LeanRidgelet.networkSynthesis_comp_ridgeletOperator
- concrete_unitary_transform(Proposition)
  
  Missing effort metadata.
  Associated lean decls (6)
- core_transform_agrees_with_unitary(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.fourierDilationTransform_parameterSchwartzRealization
  - LeanRidgelet.fourierDilationTransform_parameterSchwartzRealization_apply_ae
- discretizable_ridgelet_null_elements(Corollary)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.l2_corollary_one_discretizable_ridgelet_null_elements
- discretizable_ridgelet_null_elements_detail(Corollary)
  
  Missing effort metadata.
- encoding_and_perturbative_readout(Theorem)
  
  Missing effort metadata.
- exact_finite_null_relations(Proposition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.l2_proposition_two_exact_finite_null_relations
- exact_finite_null_relations_detail(Proposition)
  
  Missing effort metadata.
- fiber_inner_product(Proposition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.fiberInner_self_eq_zero
  - LeanRidgelet.denseRange_fiberCore_coe
- fiber_space(Definition)
  
  Missing effort metadata.
  Associated lean decls (6)
- fourier_dilation_coordinate(Definition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.frequencyDilation
  - LeanRidgelet.fourierDilationCoordinate
- fourier_dilation_core(Definition)
  
  Missing effort metadata.
  Associated lean decls (5)
- fourier_dilation_core_plancherel(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.fourierDilationTransformCore_norm_sq
  - LeanRidgelet.integral_fiberBaseNormSq_fourierDilationTransformFiberCore
- fourier_dilation_inverse(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.inverseFourierDilationTransform_apply_fourierDilationTransform
- fourier_dilation_unitary(Definition)
  
  Missing effort metadata.
  Associated lean decls (3)
- fourier_expressions(Lemma)
  
  Missing effort metadata.
  Associated lean decls (4)
- fourier_expressions_detail(Lemma)
  
  Missing effort metadata.
- fs_dplane_affine(Theorem)
  
  Missing effort metadata.
  Associated lean decls (10)
- fs_dplane_codim_one_detail(Theorem)
  
  Missing effort metadata.
  Associated lean decls (11)
- fs_dplane_detail(Theorem)
  
  Missing effort metadata.
  Associated lean decls (3)
- fs_dplane_fractional(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.fs_fourier_dPlaneTransform_fractional
- fs_dplane_inversion(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.fs_dPlaneInversion
- fs_dplane_polar_codim_one(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.norm_smul_coe_sphere
  - LeanRidgelet.fs_matrixPolarIntegration_codim_one
- fs_dplane_rubin(Theorem)
  
  Missing effort metadata.
- fs_dplane_similitude(Theorem)
  
  Missing effort metadata.
  Associated lean decls (6)
- fs_dplane_stiefel(Theorem)
  
  Missing effort metadata.
  Associated lean decls (9)
- fs_dplane_stiefel_codim_one(Theorem)
  
  Missing effort metadata.
  Associated lean decls (5)
- fs_dplane_transform(Definition)
  
  Missing effort metadata.
  Associated lean decls (6)
- fs_euclidean_agreement(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.fs_separationOfVariables_euclideanRidgeletTransform
  - LeanRidgelet.fs_admissibilityConstant_eq_fourierSlicePairing
- fs_euclidean_detail(Theorem)
  
  Missing effort metadata.
  Associated lean decls (13)
- fs_finite_field_detail(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.fs_finiteField_sum_slice
  - LeanRidgelet.fs_finiteField_synthesis_ridgelet
- fs_finite_field_mean_zero(Lemma)
  
  Missing effort metadata.
  Associated lean decls (4)
- fs_finite_field_network(Definition)
  
  Missing effort metadata.
  Associated lean decls (3)
- fs_finite_field_reconstruction(Theorem)
  
  Missing effort metadata.
  Associated lean decls (3)
- fs_finite_field_steps(Theorem)
  
  Missing effort metadata.
  Associated lean decls (3)
- fs_fourier_formula_classical(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.fs_fourierFormula_irieFunahashi
- fs_gconv_detail(Theorem)
  
  Missing effort metadata.
  Associated lean decls (3)
- fs_gconv_network(Definition)
  
  Missing effort metadata.
  Associated lean decls (7)
- fs_gconv_projection_structural(Theorem)
  
  Missing effort metadata.
  Associated lean decls (5)
- fs_gconv_reconstruction(Theorem)
  
  Missing effort metadata.
  Associated lean decls (5)
- fs_method(Theorem)
  
  Missing effort metadata.
  Associated lean decls (8)
- fs_pairing(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.fourierSlicePairing
- fs_pairing_algebra(Lemma)
  
  Missing effort metadata.
  Associated lean decls (4)
- fs_pairing_detail(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.fourierSlicePairing
- fs_radon_classical(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.fs_ae_ne_zero
  - LeanRidgelet.fs_radon_reconstruction_codim_one
- fs_reconstruction_euclidean(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.fs_inversionIntegral_euclidean
  - LeanRidgelet.fs_reconstruction_euclidean
- fs_scheme_detail(Theorem)
  
  Missing effort metadata.
  Associated lean decls (9)
- fs_symmetric_detail(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.horosphericalWeight_zero
  - LeanRidgelet.fs_symmetric_reconstruction_of_inversion
- fs_symmetric_hyperbolic(Definition)
  
  Missing effort metadata.
  Associated lean decls (21)
- fs_symmetric_inversion(Theorem)
  
  Missing effort metadata.
  Associated lean decls (3)
- fs_symmetric_network(Definition)
  
  Missing effort metadata.
  Associated lean decls (5)
- fs_symmetric_reconstruction(Theorem)
  
  Missing effort metadata.
  Associated lean decls (5)
- fs_symmetric_spd(Definition)
  
  Missing effort metadata.
  Associated lean decls (16)
- fs_target_fractional_derivative(Theorem)
  
  Missing effort metadata.
  Associated lean decls (7)
- fs_target_svd_jacobian(Lemma)
  
  Missing effort metadata.
  Associated lean decls (4)
- gaussian_activation(Proposition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.gaussianActivation
  - LeanRidgelet.gaussianActivation_ne_zero
- general_solution_kernel_translate(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.networkSolution_iff_kernel_translate
- ha_adjoint_reconstruction_detail(Theorem)
  
  Missing effort metadata.
  Associated lean decls (9)
- ha_affine_appendix(Theorem)
  
  Missing effort metadata.
- ha_affine_classical_comparison_detail(Theorem)
  
  Missing effort metadata.
  Associated lean decls (14)
- ha_affine_frequency_detail(Theorem)
  
  Missing effort metadata.
  Associated lean decls (14)
- ha_affine_group_haar_detail(Theorem)
  
  Missing effort metadata.
  Associated lean decls (9)
- ha_affine_homogeneous_l2_detail(Theorem)
  
  Missing effort metadata.
  Associated lean decls (21)
- ha_affine_homogeneous_quasiregular_detail(Definition)
  
  Missing effort metadata.
  Associated lean decls (29)
- ha_affine_irreducibility(Theorem)
  
  Missing effort metadata.
  Associated lean decls (19)
- ha_affine_jacobian_detail(Theorem)
  
  Missing effort metadata.
  Associated lean decls (11)
- ha_affine_lift_detail(Definition)
  
  Missing effort metadata.
  Associated lean decls (22)
- ha_affine_mackey_detail(Theorem)
  
  Missing effort metadata.
  Associated lean decls (18)
- ha_affine_representations(Definition)
  
  Missing effort metadata.
  Associated lean decls (4)
- ha_affine_section_induction_detail(Theorem)
  
  Missing effort metadata.
  Associated lean decls (59)
- ha_appendix_depth_two(Definition)
  
  Missing effort metadata.
- ha_architecture_detail(Theorem)
  
  Missing effort metadata.
- ha_bochner_intertwining_detail(Lemma)
  
  Missing effort metadata.
  Associated lean decls (17)
- ha_bochner_measurability_detail(Lemma)
  
  Missing effort metadata.
  Associated lean decls (11)
- ha_bochner_preliminaries(Lemma)
  
  Missing effort metadata.
- ha_boundedness_criteria(Lemma)
  
  Missing effort metadata.
- ha_classical_equivariance(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.IsEquivariant
  - LeanRidgelet.IsEquivariant.isJointEquivariant_of_fixed
- ha_classical_reconstruction(Theorem)
  
  Missing effort metadata.
  Associated lean decls (5)
- ha_deep_cascade_detail(Lemma)
  
  Missing effort metadata.
  Associated lean decls (10)
- ha_deep_feature(Lemma)
  
  Missing effort metadata.
  Associated lean decls (5)
- ha_deep_ridgelet(Corollary)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.deepRidgelet_reconstruction_formula
  - LeanRidgelet.deepRidgelet_normalized_rightInverse
- ha_depth_two_machine(Definition)
  
  Missing effort metadata.
  Associated lean decls (5)
- ha_fully_connected_detail(Lemma)
  
  Missing effort metadata.
  Associated lean decls (12)
- ha_fully_connected_feature(Definition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.deepFullyConnectedFeature
  - LeanRidgelet.deepFullyConnectedFeature_endpoint_equivariant
- ha_fully_connected_l2_representation_detail(Lemma)
  
  Missing effort metadata.
  Associated lean decls (9)
- ha_group_convolution_detail(Theorem)
  
  Missing effort metadata.
  Associated lean decls (9)
- ha_group_convolution_reconstruction(Theorem)
  
  Missing effort metadata.
  Associated lean decls (3)
- ha_group_convolution_reduction(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.groupConvolutionalSynthesis_eq_orbit
  - LeanRidgelet.groupConvolutionalRidgelet_eq_base
- ha_induced_l2_detail(Definition)
  
  Missing effort metadata.
  Associated lean decls (16)
- ha_induced_representations(Definition)
  
  Missing effort metadata.
  Associated lean decls (3)
- ha_induced_unitarity(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.invariantLpUnitaryRepresentation
  - LeanRidgelet.quasiInvariantLpUnitaryRepresentation
- ha_intertwiner_operators(Definition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.JointEquivariantMachine
  - LeanRidgelet.JointEquivariantRidgelet
- ha_joint_equivariance(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.IsJointEquivariant
- ha_joint_equivariance_constructors(Lemma)
  
  Missing effort metadata.
  Associated lean decls (5)
- ha_joint_equivariance_detail(Definition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.IsJointEquivariant
  - LeanRidgelet.IsEquivariant
- ha_joint_machine(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.JointEquivariantMachine
- ha_l2_integral_detail(Theorem)
  
  Missing effort metadata.
- ha_l2_operator_bridge_detail(Definition)
  
  Missing effort metadata.
  Associated lean decls (4)
- ha_machine_intertwines(Lemma)
  
  Missing effort metadata.
  Associated lean decls (4)
- ha_main_reconstruction(Theorem)
  
  Missing effort metadata.
  Associated lean decls (3)
- ha_normalized_right_inverse(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.ha_normalizedRidgelet_rightInverse
- ha_orbit_feature(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.orbitFeature
  - LeanRidgelet.isJointEquivariant_orbitFeature
- ha_parametric_deriv_measurable_detail(Lemma)
  
  Missing effort metadata.
  Associated lean decls (15)
- ha_quadratic_composite_detail(Theorem)
  
  Missing effort metadata.
  Associated lean decls (8)
- ha_quadratic_detail(Lemma)
  
  Missing effort metadata.
  Associated lean decls (27)
- ha_quadratic_feature(Definition)
  
  Missing effort metadata.
  Associated lean decls (16)
- ha_quadratic_finite_width_detail(Theorem)
  
  Missing effort metadata.
  Associated lean decls (4)
- ha_quadratic_measure_detail(Theorem)
  
  Missing effort metadata.
  Associated lean decls (13)
- ha_quadratic_nonzero_detail(Theorem)
  
  Missing effort metadata.
  Associated lean decls (23)
- ha_quadratic_parameter_factor_detail(Lemma)
  
  Missing effort metadata.
  Associated lean decls (13)
- ha_quadratic_reconstruction_detail(Theorem)
  
  Missing effort metadata.
  Associated lean decls (20)
- ha_quadratic_relative_measure_detail(Theorem)
  
  Missing effort metadata.
  Associated lean decls (24)
- ha_quadratic_second_difference_detail(Theorem)
  
  Missing effort metadata.
  Associated lean decls (35)
- ha_quadratic_shear_detail(Lemma)
  
  Missing effort metadata.
  Associated lean decls (19)
- ha_quadratic_sobolev_carrier_detail(Lemma)
  
  Missing effort metadata.
  Associated lean decls (34)
- ha_quadratic_sobolev_fourier_detail(Lemma)
  
  Missing effort metadata.
  Associated lean decls (3)
- ha_quadratic_sobolev_space_detail(Lemma)
  
  Missing effort metadata.
  Associated lean decls (23)
- ha_quadratic_transfer_detail(Lemma)
  
  Missing effort metadata.
  Associated lean decls (5)
- ha_reconstruction_commutant(Lemma)
  
  Missing effort metadata.
  Associated lean decls (3)
- ha_reconstruction_detail(Theorem)
  
  Missing effort metadata.
  Associated lean decls (5)
- ha_ridgelet_intertwines(Lemma)
  
  Missing effort metadata.
  Associated lean decls (4)
- ha_ridgelet_transform(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.JointEquivariantRidgelet
- ha_schur_detail(Theorem)
  
  Missing effort metadata.
  Associated lean decls (10)
- ha_schur_lemma(Theorem)
  
  Missing effort metadata.
  Associated lean decls (3)
- ha_tensor_irreducibility(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.fullyConnectedLpUnitaryRepresentation_isTopologicallyIrreducible_of
- ha_uniform_discretization(Theorem)
  
  Missing effort metadata.
- ha_unitary_irreducibility(Definition)
  
  Missing effort metadata.
  Associated lean decls (3)
- ha_unitary_representation_detail(Definition)
  
  Missing effort metadata.
  Associated lean decls (4)
- ha_vector_affine_irreducibility(Lemma)
  
  Missing effort metadata.
  Associated lean decls (3)
- hilbert_space_synthesis(Definition)
  
  Missing effort metadata.
  Associated lean decls (5)
- inverse_fourier_dilation_core(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.inverseFourierDilationTransformCore
- japanese_bracket(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.japaneseBracketPow
- l1_L2_extension(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.l1_ridgeletTransform_L2_extension
- l1_activation_classes(Proposition)
  
  Missing effort metadata.
- l1_admissibility(Definition)
  
  Missing effort metadata.
  Associated lean decls (5)
- l1_admissibility_examples(Proposition)
  
  Missing effort metadata.
  Associated lean decls (3)
- l1_balancing_distributional_rows(Theorem)
  
  Missing effort metadata.
- l1_balancing_theorem(Theorem)
  
  Missing effort metadata.
  Associated lean decls (3)
- l1_bump_ridgelet_construction(Lemma)
  
  Missing effort metadata.
  Associated lean decls (8)
- l1_construction_admissible(Corollary)
  
  Missing effort metadata.
  Associated lean decls (3)
- l1_continuity_L1_Linfty(Proposition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.norm_euclideanRidgeletTransform_zero_le
  - LeanRidgelet.l1_ridgeletTransform_bounded_L1_Linfty
- l1_dual_operator(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.l1_dualRidgeletTransform_pairing
- l1_fourier_away_from_origin(Definition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - MeasureTheory.PolynomiallyBounded
  - LeanRidgelet.HasFourierAwayFromOrigin
- l1_fourier_data_convolution(Lemma)
  
  Missing effort metadata.
  Associated lean decls (6)
- l1_fourier_expression(Theorem)
  
  Missing effort metadata.
  Associated lean decls (4)
- l1_fourier_slice_angular(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.angularFourier_slice_radonTransform
- l1_fractional_laplacian_intertwining(Corollary)
  
  Missing effort metadata.
- l1_gelfand_shilov_pairing(Lemma)
  
  Missing effort metadata.
  Associated lean decls (3)
- l1_l2_duality_steps(Lemma)
  
  Missing effort metadata.
  Associated lean decls (7)
- l1_lambda_multiplier(Theorem)
  
  Missing effort metadata.
  Associated lean decls (11)
- l1_lizorkin_moment_vanishing(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.integral_pow_mul_angularFourier1D_eq_zero
  - LeanRidgelet.integral_polynomial_mul_angularFourier1D_eq_zero
- l1_lizorkin_quotient_invariance(Proposition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.l1_hasFourierAwayFromOrigin_add_polynomial
- l1_lizorkin_spaces(Definition)
  
  Missing effort metadata.
- l1_pairing_extension(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.hasFourierAwayFromOrigin_pairing_extension
- l1_parameter_space(Definition)
  
  Missing effort metadata.
  Associated lean decls (4)
- l1_parseval_plancherel(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.l1_plancherel_identity
  - LeanRidgelet.l1_parseval_relation
- l1_plancherel_lintegral(Lemma)
  
  Missing effort metadata.
  Associated lean decls (4)
- l1_radon_backprojection(Definition)
  
  Missing effort metadata.
  Associated lean decls (3)
- l1_reconstruction(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.l1_reconstruction_formula
- l1_reconstruction_L2(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.l1_reconstruction_formula_L2
- l1_reconstruction_moment_layer(Lemma)
  
  Missing effort metadata.
  Associated lean decls (4)
- l1_reconstruction_radon(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.l1_reconstruction_formula_radon
  - LeanRidgelet.l1_radon_filtered_backprojection
- l1_reconstruction_section(Lemma)
  
  Missing effort metadata.
  Associated lean decls (9)
- l1_relu_universality(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.l1_relu_network_universal_approximation
- l1_ridgelet_transforms(Definition)
  
  Missing effort metadata.
  Associated lean decls (4)
- l1_spectral_pairing(Lemma)
  
  Missing effort metadata.
  Associated lean decls (6)
- l1_standard_activations(Definition)
  
  Missing effort metadata.
  Associated lean decls (3)
- l1_structure_theorem(Theorem)
  
  Missing effort metadata.
  Associated lean decls (4)
- l1_truncated_power_admissible(Proposition)
  
  Missing effort metadata.
  Associated lean decls (8)
- l1_truncated_power_fourier(Proposition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.l1_truncatedPower_hasFourierAwayFromOrigin
- l1_truncation_limit(Lemma)
  
  Missing effort metadata.
  Associated lean decls (10)
- l1_weak_ridgelet(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.weakRidgeletTransform
- mathlib_affine_haar(Theorem)
  
  Missing effort metadata.
  Associated lean decls (6)
- mathlib_affine_semidirect(Theorem)
  
  Missing effort metadata.
  Associated lean decls (20)
- mathlib_bochner_integral_l2(Theorem)
  
  Missing effort metadata.
  Associated lean decls (4)
- mathlib_cholesky_diag(Theorem)
  
  Missing effort metadata.
  Associated lean decls (10)
- mathlib_const_density_strong_continuity(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - UnitaryRepresentation.isStronglyContinuous_of_const_density
- mathlib_constant_density_preimage(Theorem)
  
  Missing effort metadata.
  Associated lean decls (3)
- mathlib_corner_det(Theorem)
  
  Missing effort metadata.
  Associated lean decls (23)
- mathlib_cyclic_fourier(Theorem)
  
  Missing effort metadata.
  Associated lean decls (10)
- mathlib_diagonal_scaling(Theorem)
  
  Missing effort metadata.
  Associated lean decls (7)
- mathlib_dirichlet_integral(Theorem)
  
  Missing effort metadata.
  Associated lean decls (7)
- mathlib_dplane_transform(Theorem)
  
  Missing effort metadata.
  Associated lean decls (23)
- mathlib_fourier_affine(Theorem)
  
  Missing effort metadata.
  Associated lean decls (6)
- mathlib_fourier_character_multiplier(Theorem)
  
  Missing effort metadata.
  Associated lean decls (12)
- mathlib_fourier_inversion_ae(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - MeasureTheory.Integrable.fourierInv_fourier_ae_eq
- mathlib_fourier_plancherel(Theorem)
  
  Missing effort metadata.
  Associated lean decls (7)
- mathlib_fourier_slice(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - MeasureTheory.fourier_slice_radonTransform
- mathlib_gaussian_schwartz(Theorem)
  
  Missing effort metadata.
  Associated lean decls (6)
- mathlib_general_linear_haar(Theorem)
  
  Missing effort metadata.
  Associated lean decls (18)
- mathlib_general_linear_orbit(Theorem)
  
  Missing effort metadata.
  Associated lean decls (5)
- mathlib_group_convolution_continuity(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - MeasureTheory.continuous_integral_compact_mul_right
- mathlib_haar_automorphism(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - MeasureTheory.exists_map_continuousMulEquiv_haar_eq_smul_haar
  - MeasureTheory.exists_map_continuousMulEquiv_haar_restrict_eq_smul_haar_restrict
- mathlib_haar_prod_assoc(Theorem)
  
  Missing effort metadata.
  Associated lean decls (5)
- mathlib_helgason_inversion(Theorem)
  
  Missing effort metadata.
  Associated lean decls (9)
- mathlib_hilbert_schmidt_kernel(Theorem)
  
  Missing effort metadata.
  Associated lean decls (22)
- mathlib_hilbert_symbol(Theorem)
  
  Missing effort metadata.
  Associated lean decls (11)
- mathlib_homogeneous_section_cocycle(Theorem)
  
  Missing effort metadata.
  Associated lean decls (14)
- mathlib_horocycle_radon(Theorem)
  
  Missing effort metadata.
  Associated lean decls (6)
- mathlib_hyperbolic_ball(Theorem)
  
  Missing effort metadata.
  Associated lean decls (16)
- mathlib_hyperbolic_boundary_mobius(Theorem)
  
  Missing effort metadata.
  Associated lean decls (19)
- mathlib_hyperbolic_helgason_fourier(Theorem)
  
  Missing effort metadata.
  Associated lean decls (11)
- mathlib_hyperbolic_mobius(Theorem)
  
  Missing effort metadata.
  Associated lean decls (21)
- mathlib_hyperbolic_mobius_measure(Theorem)
  
  Missing effort metadata.
  Associated lean decls (21)
- mathlib_integrated_unitary_representation(Theorem)
  
  Missing effort metadata.
  Associated lean decls (13)
- mathlib_iterated_fubini(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - MeasureTheory.integral_integral_integral_swap_left
  - MeasureTheory.integral_integral_integral_swap_right
- mathlib_l2_duality(Theorem)
  
  Missing effort metadata.
  Associated lean decls (7)
- mathlib_linear_surjection_haar(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - MeasureTheory.map_snd_restrict_prod_le
  - LinearMap.exists_map_restrict_addHaar_le_smul_addHaar
- mathlib_lipschitz_discretization(Theorem)
  
  Missing effort metadata.
  Associated lean decls (4)
- mathlib_lizorkin_space(Definition)
  
  Missing effort metadata.
  Associated lean decls (9)
- mathlib_lp_compact_multiplier(Theorem)
  
  Missing effort metadata.
  Associated lean decls (10)
- mathlib_lp_functor(Theorem)
  
  Missing effort metadata.
  Associated lean decls (14)
- mathlib_lp_indicator(Theorem)
  
  Missing effort metadata.
  Associated lean decls (12)
- mathlib_lp_integrable_dense(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - MeasureTheory.Lp.dense_setOf_integrable
- mathlib_lp_operator_of_pointwise(Theorem)
  
  Missing effort metadata.
  Associated lean decls (6)
- mathlib_lp_unimodular_multiplier(Theorem)
  
  Missing effort metadata.
  Associated lean decls (6)
- mathlib_matrix_polar(Theorem)
  
  Missing effort metadata.
  Associated lean decls (11)
- mathlib_orthogonal_complexification(Theorem)
  
  Missing effort metadata.
  Associated lean decls (11)
- mathlib_orthogonal_group(Theorem)
  
  Missing effort metadata.
  Associated lean decls (21)
- mathlib_parametric_iterated_deriv(Theorem)
  
  Missing effort metadata.
  Associated lean decls (15)
- mathlib_polar_coordinates(Theorem)
  
  Missing effort metadata.
  Associated lean decls (15)
- mathlib_polish_units(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Units.instPolishSpaceOfNormedRing
- mathlib_polynomial_growth(Theorem)
  
  Missing effort metadata.
  Associated lean decls (8)
- mathlib_prod_shear(Theorem)
  
  Missing effort metadata.
  Associated lean decls (9)
- mathlib_quasi_invariant_integral(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - MeasureTheory.integral_eq_integral_smul_comp_smul_of_map_eq_withDensity
  - NNReal.smul_inv_sqrt_smul
- mathlib_radon_l1_theory(Theorem)
  
  Missing effort metadata.
  Associated lean decls (6)
- mathlib_radon_schwartz_section(Theorem)
  
  Missing effort metadata.
  Associated lean decls (5)
- mathlib_radon_transform(Definition)
  
  Missing effort metadata.
  Associated lean decls (3)
- mathlib_relatively_invariant_density(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - MeasureTheory.Measure.map_withDensity_of_map_eq_smul
  - MeasureTheory.Measure.map_restrict_of_map_eq_smul
- mathlib_schwartz_aux(Theorem)
  
  Missing effort metadata.
  Associated lean decls (6)
- mathlib_semidirect_haar(Theorem)
  
  Missing effort metadata.
  Associated lean decls (12)
- mathlib_spd_boundary(Theorem)
  
  Missing effort metadata.
  Associated lean decls (6)
- mathlib_spd_cfunction(Theorem)
  
  Missing effort metadata.
  Associated lean decls (31)
- mathlib_spd_model(Theorem)
  
  Missing effort metadata.
  Associated lean decls (23)
- mathlib_sphere_invariant_measure(Theorem)
  
  Missing effort metadata.
  Associated lean decls (15)
- mathlib_stiefel_codim_one(Theorem)
  
  Missing effort metadata.
  Associated lean decls (5)
- mathlib_svd(Theorem)
  
  Missing effort metadata.
  Associated lean decls (6)
- mathlib_symmetric_cocycle(Theorem)
  
  Missing effort metadata.
  Associated lean decls (7)
- mathlib_symmetric_congruence_det(Theorem)
  
  Missing effort metadata.
  Associated lean decls (10)
- mathlib_symmetric_space_defs(Theorem)
  
  Missing effort metadata.
  Associated lean decls (15)
- mathlib_temperate_growth_rpow(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - Function.norm_iteratedFDerivWithin_rpow_le
  - Function.HasTemperateGrowth.rpow_of_le
- mathlib_unitary_character(Theorem)
  
  Missing effort metadata.
  Associated lean decls (7)
- mathlib_unitary_conjugation(Theorem)
  
  Missing effort metadata.
  Associated lean decls (14)
- mathlib_unitary_lp(Theorem)
  
  Missing effort metadata.
  Associated lean decls (12)
- mathlib_units_haar(Theorem)
  
  Missing effort metadata.
  Associated lean decls (26)
- mathlib_weighted_l1_smoothing(Theorem)
  
  Missing effort metadata.
  Associated lean decls (11)
- mathlib_weighted_sobolev_one_dim(Theorem)
  
  Missing effort metadata.
  Associated lean decls (8)
- mathlib_young_convolution(Theorem)
  
  Missing effort metadata.
  Associated lean decls (4)
- measure_valued_synthesis(Definition)
  
  Missing effort metadata.
- measure_valued_synthesis_detail(Definition)
  
  Missing effort metadata.
- minimum_norm_solution(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.normalizedNetworkRightInverse_unique_minimal
- network_synthesis(Definition)
  
  Missing effort metadata.
  Associated lean decls (4)
- normalized_finite_width_approximation(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.l2_theorem_five_normalized_finite_width_approximation
- normalized_finite_width_null_approximation(Theorem)
  
  Missing effort metadata.
- normalized_network_right_inverse(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.normalizedNetworkRightInverse
- normalized_network_right_inverse_spec(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.normalizedNetworkRightInverse_rightInverse
  - LeanRidgelet.surjective_networkSynthesis
- null_ridgelet_coefficients(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.activationFiberFunctional_fiberCoefficient_eq_zero_of_mem_ker
- null_space_encoding_and_perturbations(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.l2_theorem_four_encoding_and_perturbative_readout
- null_space_structure(Theorem)
  
  Missing effort metadata.
  Associated lean decls (4)
- parameter_space(Definition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.ParameterSpace
  - LeanRidgelet.parameterCoordinateEquiv
- parameter_space_and_unitary_transform(Definition)
  
  Missing effort metadata.
  Associated lean decls (4)
- pointwise_coordinate_transform(Definition)
  
  Missing effort metadata.
  Associated lean decls (4)
- pointwise_null_space(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.mem_ker_networkSynthesis_iff
  - LeanRidgelet.mem_ker_networkSynthesis_iff_fourierDilation
- relu_activation(Proposition)
  
  Missing effort metadata.
  Associated lean decls (5)
- relu_operator_theory(Proposition)
  
  Missing effort metadata.
  Associated lean decls (3)
- ridgelet_operator(Definition)
  
  Missing effort metadata.
  Associated lean decls (8)
- ridgelet_reconstruction(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.networkSynthesis_comp_ridgeletOperator
- ridgelet_series(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.hasSum_ridgeletOperator_fiberCoefficient
- ridgelet_simple_tensor(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.ridgeletOperator_apply_ae
  - LeanRidgelet.fourierDilationTransform_ridgeletOperator_apply_ae
- ridgelet_transform_and_pairing(Definition)
  
  Missing effort metadata.
  Associated lean decls (10)
- standard_activation_riesz_resolvents(Theorem)
  
  Missing effort metadata.
- tanh_activation(Proposition)
  
  Missing effort metadata.
  Associated lean decls (5)
- tanh_operator_theory(Proposition)
  
  Missing effort metadata.
  Associated lean decls (3)
- truncated_monte_carlo_quadrature(Lemma)
  
  Missing effort metadata.
- weighted_dilation_change_of_variables(Lemma)
  
  Missing effort metadata.
  Associated lean decls (2)
  - LeanRidgelet.integral_fourierDilationCoordinate_mul
  - LeanRidgelet.integrable_fourierDilationCoordinate_mul
- weighted_dilation_identity(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanRidgelet.integral_fourierDilationCoordinate_mul

Untagged (308)

abstract_basis_expansion(Theorem)

Missing tag metadata.
Associated lean decls (6)
abstract_reconstruction(Theorem)

Missing tag metadata.
Associated lean decls (4)
abstract_solution_geometry(Theorem)

Missing tag metadata.
Associated lean decls (11)
abstract_synthesis_and_reconstruction(Definition)

Missing tag metadata.
Associated lean decls (2)
- LeanRidgelet.unitarySynthesis
- LeanRidgelet.unitaryRidgelet
activation_distributional_fourier_formulas(Theorem)

Missing tag metadata.
activation_fiber_dual_bound(Theorem)

Missing tag metadata.
Associated lean decls (2)
- LeanRidgelet.norm_activationFiberFunctional_le
- LeanRidgelet.activationFiberDualMap
activation_fiber_functional(Definition)

Missing tag metadata.
Associated lean decls (5)
activation_functional(Definition)

Missing tag metadata.
Associated lean decls (5)
activation_hilbert_structure(Proposition)

Missing tag metadata.
Associated lean decls (1)
- LeanRidgelet.l2_proposition_one_activation_hilbert_structure
activation_hilbert_structure_detail(Proposition)

Missing tag metadata.
Associated lean decls (2)
- LeanRidgelet.activationCoordinateEquiv
- LeanRidgelet.activationDistribution_injective
Show all 298 more untagged entries
- activation_normalization(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.activationNormalization
- activation_normalization_positive(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.activationNormalization_pos
- activation_riesz_representer(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.activationRieszRepresenter
- activation_sobolev_inclusion(Theorem)
  
  Missing tag metadata.
- activation_space(Definition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.ActivationSpace
  - LeanRidgelet.activationDistribution
- activation_space_detail(Definition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.ActivationSpace
  - LeanRidgelet.activationDistribution
- adjoint_ridgelet_function(Definition)
  
  Missing tag metadata.
  Associated lean decls (4)
- adjoint_synthesis(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.adjoint_networkSynthesis
  - LeanRidgelet.networkSynthesis_comp_adjoint
- angular_fourier_convention(Definition)
  
  Missing tag metadata.
  Associated lean decls (3)
- angular_plancherel(Theorem)
  
  Missing tag metadata.
  Associated lean decls (4)
- bounded_network_synthesis(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.norm_networkSynthesis_le
  - LeanRidgelet.norm_networkSynthesis_apply_le
- bounded_synthesis(Theorem)
  
  Missing tag metadata.
  Associated lean decls (4)
- canonical_parameter_projection(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.networkVisibleProjection
- canonical_parameter_projection_properties(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.isIdempotentElem_networkVisibleProjection
  - LeanRidgelet.isSelfAdjoint_networkVisibleProjection
- canonical_parameter_projection_range_kernel(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.ker_networkVisibleProjection
  - LeanRidgelet.range_networkVisibleProjection
- canonical_solution_and_projection(Definition)
  
  Missing tag metadata.
  Associated lean decls (4)
- classical_ridgelet_agreement(Theorem)
  
  Missing tag metadata.
  Associated lean decls (6)
- classical_synthesis_agreement(Theorem)
  
  Missing tag metadata.
  Associated lean decls (4)
- coefficient_space(Definition)
  
  Missing tag metadata.
  Associated lean decls (4)
- coefficient_vector(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.fiberCoefficient
- concrete_adjoint(Lemma)
  
  Missing tag metadata.
  Associated lean decls (3)
- concrete_null_space_and_general_solution(Theorem)
  
  Missing tag metadata.
  Associated lean decls (6)
- concrete_reconstruction(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.l2_theorem_two_reconstruction
  - LeanRidgelet.networkSynthesis_comp_ridgeletOperator
- concrete_unitary_transform(Proposition)
  
  Missing tag metadata.
  Associated lean decls (6)
- core_transform_agrees_with_unitary(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.fourierDilationTransform_parameterSchwartzRealization
  - LeanRidgelet.fourierDilationTransform_parameterSchwartzRealization_apply_ae
- discretizable_ridgelet_null_elements(Corollary)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.l2_corollary_one_discretizable_ridgelet_null_elements
- discretizable_ridgelet_null_elements_detail(Corollary)
  
  Missing tag metadata.
- encoding_and_perturbative_readout(Theorem)
  
  Missing tag metadata.
- exact_finite_null_relations(Proposition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.l2_proposition_two_exact_finite_null_relations
- exact_finite_null_relations_detail(Proposition)
  
  Missing tag metadata.
- fiber_inner_product(Proposition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.fiberInner_self_eq_zero
  - LeanRidgelet.denseRange_fiberCore_coe
- fiber_space(Definition)
  
  Missing tag metadata.
  Associated lean decls (6)
- fourier_dilation_coordinate(Definition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.frequencyDilation
  - LeanRidgelet.fourierDilationCoordinate
- fourier_dilation_core(Definition)
  
  Missing tag metadata.
  Associated lean decls (5)
- fourier_dilation_core_plancherel(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.fourierDilationTransformCore_norm_sq
  - LeanRidgelet.integral_fiberBaseNormSq_fourierDilationTransformFiberCore
- fourier_dilation_inverse(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.inverseFourierDilationTransform_apply_fourierDilationTransform
- fourier_dilation_unitary(Definition)
  
  Missing tag metadata.
  Associated lean decls (3)
- fourier_expressions(Lemma)
  
  Missing tag metadata.
  Associated lean decls (4)
- fourier_expressions_detail(Lemma)
  
  Missing tag metadata.
- fs_dplane_affine(Theorem)
  
  Missing tag metadata.
  Associated lean decls (10)
- fs_dplane_codim_one_detail(Theorem)
  
  Missing tag metadata.
  Associated lean decls (11)
- fs_dplane_detail(Theorem)
  
  Missing tag metadata.
  Associated lean decls (3)
- fs_dplane_fractional(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.fs_fourier_dPlaneTransform_fractional
- fs_dplane_inversion(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.fs_dPlaneInversion
- fs_dplane_polar_codim_one(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.norm_smul_coe_sphere
  - LeanRidgelet.fs_matrixPolarIntegration_codim_one
- fs_dplane_rubin(Theorem)
  
  Missing tag metadata.
- fs_dplane_similitude(Theorem)
  
  Missing tag metadata.
  Associated lean decls (6)
- fs_dplane_stiefel(Theorem)
  
  Missing tag metadata.
  Associated lean decls (9)
- fs_dplane_stiefel_codim_one(Theorem)
  
  Missing tag metadata.
  Associated lean decls (5)
- fs_dplane_transform(Definition)
  
  Missing tag metadata.
  Associated lean decls (6)
- fs_euclidean_agreement(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.fs_separationOfVariables_euclideanRidgeletTransform
  - LeanRidgelet.fs_admissibilityConstant_eq_fourierSlicePairing
- fs_euclidean_detail(Theorem)
  
  Missing tag metadata.
  Associated lean decls (13)
- fs_finite_field_detail(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.fs_finiteField_sum_slice
  - LeanRidgelet.fs_finiteField_synthesis_ridgelet
- fs_finite_field_mean_zero(Lemma)
  
  Missing tag metadata.
  Associated lean decls (4)
- fs_finite_field_network(Definition)
  
  Missing tag metadata.
  Associated lean decls (3)
- fs_finite_field_reconstruction(Theorem)
  
  Missing tag metadata.
  Associated lean decls (3)
- fs_finite_field_steps(Theorem)
  
  Missing tag metadata.
  Associated lean decls (3)
- fs_fourier_formula_classical(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.fs_fourierFormula_irieFunahashi
- fs_gconv_detail(Theorem)
  
  Missing tag metadata.
  Associated lean decls (3)
- fs_gconv_network(Definition)
  
  Missing tag metadata.
  Associated lean decls (7)
- fs_gconv_projection_structural(Theorem)
  
  Missing tag metadata.
  Associated lean decls (5)
- fs_gconv_reconstruction(Theorem)
  
  Missing tag metadata.
  Associated lean decls (5)
- fs_method(Theorem)
  
  Missing tag metadata.
  Associated lean decls (8)
- fs_pairing(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.fourierSlicePairing
- fs_pairing_algebra(Lemma)
  
  Missing tag metadata.
  Associated lean decls (4)
- fs_pairing_detail(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.fourierSlicePairing
- fs_radon_classical(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.fs_ae_ne_zero
  - LeanRidgelet.fs_radon_reconstruction_codim_one
- fs_reconstruction_euclidean(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.fs_inversionIntegral_euclidean
  - LeanRidgelet.fs_reconstruction_euclidean
- fs_scheme_detail(Theorem)
  
  Missing tag metadata.
  Associated lean decls (9)
- fs_symmetric_detail(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.horosphericalWeight_zero
  - LeanRidgelet.fs_symmetric_reconstruction_of_inversion
- fs_symmetric_hyperbolic(Definition)
  
  Missing tag metadata.
  Associated lean decls (21)
- fs_symmetric_inversion(Theorem)
  
  Missing tag metadata.
  Associated lean decls (3)
- fs_symmetric_network(Definition)
  
  Missing tag metadata.
  Associated lean decls (5)
- fs_symmetric_reconstruction(Theorem)
  
  Missing tag metadata.
  Associated lean decls (5)
- fs_symmetric_spd(Definition)
  
  Missing tag metadata.
  Associated lean decls (16)
- fs_target_fractional_derivative(Theorem)
  
  Missing tag metadata.
  Associated lean decls (7)
- fs_target_svd_jacobian(Lemma)
  
  Missing tag metadata.
  Associated lean decls (4)
- gaussian_activation(Proposition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.gaussianActivation
  - LeanRidgelet.gaussianActivation_ne_zero
- general_solution_kernel_translate(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.networkSolution_iff_kernel_translate
- ha_adjoint_reconstruction_detail(Theorem)
  
  Missing tag metadata.
  Associated lean decls (9)
- ha_affine_appendix(Theorem)
  
  Missing tag metadata.
- ha_affine_classical_comparison_detail(Theorem)
  
  Missing tag metadata.
  Associated lean decls (14)
- ha_affine_frequency_detail(Theorem)
  
  Missing tag metadata.
  Associated lean decls (14)
- ha_affine_group_haar_detail(Theorem)
  
  Missing tag metadata.
  Associated lean decls (9)
- ha_affine_homogeneous_l2_detail(Theorem)
  
  Missing tag metadata.
  Associated lean decls (21)
- ha_affine_homogeneous_quasiregular_detail(Definition)
  
  Missing tag metadata.
  Associated lean decls (29)
- ha_affine_irreducibility(Theorem)
  
  Missing tag metadata.
  Associated lean decls (19)
- ha_affine_jacobian_detail(Theorem)
  
  Missing tag metadata.
  Associated lean decls (11)
- ha_affine_lift_detail(Definition)
  
  Missing tag metadata.
  Associated lean decls (22)
- ha_affine_mackey_detail(Theorem)
  
  Missing tag metadata.
  Associated lean decls (18)
- ha_affine_representations(Definition)
  
  Missing tag metadata.
  Associated lean decls (4)
- ha_affine_section_induction_detail(Theorem)
  
  Missing tag metadata.
  Associated lean decls (59)
- ha_appendix_depth_two(Definition)
  
  Missing tag metadata.
- ha_architecture_detail(Theorem)
  
  Missing tag metadata.
- ha_bochner_intertwining_detail(Lemma)
  
  Missing tag metadata.
  Associated lean decls (17)
- ha_bochner_measurability_detail(Lemma)
  
  Missing tag metadata.
  Associated lean decls (11)
- ha_bochner_preliminaries(Lemma)
  
  Missing tag metadata.
- ha_boundedness_criteria(Lemma)
  
  Missing tag metadata.
- ha_classical_equivariance(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.IsEquivariant
  - LeanRidgelet.IsEquivariant.isJointEquivariant_of_fixed
- ha_classical_reconstruction(Theorem)
  
  Missing tag metadata.
  Associated lean decls (5)
- ha_deep_cascade_detail(Lemma)
  
  Missing tag metadata.
  Associated lean decls (10)
- ha_deep_feature(Lemma)
  
  Missing tag metadata.
  Associated lean decls (5)
- ha_deep_ridgelet(Corollary)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.deepRidgelet_reconstruction_formula
  - LeanRidgelet.deepRidgelet_normalized_rightInverse
- ha_depth_two_machine(Definition)
  
  Missing tag metadata.
  Associated lean decls (5)
- ha_fully_connected_detail(Lemma)
  
  Missing tag metadata.
  Associated lean decls (12)
- ha_fully_connected_feature(Definition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.deepFullyConnectedFeature
  - LeanRidgelet.deepFullyConnectedFeature_endpoint_equivariant
- ha_fully_connected_l2_representation_detail(Lemma)
  
  Missing tag metadata.
  Associated lean decls (9)
- ha_group_convolution_detail(Theorem)
  
  Missing tag metadata.
  Associated lean decls (9)
- ha_group_convolution_reconstruction(Theorem)
  
  Missing tag metadata.
  Associated lean decls (3)
- ha_group_convolution_reduction(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.groupConvolutionalSynthesis_eq_orbit
  - LeanRidgelet.groupConvolutionalRidgelet_eq_base
- ha_induced_l2_detail(Definition)
  
  Missing tag metadata.
  Associated lean decls (16)
- ha_induced_representations(Definition)
  
  Missing tag metadata.
  Associated lean decls (3)
- ha_induced_unitarity(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.invariantLpUnitaryRepresentation
  - LeanRidgelet.quasiInvariantLpUnitaryRepresentation
- ha_intertwiner_operators(Definition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.JointEquivariantMachine
  - LeanRidgelet.JointEquivariantRidgelet
- ha_joint_equivariance(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.IsJointEquivariant
- ha_joint_equivariance_constructors(Lemma)
  
  Missing tag metadata.
  Associated lean decls (5)
- ha_joint_equivariance_detail(Definition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.IsJointEquivariant
  - LeanRidgelet.IsEquivariant
- ha_joint_machine(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.JointEquivariantMachine
- ha_l2_integral_detail(Theorem)
  
  Missing tag metadata.
- ha_l2_operator_bridge_detail(Definition)
  
  Missing tag metadata.
  Associated lean decls (4)
- ha_machine_intertwines(Lemma)
  
  Missing tag metadata.
  Associated lean decls (4)
- ha_main_reconstruction(Theorem)
  
  Missing tag metadata.
  Associated lean decls (3)
- ha_normalized_right_inverse(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.ha_normalizedRidgelet_rightInverse
- ha_orbit_feature(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.orbitFeature
  - LeanRidgelet.isJointEquivariant_orbitFeature
- ha_parametric_deriv_measurable_detail(Lemma)
  
  Missing tag metadata.
  Associated lean decls (15)
- ha_quadratic_composite_detail(Theorem)
  
  Missing tag metadata.
  Associated lean decls (8)
- ha_quadratic_detail(Lemma)
  
  Missing tag metadata.
  Associated lean decls (27)
- ha_quadratic_feature(Definition)
  
  Missing tag metadata.
  Associated lean decls (16)
- ha_quadratic_finite_width_detail(Theorem)
  
  Missing tag metadata.
  Associated lean decls (4)
- ha_quadratic_measure_detail(Theorem)
  
  Missing tag metadata.
  Associated lean decls (13)
- ha_quadratic_nonzero_detail(Theorem)
  
  Missing tag metadata.
  Associated lean decls (23)
- ha_quadratic_parameter_factor_detail(Lemma)
  
  Missing tag metadata.
  Associated lean decls (13)
- ha_quadratic_reconstruction_detail(Theorem)
  
  Missing tag metadata.
  Associated lean decls (20)
- ha_quadratic_relative_measure_detail(Theorem)
  
  Missing tag metadata.
  Associated lean decls (24)
- ha_quadratic_second_difference_detail(Theorem)
  
  Missing tag metadata.
  Associated lean decls (35)
- ha_quadratic_shear_detail(Lemma)
  
  Missing tag metadata.
  Associated lean decls (19)
- ha_quadratic_sobolev_carrier_detail(Lemma)
  
  Missing tag metadata.
  Associated lean decls (34)
- ha_quadratic_sobolev_fourier_detail(Lemma)
  
  Missing tag metadata.
  Associated lean decls (3)
- ha_quadratic_sobolev_space_detail(Lemma)
  
  Missing tag metadata.
  Associated lean decls (23)
- ha_quadratic_transfer_detail(Lemma)
  
  Missing tag metadata.
  Associated lean decls (5)
- ha_reconstruction_commutant(Lemma)
  
  Missing tag metadata.
  Associated lean decls (3)
- ha_reconstruction_detail(Theorem)
  
  Missing tag metadata.
  Associated lean decls (5)
- ha_ridgelet_intertwines(Lemma)
  
  Missing tag metadata.
  Associated lean decls (4)
- ha_ridgelet_transform(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.JointEquivariantRidgelet
- ha_schur_detail(Theorem)
  
  Missing tag metadata.
  Associated lean decls (10)
- ha_schur_lemma(Theorem)
  
  Missing tag metadata.
  Associated lean decls (3)
- ha_tensor_irreducibility(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.fullyConnectedLpUnitaryRepresentation_isTopologicallyIrreducible_of
- ha_uniform_discretization(Theorem)
  
  Missing tag metadata.
- ha_unitary_irreducibility(Definition)
  
  Missing tag metadata.
  Associated lean decls (3)
- ha_unitary_representation_detail(Definition)
  
  Missing tag metadata.
  Associated lean decls (4)
- ha_vector_affine_irreducibility(Lemma)
  
  Missing tag metadata.
  Associated lean decls (3)
- hilbert_space_synthesis(Definition)
  
  Missing tag metadata.
  Associated lean decls (5)
- inverse_fourier_dilation_core(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.inverseFourierDilationTransformCore
- japanese_bracket(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.japaneseBracketPow
- l1_L2_extension(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.l1_ridgeletTransform_L2_extension
- l1_activation_classes(Proposition)
  
  Missing tag metadata.
- l1_admissibility(Definition)
  
  Missing tag metadata.
  Associated lean decls (5)
- l1_admissibility_examples(Proposition)
  
  Missing tag metadata.
  Associated lean decls (3)
- l1_balancing_distributional_rows(Theorem)
  
  Missing tag metadata.
- l1_balancing_theorem(Theorem)
  
  Missing tag metadata.
  Associated lean decls (3)
- l1_bump_ridgelet_construction(Lemma)
  
  Missing tag metadata.
  Associated lean decls (8)
- l1_construction_admissible(Corollary)
  
  Missing tag metadata.
  Associated lean decls (3)
- l1_continuity_L1_Linfty(Proposition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.norm_euclideanRidgeletTransform_zero_le
  - LeanRidgelet.l1_ridgeletTransform_bounded_L1_Linfty
- l1_dual_operator(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.l1_dualRidgeletTransform_pairing
- l1_fourier_away_from_origin(Definition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - MeasureTheory.PolynomiallyBounded
  - LeanRidgelet.HasFourierAwayFromOrigin
- l1_fourier_data_convolution(Lemma)
  
  Missing tag metadata.
  Associated lean decls (6)
- l1_fourier_expression(Theorem)
  
  Missing tag metadata.
  Associated lean decls (4)
- l1_fourier_slice_angular(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.angularFourier_slice_radonTransform
- l1_fractional_laplacian_intertwining(Corollary)
  
  Missing tag metadata.
- l1_gelfand_shilov_pairing(Lemma)
  
  Missing tag metadata.
  Associated lean decls (3)
- l1_l2_duality_steps(Lemma)
  
  Missing tag metadata.
  Associated lean decls (7)
- l1_lambda_multiplier(Theorem)
  
  Missing tag metadata.
  Associated lean decls (11)
- l1_lizorkin_moment_vanishing(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.integral_pow_mul_angularFourier1D_eq_zero
  - LeanRidgelet.integral_polynomial_mul_angularFourier1D_eq_zero
- l1_lizorkin_quotient_invariance(Proposition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.l1_hasFourierAwayFromOrigin_add_polynomial
- l1_lizorkin_spaces(Definition)
  
  Missing tag metadata.
- l1_pairing_extension(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.hasFourierAwayFromOrigin_pairing_extension
- l1_parameter_space(Definition)
  
  Missing tag metadata.
  Associated lean decls (4)
- l1_parseval_plancherel(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.l1_plancherel_identity
  - LeanRidgelet.l1_parseval_relation
- l1_plancherel_lintegral(Lemma)
  
  Missing tag metadata.
  Associated lean decls (4)
- l1_radon_backprojection(Definition)
  
  Missing tag metadata.
  Associated lean decls (3)
- l1_reconstruction(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.l1_reconstruction_formula
- l1_reconstruction_L2(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.l1_reconstruction_formula_L2
- l1_reconstruction_moment_layer(Lemma)
  
  Missing tag metadata.
  Associated lean decls (4)
- l1_reconstruction_radon(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.l1_reconstruction_formula_radon
  - LeanRidgelet.l1_radon_filtered_backprojection
- l1_reconstruction_section(Lemma)
  
  Missing tag metadata.
  Associated lean decls (9)
- l1_relu_universality(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.l1_relu_network_universal_approximation
- l1_ridgelet_transforms(Definition)
  
  Missing tag metadata.
  Associated lean decls (4)
- l1_spectral_pairing(Lemma)
  
  Missing tag metadata.
  Associated lean decls (6)
- l1_standard_activations(Definition)
  
  Missing tag metadata.
  Associated lean decls (3)
- l1_structure_theorem(Theorem)
  
  Missing tag metadata.
  Associated lean decls (4)
- l1_truncated_power_admissible(Proposition)
  
  Missing tag metadata.
  Associated lean decls (8)
- l1_truncated_power_fourier(Proposition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.l1_truncatedPower_hasFourierAwayFromOrigin
- l1_truncation_limit(Lemma)
  
  Missing tag metadata.
  Associated lean decls (10)
- l1_weak_ridgelet(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.weakRidgeletTransform
- mathlib_affine_haar(Theorem)
  
  Missing tag metadata.
  Associated lean decls (6)
- mathlib_affine_semidirect(Theorem)
  
  Missing tag metadata.
  Associated lean decls (20)
- mathlib_bochner_integral_l2(Theorem)
  
  Missing tag metadata.
  Associated lean decls (4)
- mathlib_cholesky_diag(Theorem)
  
  Missing tag metadata.
  Associated lean decls (10)
- mathlib_const_density_strong_continuity(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - UnitaryRepresentation.isStronglyContinuous_of_const_density
- mathlib_constant_density_preimage(Theorem)
  
  Missing tag metadata.
  Associated lean decls (3)
- mathlib_corner_det(Theorem)
  
  Missing tag metadata.
  Associated lean decls (23)
- mathlib_cyclic_fourier(Theorem)
  
  Missing tag metadata.
  Associated lean decls (10)
- mathlib_diagonal_scaling(Theorem)
  
  Missing tag metadata.
  Associated lean decls (7)
- mathlib_dirichlet_integral(Theorem)
  
  Missing tag metadata.
  Associated lean decls (7)
- mathlib_dplane_transform(Theorem)
  
  Missing tag metadata.
  Associated lean decls (23)
- mathlib_fourier_affine(Theorem)
  
  Missing tag metadata.
  Associated lean decls (6)
- mathlib_fourier_character_multiplier(Theorem)
  
  Missing tag metadata.
  Associated lean decls (12)
- mathlib_fourier_inversion_ae(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - MeasureTheory.Integrable.fourierInv_fourier_ae_eq
- mathlib_fourier_plancherel(Theorem)
  
  Missing tag metadata.
  Associated lean decls (7)
- mathlib_fourier_slice(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - MeasureTheory.fourier_slice_radonTransform
- mathlib_gaussian_schwartz(Theorem)
  
  Missing tag metadata.
  Associated lean decls (6)
- mathlib_general_linear_haar(Theorem)
  
  Missing tag metadata.
  Associated lean decls (18)
- mathlib_general_linear_orbit(Theorem)
  
  Missing tag metadata.
  Associated lean decls (5)
- mathlib_group_convolution_continuity(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - MeasureTheory.continuous_integral_compact_mul_right
- mathlib_haar_automorphism(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - MeasureTheory.exists_map_continuousMulEquiv_haar_eq_smul_haar
  - MeasureTheory.exists_map_continuousMulEquiv_haar_restrict_eq_smul_haar_restrict
- mathlib_haar_prod_assoc(Theorem)
  
  Missing tag metadata.
  Associated lean decls (5)
- mathlib_helgason_inversion(Theorem)
  
  Missing tag metadata.
  Associated lean decls (9)
- mathlib_hilbert_schmidt_kernel(Theorem)
  
  Missing tag metadata.
  Associated lean decls (22)
- mathlib_hilbert_symbol(Theorem)
  
  Missing tag metadata.
  Associated lean decls (11)
- mathlib_homogeneous_section_cocycle(Theorem)
  
  Missing tag metadata.
  Associated lean decls (14)
- mathlib_horocycle_radon(Theorem)
  
  Missing tag metadata.
  Associated lean decls (6)
- mathlib_hyperbolic_ball(Theorem)
  
  Missing tag metadata.
  Associated lean decls (16)
- mathlib_hyperbolic_boundary_mobius(Theorem)
  
  Missing tag metadata.
  Associated lean decls (19)
- mathlib_hyperbolic_helgason_fourier(Theorem)
  
  Missing tag metadata.
  Associated lean decls (11)
- mathlib_hyperbolic_mobius(Theorem)
  
  Missing tag metadata.
  Associated lean decls (21)
- mathlib_hyperbolic_mobius_measure(Theorem)
  
  Missing tag metadata.
  Associated lean decls (21)
- mathlib_integrated_unitary_representation(Theorem)
  
  Missing tag metadata.
  Associated lean decls (13)
- mathlib_iterated_fubini(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - MeasureTheory.integral_integral_integral_swap_left
  - MeasureTheory.integral_integral_integral_swap_right
- mathlib_l2_duality(Theorem)
  
  Missing tag metadata.
  Associated lean decls (7)
- mathlib_linear_surjection_haar(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - MeasureTheory.map_snd_restrict_prod_le
  - LinearMap.exists_map_restrict_addHaar_le_smul_addHaar
- mathlib_lipschitz_discretization(Theorem)
  
  Missing tag metadata.
  Associated lean decls (4)
- mathlib_lizorkin_space(Definition)
  
  Missing tag metadata.
  Associated lean decls (9)
- mathlib_lp_compact_multiplier(Theorem)
  
  Missing tag metadata.
  Associated lean decls (10)
- mathlib_lp_functor(Theorem)
  
  Missing tag metadata.
  Associated lean decls (14)
- mathlib_lp_indicator(Theorem)
  
  Missing tag metadata.
  Associated lean decls (12)
- mathlib_lp_integrable_dense(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - MeasureTheory.Lp.dense_setOf_integrable
- mathlib_lp_operator_of_pointwise(Theorem)
  
  Missing tag metadata.
  Associated lean decls (6)
- mathlib_lp_unimodular_multiplier(Theorem)
  
  Missing tag metadata.
  Associated lean decls (6)
- mathlib_matrix_polar(Theorem)
  
  Missing tag metadata.
  Associated lean decls (11)
- mathlib_orthogonal_complexification(Theorem)
  
  Missing tag metadata.
  Associated lean decls (11)
- mathlib_orthogonal_group(Theorem)
  
  Missing tag metadata.
  Associated lean decls (21)
- mathlib_parametric_iterated_deriv(Theorem)
  
  Missing tag metadata.
  Associated lean decls (15)
- mathlib_polar_coordinates(Theorem)
  
  Missing tag metadata.
  Associated lean decls (15)
- mathlib_polish_units(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Units.instPolishSpaceOfNormedRing
- mathlib_polynomial_growth(Theorem)
  
  Missing tag metadata.
  Associated lean decls (8)
- mathlib_prod_shear(Theorem)
  
  Missing tag metadata.
  Associated lean decls (9)
- mathlib_quasi_invariant_integral(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - MeasureTheory.integral_eq_integral_smul_comp_smul_of_map_eq_withDensity
  - NNReal.smul_inv_sqrt_smul
- mathlib_radon_l1_theory(Theorem)
  
  Missing tag metadata.
  Associated lean decls (6)
- mathlib_radon_schwartz_section(Theorem)
  
  Missing tag metadata.
  Associated lean decls (5)
- mathlib_radon_transform(Definition)
  
  Missing tag metadata.
  Associated lean decls (3)
- mathlib_relatively_invariant_density(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - MeasureTheory.Measure.map_withDensity_of_map_eq_smul
  - MeasureTheory.Measure.map_restrict_of_map_eq_smul
- mathlib_schwartz_aux(Theorem)
  
  Missing tag metadata.
  Associated lean decls (6)
- mathlib_semidirect_haar(Theorem)
  
  Missing tag metadata.
  Associated lean decls (12)
- mathlib_spd_boundary(Theorem)
  
  Missing tag metadata.
  Associated lean decls (6)
- mathlib_spd_cfunction(Theorem)
  
  Missing tag metadata.
  Associated lean decls (31)
- mathlib_spd_model(Theorem)
  
  Missing tag metadata.
  Associated lean decls (23)
- mathlib_sphere_invariant_measure(Theorem)
  
  Missing tag metadata.
  Associated lean decls (15)
- mathlib_stiefel_codim_one(Theorem)
  
  Missing tag metadata.
  Associated lean decls (5)
- mathlib_svd(Theorem)
  
  Missing tag metadata.
  Associated lean decls (6)
- mathlib_symmetric_cocycle(Theorem)
  
  Missing tag metadata.
  Associated lean decls (7)
- mathlib_symmetric_congruence_det(Theorem)
  
  Missing tag metadata.
  Associated lean decls (10)
- mathlib_symmetric_space_defs(Theorem)
  
  Missing tag metadata.
  Associated lean decls (15)
- mathlib_temperate_growth_rpow(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - Function.norm_iteratedFDerivWithin_rpow_le
  - Function.HasTemperateGrowth.rpow_of_le
- mathlib_unitary_character(Theorem)
  
  Missing tag metadata.
  Associated lean decls (7)
- mathlib_unitary_conjugation(Theorem)
  
  Missing tag metadata.
  Associated lean decls (14)
- mathlib_unitary_lp(Theorem)
  
  Missing tag metadata.
  Associated lean decls (12)
- mathlib_units_haar(Theorem)
  
  Missing tag metadata.
  Associated lean decls (26)
- mathlib_weighted_l1_smoothing(Theorem)
  
  Missing tag metadata.
  Associated lean decls (11)
- mathlib_weighted_sobolev_one_dim(Theorem)
  
  Missing tag metadata.
  Associated lean decls (8)
- mathlib_young_convolution(Theorem)
  
  Missing tag metadata.
  Associated lean decls (4)
- measure_valued_synthesis(Definition)
  
  Missing tag metadata.
- measure_valued_synthesis_detail(Definition)
  
  Missing tag metadata.
- minimum_norm_solution(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.normalizedNetworkRightInverse_unique_minimal
- network_synthesis(Definition)
  
  Missing tag metadata.
  Associated lean decls (4)
- normalized_finite_width_approximation(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.l2_theorem_five_normalized_finite_width_approximation
- normalized_finite_width_null_approximation(Theorem)
  
  Missing tag metadata.
- normalized_network_right_inverse(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.normalizedNetworkRightInverse
- normalized_network_right_inverse_spec(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.normalizedNetworkRightInverse_rightInverse
  - LeanRidgelet.surjective_networkSynthesis
- null_ridgelet_coefficients(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.activationFiberFunctional_fiberCoefficient_eq_zero_of_mem_ker
- null_space_encoding_and_perturbations(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.l2_theorem_four_encoding_and_perturbative_readout
- null_space_structure(Theorem)
  
  Missing tag metadata.
  Associated lean decls (4)
- parameter_space(Definition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.ParameterSpace
  - LeanRidgelet.parameterCoordinateEquiv
- parameter_space_and_unitary_transform(Definition)
  
  Missing tag metadata.
  Associated lean decls (4)
- pointwise_coordinate_transform(Definition)
  
  Missing tag metadata.
  Associated lean decls (4)
- pointwise_null_space(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.mem_ker_networkSynthesis_iff
  - LeanRidgelet.mem_ker_networkSynthesis_iff_fourierDilation
- relu_activation(Proposition)
  
  Missing tag metadata.
  Associated lean decls (5)
- relu_operator_theory(Proposition)
  
  Missing tag metadata.
  Associated lean decls (3)
- ridgelet_operator(Definition)
  
  Missing tag metadata.
  Associated lean decls (8)
- ridgelet_reconstruction(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.networkSynthesis_comp_ridgeletOperator
- ridgelet_series(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.hasSum_ridgeletOperator_fiberCoefficient
- ridgelet_simple_tensor(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.ridgeletOperator_apply_ae
  - LeanRidgelet.fourierDilationTransform_ridgeletOperator_apply_ae
- ridgelet_transform_and_pairing(Definition)
  
  Missing tag metadata.
  Associated lean decls (10)
- standard_activation_riesz_resolvents(Theorem)
  
  Missing tag metadata.
- tanh_activation(Proposition)
  
  Missing tag metadata.
  Associated lean decls (5)
- tanh_operator_theory(Proposition)
  
  Missing tag metadata.
  Associated lean decls (3)
- truncated_monte_carlo_quadrature(Lemma)
  
  Missing tag metadata.
- weighted_dilation_change_of_variables(Lemma)
  
  Missing tag metadata.
  Associated lean decls (2)
  - LeanRidgelet.integral_fourierDilationCoordinate_mul
  - LeanRidgelet.integrable_fourierDilationCoordinate_mul
- weighted_dilation_identity(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanRidgelet.integral_fourierDilationCoordinate_mul

Structure and coverage

Informal-only23Statements with no associated Lean code yet.

Ready to formalize8Entries whose next step is currently unblocked.

Fully closed277Local code and ancestor closure are both complete.

Heaviest prerequisites (204)

ha_affine_section_induction_detail(Theorem)

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

total deps: 8statement deps: 8proof deps: 0direct uses: 1downstream unlocks: 1
Associated lean decls (59)
fs_dplane_codim_one_detail(Theorem)

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 (11)
fs_symmetric_hyperbolic(Definition)

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 (21)
l1_parseval_plancherel(Theorem)

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

total deps: 6statement deps: 6proof deps: 0direct uses: 3downstream unlocks: 3
Associated lean decls (2)
- LeanRidgelet.l1_plancherel_identity
- LeanRidgelet.l1_parseval_relation
fs_dplane_affine(Theorem)

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

total deps: 5statement deps: 5proof deps: 0direct uses: 1downstream unlocks: 1
Associated lean decls (10)
fs_dplane_stiefel(Theorem)

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

total deps: 5statement deps: 5proof deps: 0direct uses: 3downstream unlocks: 5
Associated lean decls (9)
ha_affine_mackey_detail(Theorem)

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

total deps: 5statement deps: 5proof deps: 0direct uses: 4downstream unlocks: 8
Associated lean decls (18)
l1_balancing_theorem(Theorem)

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

total deps: 5statement deps: 5proof deps: 0direct uses: 2downstream unlocks: 2
Associated lean decls (3)
l1_reconstruction_radon(Theorem)

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

total deps: 5statement deps: 5proof deps: 0direct uses: 1downstream unlocks: 1
Associated lean decls (2)
- LeanRidgelet.l1_reconstruction_formula_radon
- LeanRidgelet.l1_radon_filtered_backprojection
l1_structure_theorem(Theorem)

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 (4)
Show all 194 more heaviest-prerequisite entries
- l1_truncated_power_admissible(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 5statement deps: 5proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (8)
- null_space_structure(Theorem)
  
  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 (4)
- fs_dplane_stiefel_codim_one(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 4statement deps: 4proof deps: 0direct uses: 3downstream unlocks: 8
  Associated lean decls (5)
- fs_symmetric_spd(Definition)
  
  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)
- ha_affine_frequency_detail(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 9
  Associated lean decls (14)
- ha_affine_irreducibility(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 4statement deps: 4proof deps: 0direct uses: 3downstream unlocks: 13
  Associated lean decls (19)
- ha_fully_connected_l2_representation_detail(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (9)
- ha_quadratic_reconstruction_detail(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 4statement deps: 4proof deps: 0direct uses: 2downstream unlocks: 9
  Associated lean decls (20)
- ha_quadratic_sobolev_space_detail(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 (23)
- l1_activation_classes(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
- l1_admissibility_examples(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 (3)
- l1_fourier_data_convolution(Lemma)
  
  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 (6)
- l1_lambda_multiplier(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 4statement deps: 4proof deps: 0direct uses: 3downstream unlocks: 7
  Associated lean decls (11)
- l1_reconstruction(Theorem)
  
  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 (1)
  - LeanRidgelet.l1_reconstruction_formula
- l1_reconstruction_L2(Theorem)
  
  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)
  - LeanRidgelet.l1_reconstruction_formula_L2
- mathlib_hyperbolic_helgason_fourier(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 4statement deps: 4proof deps: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (11)
- concrete_null_space_and_general_solution(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (6)
- fourier_expressions_detail(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
- fs_dplane_inversion(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 (1)
  - LeanRidgelet.fs_dPlaneInversion
- fs_dplane_similitude(Theorem)
  
  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 (6)
- fs_euclidean_agreement(Theorem)
  
  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)
  - LeanRidgelet.fs_separationOfVariables_euclideanRidgeletTransform
  - LeanRidgelet.fs_admissibilityConstant_eq_fourierSlicePairing
- fs_symmetric_reconstruction(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 3downstream unlocks: 3
  Associated lean decls (5)
- ha_affine_group_haar_detail(Theorem)
  
  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 (9)
- ha_affine_lift_detail(Definition)
  
  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 (22)
- ha_architecture_detail(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
- ha_bochner_intertwining_detail(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 3downstream unlocks: 38
  Associated lean decls (17)
- ha_main_reconstruction(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 3downstream unlocks: 5
  Associated lean decls (3)
- ha_parametric_deriv_measurable_detail(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (15)
- ha_quadratic_measure_detail(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 12
  Associated lean decls (13)
- ha_quadratic_relative_measure_detail(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 3downstream unlocks: 11
  Associated lean decls (24)
- ha_quadratic_second_difference_detail(Theorem)
  
  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 (35)
- ha_quadratic_sobolev_carrier_detail(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 (34)
- ha_quadratic_sobolev_fourier_detail(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 (3)
- hilbert_space_synthesis(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 6
  Associated lean decls (5)
- l1_L2_extension(Theorem)
  
  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)
  - LeanRidgelet.l1_ridgeletTransform_L2_extension
- l1_fourier_slice_angular(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - LeanRidgelet.angularFourier_slice_radonTransform
- l1_l2_duality_steps(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 (7)
- l1_pairing_extension(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 2downstream unlocks: 6
  Associated lean decls (1)
  - LeanRidgelet.hasFourierAwayFromOrigin_pairing_extension
- l1_reconstruction_section(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 6
  Associated lean decls (9)
- l1_truncated_power_fourier(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 3downstream unlocks: 4
  Associated lean decls (1)
  - LeanRidgelet.l1_truncatedPower_hasFourierAwayFromOrigin
- l1_truncation_limit(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (10)
- mathlib_general_linear_haar(Theorem)
  
  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 (18)
- mathlib_matrix_polar(Theorem)
  
  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 (11)
- mathlib_spd_model(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 3downstream unlocks: 3
  Associated lean decls (23)
- parameter_space_and_unitary_transform(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 12
  Associated lean decls (4)
- activation_functional(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 10
  Associated lean decls (5)
- adjoint_ridgelet_function(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 5
  Associated lean decls (4)
- canonical_solution_and_projection(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 3
  Associated lean decls (4)
- concrete_adjoint(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (3)
- concrete_reconstruction(Theorem)
  
  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)
  - LeanRidgelet.l2_theorem_two_reconstruction
  - LeanRidgelet.networkSynthesis_comp_ridgeletOperator
- core_transform_agrees_with_unitary(Theorem)
  
  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)
  - LeanRidgelet.fourierDilationTransform_parameterSchwartzRealization
  - LeanRidgelet.fourierDilationTransform_parameterSchwartzRealization_apply_ae
- discretizable_ridgelet_null_elements(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)
  - LeanRidgelet.l2_corollary_one_discretizable_ridgelet_null_elements
- fourier_expressions(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 4
  Associated lean decls (4)
- fs_dplane_detail(Theorem)
  
  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 (3)
- fs_dplane_fractional(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 9
  Associated lean decls (1)
  - LeanRidgelet.fs_fourier_dPlaneTransform_fractional
- fs_euclidean_detail(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (13)
- fs_finite_field_reconstruction(Theorem)
  
  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 (3)
- fs_gconv_detail(Theorem)
  
  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 (3)
- fs_gconv_reconstruction(Theorem)
  
  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 (5)
- fs_method(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 20
  Associated lean decls (8)
- fs_reconstruction_euclidean(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 6downstream unlocks: 15
  Associated lean decls (2)
  - LeanRidgelet.fs_inversionIntegral_euclidean
  - LeanRidgelet.fs_reconstruction_euclidean
- fs_scheme_detail(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 5
  Associated lean decls (9)
- fs_symmetric_detail(Theorem)
  
  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)
  - LeanRidgelet.horosphericalWeight_zero
  - LeanRidgelet.fs_symmetric_reconstruction_of_inversion
- fs_symmetric_inversion(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (3)
- fs_target_fractional_derivative(Theorem)
  
  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 (7)
- fs_target_svd_jacobian(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 (4)
- ha_adjoint_reconstruction_detail(Theorem)
  
  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 (9)
- ha_affine_classical_comparison_detail(Theorem)
  
  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 (14)
- ha_affine_homogeneous_quasiregular_detail(Definition)
  
  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 (29)
- ha_affine_jacobian_detail(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 5downstream unlocks: 30
  Associated lean decls (11)
- ha_appendix_depth_two(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
- ha_bochner_measurability_detail(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 (11)
- ha_boundedness_criteria(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
- ha_classical_reconstruction(Theorem)
  
  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 (5)
- ha_deep_cascade_detail(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 9
  Associated lean decls (10)
- ha_deep_ridgelet(Corollary)
  
  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)
  - LeanRidgelet.deepRidgelet_reconstruction_formula
  - LeanRidgelet.deepRidgelet_normalized_rightInverse
- ha_group_convolution_detail(Theorem)
  
  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 (9)
- ha_joint_machine(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 9
  Associated lean decls (1)
  - LeanRidgelet.JointEquivariantMachine
- ha_l2_integral_detail(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
- ha_l2_operator_bridge_detail(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 6
  Associated lean decls (4)
- ha_quadratic_composite_detail(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 8
  Associated lean decls (8)
- ha_quadratic_detail(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 15
  Associated lean decls (27)
- ha_quadratic_feature(Definition)
  
  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 (16)
- ha_quadratic_finite_width_detail(Theorem)
  
  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 (4)
- ha_quadratic_nonzero_detail(Theorem)
  
  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 (23)
- ha_quadratic_parameter_factor_detail(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 7
  Associated lean decls (13)
- ha_quadratic_shear_detail(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 4downstream unlocks: 6
  Associated lean decls (19)
- ha_reconstruction_detail(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 21
  Associated lean decls (5)
- ha_ridgelet_transform(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 8
  Associated lean decls (1)
  - LeanRidgelet.JointEquivariantRidgelet
- ha_uniform_discretization(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
- ha_vector_affine_irreducibility(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 (3)
- l1_balancing_distributional_rows(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
- l1_bump_ridgelet_construction(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 (8)
- l1_construction_admissible(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 3
  Associated lean decls (3)
- l1_fourier_away_from_origin(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 7downstream unlocks: 23
  Associated lean decls (2)
  - MeasureTheory.PolynomiallyBounded
  - LeanRidgelet.HasFourierAwayFromOrigin
- l1_fourier_expression(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 6
  Associated lean decls (4)
- l1_fractional_laplacian_intertwining(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
- l1_gelfand_shilov_pairing(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 5
  Associated lean decls (3)
- l1_lizorkin_moment_vanishing(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (2)
  - LeanRidgelet.integral_pow_mul_angularFourier1D_eq_zero
  - LeanRidgelet.integral_polynomial_mul_angularFourier1D_eq_zero
- l1_lizorkin_quotient_invariance(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (1)
  - LeanRidgelet.l1_hasFourierAwayFromOrigin_add_polynomial
- l1_plancherel_lintegral(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 4
  Associated lean decls (4)
- l1_radon_backprojection(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 4downstream unlocks: 15
  Associated lean decls (3)
- l1_reconstruction_moment_layer(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 10
  Associated lean decls (4)
- l1_relu_universality(Theorem)
  
  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)
  - LeanRidgelet.l1_relu_network_universal_approximation
- l1_spectral_pairing(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 5
  Associated lean decls (6)
- l1_weak_ridgelet(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - LeanRidgelet.weakRidgeletTransform
- mathlib_const_density_strong_continuity(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 9
  Associated lean decls (1)
  - UnitaryRepresentation.isStronglyContinuous_of_const_density
- mathlib_dplane_transform(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 5downstream unlocks: 24
  Associated lean decls (23)
- mathlib_fourier_slice(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 32
  Associated lean decls (1)
  - MeasureTheory.fourier_slice_radonTransform
- mathlib_helgason_inversion(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 5downstream unlocks: 10
  Associated lean decls (9)
- mathlib_hilbert_symbol(Theorem)
  
  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 (11)
- mathlib_hyperbolic_boundary_mobius(Theorem)
  
  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 (19)
- mathlib_radon_schwartz_section(Theorem)
  
  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 (5)
- mathlib_spd_boundary(Theorem)
  
  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 (6)
- mathlib_spd_cfunction(Theorem)
  
  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 (31)
- mathlib_sphere_invariant_measure(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 13
  Associated lean decls (15)
- mathlib_stiefel_codim_one(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 7
  Associated lean decls (5)
- mathlib_unitary_lp(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (12)
- null_space_encoding_and_perturbations(Theorem)
  
  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)
  - LeanRidgelet.l2_theorem_four_encoding_and_perturbative_readout
- abstract_basis_expansion(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (6)
- abstract_reconstruction(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 12
  Associated lean decls (4)
- abstract_solution_geometry(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (11)
- activation_hilbert_structure(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - LeanRidgelet.l2_proposition_one_activation_hilbert_structure
- bounded_synthesis(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 5
  Associated lean decls (4)
- classical_ridgelet_agreement(Theorem)
  
  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 (6)
- concrete_unitary_transform(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 11
  Associated lean decls (6)
- discretizable_ridgelet_null_elements_detail(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
- fs_dplane_polar_codim_one(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 9
  Associated lean decls (2)
  - LeanRidgelet.norm_smul_coe_sphere
  - LeanRidgelet.fs_matrixPolarIntegration_codim_one
- fs_dplane_rubin(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
- fs_dplane_transform(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 6downstream unlocks: 11
  Associated lean decls (6)
- fs_finite_field_detail(Theorem)
  
  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 (2)
  - LeanRidgelet.fs_finiteField_sum_slice
  - LeanRidgelet.fs_finiteField_synthesis_ridgelet
- fs_finite_field_mean_zero(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (4)
- fs_finite_field_steps(Theorem)
  
  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 (3)
- fs_fourier_formula_classical(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - LeanRidgelet.fs_fourierFormula_irieFunahashi
- fs_gconv_projection_structural(Theorem)
  
  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 (5)
- fs_pairing_algebra(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (4)
- fs_radon_classical(Theorem)
  
  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 (2)
  - LeanRidgelet.fs_ae_ne_zero
  - LeanRidgelet.fs_radon_reconstruction_codim_one
- ha_affine_appendix(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
- ha_affine_homogeneous_l2_detail(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (21)
- ha_affine_representations(Definition)
  
  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 (4)
- ha_classical_equivariance(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - LeanRidgelet.IsEquivariant
  - LeanRidgelet.IsEquivariant.isJointEquivariant_of_fixed
- ha_deep_feature(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 6
  Associated lean decls (5)
- ha_fully_connected_detail(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (12)
- ha_fully_connected_feature(Definition)
  
  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 (2)
  - LeanRidgelet.deepFullyConnectedFeature
  - LeanRidgelet.deepFullyConnectedFeature_endpoint_equivariant
- ha_group_convolution_reconstruction(Theorem)
  
  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 (3)
- ha_group_convolution_reduction(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - LeanRidgelet.groupConvolutionalSynthesis_eq_orbit
  - LeanRidgelet.groupConvolutionalRidgelet_eq_base
- ha_induced_l2_detail(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 39
  Associated lean decls (16)
- ha_induced_representations(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 13
  Associated lean decls (3)
- ha_induced_unitarity(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - LeanRidgelet.invariantLpUnitaryRepresentation
  - LeanRidgelet.quasiInvariantLpUnitaryRepresentation
- ha_intertwiner_operators(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 23
  Associated lean decls (2)
  - LeanRidgelet.JointEquivariantMachine
  - LeanRidgelet.JointEquivariantRidgelet
- ha_joint_equivariance_constructors(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 39
  Associated lean decls (5)
- ha_machine_intertwines(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 (4)
- ha_normalized_right_inverse(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - LeanRidgelet.ha_normalizedRidgelet_rightInverse
- ha_orbit_feature(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - LeanRidgelet.orbitFeature
  - LeanRidgelet.isJointEquivariant_orbitFeature
- ha_quadratic_transfer_detail(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 7
  Associated lean decls (5)
- ha_reconstruction_commutant(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 22
  Associated lean decls (3)
- ha_ridgelet_intertwines(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 (4)
- ha_schur_detail(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 22
  Associated lean decls (10)
- ha_schur_lemma(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 20
  Associated lean decls (3)
- ha_tensor_irreducibility(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - LeanRidgelet.fullyConnectedLpUnitaryRepresentation_isTopologicallyIrreducible_of
- l1_admissibility(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 7downstream unlocks: 14
  Associated lean decls (5)
- l1_continuity_L1_Linfty(Proposition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (2)
  - LeanRidgelet.norm_euclideanRidgeletTransform_zero_le
  - LeanRidgelet.l1_ridgeletTransform_bounded_L1_Linfty
- l1_dual_operator(Theorem)
  
  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 (1)
  - LeanRidgelet.l1_dualRidgeletTransform_pairing
- l1_ridgelet_transforms(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 7downstream unlocks: 23
  Associated lean decls (4)
- mathlib_affine_semidirect(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 9
  Associated lean decls (20)
- mathlib_cholesky_diag(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 5
  Associated lean decls (10)
- mathlib_corner_det(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 4
  Associated lean decls (23)
- mathlib_fourier_affine(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 (6)
- mathlib_fourier_character_multiplier(Theorem)
  
  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 (12)
- mathlib_haar_automorphism(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (2)
  - MeasureTheory.exists_map_continuousMulEquiv_haar_eq_smul_haar
  - MeasureTheory.exists_map_continuousMulEquiv_haar_restrict_eq_smul_haar_restrict
- mathlib_haar_prod_assoc(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 8
  Associated lean decls (5)
- mathlib_hilbert_schmidt_kernel(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 10
  Associated lean decls (22)
- mathlib_horocycle_radon(Theorem)
  
  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 (6)
- mathlib_hyperbolic_ball(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 5
  Associated lean decls (16)
- mathlib_hyperbolic_mobius(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 4
  Associated lean decls (21)
- mathlib_hyperbolic_mobius_measure(Theorem)
  
  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 (21)
- mathlib_integrated_unitary_representation(Theorem)
  
  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 (13)
- mathlib_linear_surjection_haar(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (2)
  - MeasureTheory.map_snd_restrict_prod_le
  - LinearMap.exists_map_restrict_addHaar_le_smul_addHaar
- mathlib_lipschitz_discretization(Theorem)
  
  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 (4)
- mathlib_lp_compact_multiplier(Theorem)
  
  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 (10)
- mathlib_orthogonal_complexification(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (11)
- mathlib_orthogonal_group(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 18
  Associated lean decls (21)
- mathlib_radon_l1_theory(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 33
  Associated lean decls (6)
- mathlib_relatively_invariant_density(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 12
  Associated lean decls (2)
  - MeasureTheory.Measure.map_withDensity_of_map_eq_smul
  - MeasureTheory.Measure.map_restrict_of_map_eq_smul
- mathlib_semidirect_haar(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 4
  Associated lean decls (12)
- mathlib_svd(Theorem)
  
  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)
- mathlib_symmetric_cocycle(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (7)
- mathlib_unitary_character(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 9
  Associated lean decls (7)
- mathlib_weighted_sobolev_one_dim(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (8)
- normalized_finite_width_approximation(Theorem)
  
  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 (1)
  - LeanRidgelet.l2_theorem_five_normalized_finite_width_approximation
- normalized_finite_width_null_approximation(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
- ridgelet_transform_and_pairing(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 8
  Associated lean decls (10)
- truncated_monte_carlo_quadrature(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
- weighted_dilation_identity(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 13
  Associated lean decls (1)
  - LeanRidgelet.integral_fourierDilationCoordinate_mul

No prerequisites (104)

mathlib_diagonal_scaling(Theorem)
Associated lean decls (7)
mathlib_polynomial_growth(Theorem)
Associated lean decls (8)
fs_gconv_network(Definition)
Associated lean decls (7)
fiber_space(Definition)
Associated lean decls (6)
mathlib_fourier_plancherel(Theorem)
Associated lean decls (7)
mathlib_general_linear_orbit(Theorem)
Associated lean decls (5)
relu_operator_theory(Proposition)
Associated lean decls (3)
ridgelet_reconstruction(Theorem)
Associated lean decls (1)
- LeanRidgelet.networkSynthesis_comp_ridgeletOperator
measure_valued_synthesis_detail(Definition)
measure_valued_synthesis(Definition)
Show all 94 more entries without prerequisites
- mathlib_iterated_fubini(Lemma)
  Associated lean decls (2)
  - MeasureTheory.integral_integral_integral_swap_left
  - MeasureTheory.integral_integral_integral_swap_right
- activation_hilbert_structure_detail(Proposition)
  Associated lean decls (2)
  - LeanRidgelet.activationCoordinateEquiv
  - LeanRidgelet.activationDistribution_injective
- mathlib_homogeneous_section_cocycle(Theorem)
  Associated lean decls (14)
- mathlib_lp_unimodular_multiplier(Theorem)
  Associated lean decls (6)
- tanh_activation(Proposition)
  Associated lean decls (5)
- activation_distributional_fourier_formulas(Theorem)
- mathlib_lp_integrable_dense(Theorem)
  Associated lean decls (1)
  - MeasureTheory.Lp.dense_setOf_integrable
- coefficient_vector(Definition)
  Associated lean decls (1)
  - LeanRidgelet.fiberCoefficient
- activation_space(Definition)
  Associated lean decls (2)
  - LeanRidgelet.ActivationSpace
  - LeanRidgelet.activationDistribution
- network_synthesis(Definition)
  Associated lean decls (4)
- mathlib_dirichlet_integral(Theorem)
  Associated lean decls (7)
- relu_activation(Proposition)
  Associated lean decls (5)
- fs_symmetric_network(Definition)
  Associated lean decls (5)
- normalized_network_right_inverse_spec(Theorem)
  Associated lean decls (2)
  - LeanRidgelet.normalizedNetworkRightInverse_rightInverse
  - LeanRidgelet.surjective_networkSynthesis
- weighted_dilation_change_of_variables(Lemma)
  Associated lean decls (2)
  - LeanRidgelet.integral_fourierDilationCoordinate_mul
  - LeanRidgelet.integrable_fourierDilationCoordinate_mul
- activation_normalization(Definition)
  Associated lean decls (1)
  - LeanRidgelet.activationNormalization
- mathlib_weighted_l1_smoothing(Theorem)
  Associated lean decls (11)
- mathlib_lp_functor(Theorem)
  Associated lean decls (14)
- mathlib_symmetric_congruence_det(Theorem)
  Associated lean decls (10)
- ridgelet_series(Theorem)
  Associated lean decls (1)
  - LeanRidgelet.hasSum_ridgeletOperator_fiberCoefficient
- canonical_parameter_projection(Definition)
  Associated lean decls (1)
  - LeanRidgelet.networkVisibleProjection
- mathlib_symmetric_space_defs(Theorem)
  Associated lean decls (15)
- mathlib_schwartz_aux(Theorem)
  Associated lean decls (6)
- canonical_parameter_projection_properties(Theorem)
  Associated lean decls (2)
  - LeanRidgelet.isIdempotentElem_networkVisibleProjection
  - LeanRidgelet.isSelfAdjoint_networkVisibleProjection
- mathlib_temperate_growth_rpow(Theorem)
  Associated lean decls (2)
  - Function.norm_iteratedFDerivWithin_rpow_le
  - Function.HasTemperateGrowth.rpow_of_le
- activation_riesz_representer(Definition)
  Associated lean decls (1)
  - LeanRidgelet.activationRieszRepresenter
- mathlib_gaussian_schwartz(Theorem)
  Associated lean decls (6)
- pointwise_coordinate_transform(Definition)
  Associated lean decls (4)
- mathlib_lp_indicator(Theorem)
  Associated lean decls (12)
- japanese_bracket(Definition)
  Associated lean decls (1)
  - LeanRidgelet.japaneseBracketPow
- l1_standard_activations(Definition)
  Associated lean decls (3)
- minimum_norm_solution(Theorem)
  Associated lean decls (1)
  - LeanRidgelet.normalizedNetworkRightInverse_unique_minimal
- mathlib_constant_density_preimage(Theorem)
  Associated lean decls (3)
- fs_pairing_detail(Definition)
  Associated lean decls (1)
  - LeanRidgelet.fourierSlicePairing
- abstract_synthesis_and_reconstruction(Definition)
  Associated lean decls (2)
  - LeanRidgelet.unitarySynthesis
  - LeanRidgelet.unitaryRidgelet
- null_ridgelet_coefficients(Theorem)
  Associated lean decls (1)
  - LeanRidgelet.activationFiberFunctional_fiberCoefficient_eq_zero_of_mem_ker
- mathlib_prod_shear(Theorem)
  Associated lean decls (9)
- mathlib_lp_operator_of_pointwise(Theorem)
  Associated lean decls (6)
- l1_lizorkin_spaces(Definition)
- mathlib_quasi_invariant_integral(Theorem)
  Associated lean decls (2)
  - MeasureTheory.integral_eq_integral_smul_comp_smul_of_map_eq_withDensity
  - NNReal.smul_inv_sqrt_smul
- ridgelet_simple_tensor(Lemma)
  Associated lean decls (2)
  - LeanRidgelet.ridgeletOperator_apply_ae
  - LeanRidgelet.fourierDilationTransform_ridgeletOperator_apply_ae
- inverse_fourier_dilation_core(Definition)
  Associated lean decls (1)
  - LeanRidgelet.inverseFourierDilationTransformCore
- mathlib_unitary_conjugation(Theorem)
  Associated lean decls (14)
- parameter_space(Definition)
  Associated lean decls (2)
  - LeanRidgelet.ParameterSpace
  - LeanRidgelet.parameterCoordinateEquiv
- tanh_operator_theory(Proposition)
  Associated lean decls (3)
- activation_fiber_dual_bound(Theorem)
  Associated lean decls (2)
  - LeanRidgelet.norm_activationFiberFunctional_le
  - LeanRidgelet.activationFiberDualMap
- coefficient_space(Definition)
  Associated lean decls (4)
- mathlib_radon_transform(Definition)
  Associated lean decls (3)
- mathlib_polish_units(Theorem)
  Associated lean decls (1)
  - Units.instPolishSpaceOfNormedRing
- mathlib_cyclic_fourier(Theorem)
  Associated lean decls (10)
- mathlib_group_convolution_continuity(Theorem)
  Associated lean decls (1)
  - MeasureTheory.continuous_integral_compact_mul_right
- pointwise_null_space(Theorem)
  Associated lean decls (2)
  - LeanRidgelet.mem_ker_networkSynthesis_iff
  - LeanRidgelet.mem_ker_networkSynthesis_iff_fourierDilation
- activation_sobolev_inclusion(Theorem)
- standard_activation_riesz_resolvents(Theorem)
- mathlib_fourier_inversion_ae(Theorem)
  Associated lean decls (1)
  - MeasureTheory.Integrable.fourierInv_fourier_ae_eq
- fourier_dilation_core(Definition)
  Associated lean decls (5)
- fiber_inner_product(Proposition)
  Associated lean decls (2)
  - LeanRidgelet.fiberInner_self_eq_zero
  - LeanRidgelet.denseRange_fiberCore_coe
- mathlib_polar_coordinates(Theorem)
  Associated lean decls (15)
- mathlib_young_convolution(Theorem)
  Associated lean decls (4)
- ha_depth_two_machine(Definition)
  Associated lean decls (5)
- general_solution_kernel_translate(Theorem)
  Associated lean decls (1)
  - LeanRidgelet.networkSolution_iff_kernel_translate
- ha_bochner_preliminaries(Lemma)
- mathlib_parametric_iterated_deriv(Theorem)
  Associated lean decls (15)
- fs_pairing(Definition)
  Associated lean decls (1)
  - LeanRidgelet.fourierSlicePairing
- gaussian_activation(Proposition)
  Associated lean decls (2)
  - LeanRidgelet.gaussianActivation
  - LeanRidgelet.gaussianActivation_ne_zero
- mathlib_l2_duality(Theorem)
  Associated lean decls (7)
- fourier_dilation_coordinate(Definition)
  Associated lean decls (2)
  - LeanRidgelet.frequencyDilation
  - LeanRidgelet.fourierDilationCoordinate
- ha_joint_equivariance(Definition)
  Associated lean decls (1)
  - LeanRidgelet.IsJointEquivariant
- exact_finite_null_relations(Proposition)
  Associated lean decls (1)
  - LeanRidgelet.l2_proposition_two_exact_finite_null_relations
- normalized_network_right_inverse(Definition)
  Associated lean decls (1)
  - LeanRidgelet.normalizedNetworkRightInverse
- canonical_parameter_projection_range_kernel(Theorem)
  Associated lean decls (2)
  - LeanRidgelet.ker_networkVisibleProjection
  - LeanRidgelet.range_networkVisibleProjection
- mathlib_affine_haar(Theorem)
  Associated lean decls (6)
- ridgelet_operator(Definition)
  Associated lean decls (8)
- classical_synthesis_agreement(Theorem)
  Associated lean decls (4)
- activation_normalization_positive(Theorem)
  Associated lean decls (1)
  - LeanRidgelet.activationNormalization_pos
- ha_unitary_irreducibility(Definition)
  Associated lean decls (3)
- bounded_network_synthesis(Theorem)
  Associated lean decls (2)
  - LeanRidgelet.norm_networkSynthesis_le
  - LeanRidgelet.norm_networkSynthesis_apply_le
- encoding_and_perturbative_readout(Theorem)
- fourier_dilation_unitary(Definition)
  Associated lean decls (3)
- mathlib_units_haar(Theorem)
  Associated lean decls (26)
- adjoint_synthesis(Theorem)
  Associated lean decls (2)
  - LeanRidgelet.adjoint_networkSynthesis
  - LeanRidgelet.networkSynthesis_comp_adjoint
- exact_finite_null_relations_detail(Proposition)
- ha_unitary_representation_detail(Definition)
  Associated lean decls (4)
- activation_space_detail(Definition)
  Associated lean decls (2)
  - LeanRidgelet.ActivationSpace
  - LeanRidgelet.activationDistribution
- angular_plancherel(Theorem)
  Associated lean decls (4)
- mathlib_bochner_integral_l2(Theorem)
  Associated lean decls (4)
- fourier_dilation_core_plancherel(Theorem)
  Associated lean decls (2)
  - LeanRidgelet.fourierDilationTransformCore_norm_sq
  - LeanRidgelet.integral_fiberBaseNormSq_fourierDilationTransformFiberCore
- l1_parameter_space(Definition)
  Associated lean decls (4)
- ha_joint_equivariance_detail(Definition)
  Associated lean decls (2)
  - LeanRidgelet.IsJointEquivariant
  - LeanRidgelet.IsEquivariant
- fourier_dilation_inverse(Theorem)
  Associated lean decls (1)
  - LeanRidgelet.inverseFourierDilationTransform_apply_fourierDilationTransform
- activation_fiber_functional(Definition)
  Associated lean decls (5)
- mathlib_lizorkin_space(Definition)
  Associated lean decls (9)
- angular_fourier_convention(Definition)
  Associated lean decls (3)
- fs_finite_field_network(Definition)
  Associated lean decls (3)

No dependents (93)

l1_admissibility_examples(Proposition)
Associated lean decls (3)
fiber_space(Definition)
Associated lean decls (6)
ha_bochner_measurability_detail(Lemma)
Associated lean decls (11)
ha_affine_appendix(Theorem)
activation_fiber_functional(Definition)
Associated lean decls (5)
fourier_dilation_core_plancherel(Theorem)
Associated lean decls (2)
- LeanRidgelet.fourierDilationTransformCore_norm_sq
- LeanRidgelet.integral_fiberBaseNormSq_fourierDilationTransformFiberCore
ha_group_convolution_reduction(Lemma)
Associated lean decls (2)
- LeanRidgelet.groupConvolutionalSynthesis_eq_orbit
- LeanRidgelet.groupConvolutionalRidgelet_eq_base
discretizable_ridgelet_null_elements_detail(Corollary)
fs_target_fractional_derivative(Theorem)
Associated lean decls (7)
exact_finite_null_relations_detail(Proposition)
Show all 83 more entries without dependents
- fs_euclidean_agreement(Theorem)
  Associated lean decls (2)
  - LeanRidgelet.fs_separationOfVariables_euclideanRidgeletTransform
  - LeanRidgelet.fs_admissibilityConstant_eq_fourierSlicePairing
- tanh_activation(Proposition)
  Associated lean decls (5)
- activation_distributional_fourier_formulas(Theorem)
- ha_normalized_right_inverse(Theorem)
  Associated lean decls (1)
  - LeanRidgelet.ha_normalizedRidgelet_rightInverse
- relu_activation(Proposition)
  Associated lean decls (5)
- null_space_structure(Theorem)
  Associated lean decls (4)
- ridgelet_operator(Definition)
  Associated lean decls (8)
- canonical_parameter_projection_range_kernel(Theorem)
  Associated lean decls (2)
  - LeanRidgelet.ker_networkVisibleProjection
  - LeanRidgelet.range_networkVisibleProjection
- ha_uniform_discretization(Theorem)
- ha_quadratic_second_difference_detail(Theorem)
  Associated lean decls (35)
- normalized_network_right_inverse(Definition)
  Associated lean decls (1)
  - LeanRidgelet.normalizedNetworkRightInverse
- exact_finite_null_relations(Proposition)
  Associated lean decls (1)
  - LeanRidgelet.l2_proposition_two_exact_finite_null_relations
- activation_normalization(Definition)
  Associated lean decls (1)
  - LeanRidgelet.activationNormalization
- fs_finite_field_mean_zero(Lemma)
  Associated lean decls (4)
- fourier_dilation_coordinate(Definition)
  Associated lean decls (2)
  - LeanRidgelet.frequencyDilation
  - LeanRidgelet.fourierDilationCoordinate
- gaussian_activation(Proposition)
  Associated lean decls (2)
  - LeanRidgelet.gaussianActivation
  - LeanRidgelet.gaussianActivation_ne_zero
- mathlib_weighted_sobolev_one_dim(Theorem)
  Associated lean decls (8)
- fs_dplane_inversion(Lemma)
  Associated lean decls (1)
  - LeanRidgelet.fs_dPlaneInversion
- fiber_inner_product(Proposition)
  Associated lean decls (2)
  - LeanRidgelet.fiberInner_self_eq_zero
  - LeanRidgelet.denseRange_fiberCore_coe
- l1_reconstruction_L2(Theorem)
  Associated lean decls (1)
  - LeanRidgelet.l1_reconstruction_formula_L2
- standard_activation_riesz_resolvents(Theorem)
- l1_relu_universality(Theorem)
  Associated lean decls (1)
  - LeanRidgelet.l1_relu_network_universal_approximation
- activation_riesz_representer(Definition)
  Associated lean decls (1)
  - LeanRidgelet.activationRieszRepresenter
- fourier_expressions_detail(Lemma)
- fs_gconv_detail(Theorem)
  Associated lean decls (3)
- fs_target_svd_jacobian(Lemma)
  Associated lean decls (4)
- fs_finite_field_reconstruction(Theorem)
  Associated lean decls (3)
- tanh_operator_theory(Proposition)
  Associated lean decls (3)
- ha_orbit_feature(Lemma)
  Associated lean decls (2)
  - LeanRidgelet.orbitFeature
  - LeanRidgelet.isJointEquivariant_orbitFeature
- mathlib_lp_operator_of_pointwise(Theorem)
  Associated lean decls (6)
- null_space_encoding_and_perturbations(Theorem)
  Associated lean decls (1)
  - LeanRidgelet.l2_theorem_four_encoding_and_perturbative_readout
- parameter_space(Definition)
  Associated lean decls (2)
  - LeanRidgelet.ParameterSpace
  - LeanRidgelet.parameterCoordinateEquiv
- inverse_fourier_dilation_core(Definition)
  Associated lean decls (1)
  - LeanRidgelet.inverseFourierDilationTransformCore
- mathlib_spd_boundary(Theorem)
  Associated lean decls (6)
- ha_induced_unitarity(Lemma)
  Associated lean decls (2)
  - LeanRidgelet.invariantLpUnitaryRepresentation
  - LeanRidgelet.quasiInvariantLpUnitaryRepresentation
- ha_classical_equivariance(Lemma)
  Associated lean decls (2)
  - LeanRidgelet.IsEquivariant
  - LeanRidgelet.IsEquivariant.isJointEquivariant_of_fixed
- fs_symmetric_detail(Theorem)
  Associated lean decls (2)
  - LeanRidgelet.horosphericalWeight_zero
  - LeanRidgelet.fs_symmetric_reconstruction_of_inversion
- ha_boundedness_criteria(Lemma)
- activation_fiber_dual_bound(Theorem)
  Associated lean decls (2)
  - LeanRidgelet.norm_activationFiberFunctional_le
  - LeanRidgelet.activationFiberDualMap
- discretizable_ridgelet_null_elements(Corollary)
  Associated lean decls (1)
  - LeanRidgelet.l2_corollary_one_discretizable_ridgelet_null_elements
- activation_hilbert_structure(Proposition)
  Associated lean decls (1)
  - LeanRidgelet.l2_proposition_one_activation_hilbert_structure
- l1_balancing_distributional_rows(Theorem)
- ha_quadratic_sobolev_fourier_detail(Lemma)
  Associated lean decls (3)
- japanese_bracket(Definition)
  Associated lean decls (1)
  - LeanRidgelet.japaneseBracketPow
- fs_dplane_rubin(Theorem)
- mathlib_spd_cfunction(Theorem)
  Associated lean decls (31)
- activation_sobolev_inclusion(Theorem)
- truncated_monte_carlo_quadrature(Lemma)
- ha_appendix_depth_two(Definition)
- ha_quadratic_feature(Definition)
  Associated lean decls (16)
- ha_architecture_detail(Theorem)
- canonical_parameter_projection_properties(Theorem)
  Associated lean decls (2)
  - LeanRidgelet.isIdempotentElem_networkVisibleProjection
  - LeanRidgelet.isSelfAdjoint_networkVisibleProjection
- canonical_parameter_projection(Definition)
  Associated lean decls (1)
  - LeanRidgelet.networkVisibleProjection
- ha_affine_lift_detail(Definition)
  Associated lean decls (22)
- l1_activation_classes(Proposition)
- l1_structure_theorem(Theorem)
  Associated lean decls (4)
- ha_adjoint_reconstruction_detail(Theorem)
  Associated lean decls (9)
- weighted_dilation_change_of_variables(Lemma)
  Associated lean decls (2)
  - LeanRidgelet.integral_fourierDilationCoordinate_mul
  - LeanRidgelet.integrable_fourierDilationCoordinate_mul
- fs_symmetric_spd(Definition)
  Associated lean decls (16)
- activation_normalization_positive(Theorem)
  Associated lean decls (1)
  - LeanRidgelet.activationNormalization_pos
- l1_fractional_laplacian_intertwining(Corollary)
- normalized_network_right_inverse_spec(Theorem)
  Associated lean decls (2)
  - LeanRidgelet.normalizedNetworkRightInverse_rightInverse
  - LeanRidgelet.surjective_networkSynthesis
- bounded_network_synthesis(Theorem)
  Associated lean decls (2)
  - LeanRidgelet.norm_networkSynthesis_le
  - LeanRidgelet.norm_networkSynthesis_apply_le
- mathlib_symmetric_cocycle(Theorem)
  Associated lean decls (7)
- fs_pairing_algebra(Lemma)
  Associated lean decls (4)
- encoding_and_perturbative_readout(Theorem)
- ha_quadratic_nonzero_detail(Theorem)
  Associated lean decls (23)
- ha_tensor_irreducibility(Lemma)
  Associated lean decls (1)
  - LeanRidgelet.fullyConnectedLpUnitaryRepresentation_isTopologicallyIrreducible_of
- network_synthesis(Definition)
  Associated lean decls (4)
- adjoint_synthesis(Theorem)
  Associated lean decls (2)
  - LeanRidgelet.adjoint_networkSynthesis
  - LeanRidgelet.networkSynthesis_comp_adjoint
- coefficient_vector(Definition)
  Associated lean decls (1)
  - LeanRidgelet.fiberCoefficient
- activation_hilbert_structure_detail(Proposition)
  Associated lean decls (2)
  - LeanRidgelet.activationCoordinateEquiv
  - LeanRidgelet.activationDistribution_injective
- concrete_reconstruction(Theorem)
  Associated lean decls (2)
  - LeanRidgelet.l2_theorem_two_reconstruction
  - LeanRidgelet.networkSynthesis_comp_ridgeletOperator
- activation_space_detail(Definition)
  Associated lean decls (2)
  - LeanRidgelet.ActivationSpace
  - LeanRidgelet.activationDistribution
- fourier_dilation_inverse(Theorem)
  Associated lean decls (1)
  - LeanRidgelet.inverseFourierDilationTransform_apply_fourierDilationTransform
- ridgelet_reconstruction(Theorem)
  Associated lean decls (1)
  - LeanRidgelet.networkSynthesis_comp_ridgeletOperator
- angular_fourier_convention(Definition)
  Associated lean decls (3)
- core_transform_agrees_with_unitary(Theorem)
  Associated lean decls (2)
  - LeanRidgelet.fourierDilationTransform_parameterSchwartzRealization
  - LeanRidgelet.fourierDilationTransform_parameterSchwartzRealization_apply_ae
- fs_symmetric_hyperbolic(Definition)
  Associated lean decls (21)
- l1_continuity_L1_Linfty(Proposition)
  Associated lean decls (2)
  - LeanRidgelet.norm_euclideanRidgeletTransform_zero_le
  - LeanRidgelet.l1_ridgeletTransform_bounded_L1_Linfty
- mathlib_hyperbolic_boundary_mobius(Theorem)
  Associated lean decls (19)
- fs_dplane_codim_one_detail(Theorem)
  Associated lean decls (11)
- fs_fourier_formula_classical(Theorem)
  Associated lean decls (1)
  - LeanRidgelet.fs_fourierFormula_irieFunahashi