/- Copyright (c) 2026 Sho Sonoda. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Sho Sonoda, OpenAI Codex -/ import LeanRidgelet import Mathlib.Util.AssertNoSorry /-! # Assumption audit This file checks every declaration in the `LeanRidgelet` namespace, not only a selected final theorem. It enforces two repository policies: 1. A declaration may transitively depend only on Lean's standard classical axioms listed in `permittedAxioms`. The only exceptions are the explicitly named unfinished results in `permittedSorryDeclarations` and the explicitly reviewed endpoints derived from them in `permittedSorryDependents`; all other uses of `sorryAx` and all project axioms are rejected. 2. A project-defined structure or class may not have a proposition-valued field unless that field has been reviewed and added to `permittedProofFields`. The second check is deliberately conservative. It prevents analytic results from being moved into an assumptions structure or typeclass where `#print axioms` would not identify them as axioms. Run this file through `scripts/audit-assumptions.sh`; do not import it from the library. -/ open Lean Meta Elab Command namespace LeanRidgelet.Audit /-- Kernel axioms routinely permitted by Mathlib's classical development. -/ private def permittedAxioms : NameSet := ((({} : NameSet).insert ``propext).insert ``Quot.sound).insert ``Classical.choice /-- Named statements whose proofs remain to be formalized. The L1 theory is complete: since 2026-08-05 it contains no placeholder. The HA theory's Mackey route is complete as well: since 2026-08-15 it contains no placeholder, Folland Lemma 6.29 having been the last one, so regular-section density, the operator-theoretic remainder of 6.28, Theorem 6.39, Lemma 6.30's inducing-fiber correspondence, the one-dimensional fiber classification, and the Mathlib-general Fourier-character form of Theorem 4.44 are all unconditional. The HA theory has had no entry at all since 2026-09-08, when the admissibility placeholder of the Section 7 quadratic example was withdrawn -- the fixed-coefficient energy identity showed it to be false as stated -- and the Section 7 endpoint was restated and proved at a fixed shape matrix. Built by folding `NameSet.insert` over a flat list so that adding or removing an entry is a single-line edit with no parenthesis bookkeeping. -/ private def permittedSorryDeclarations : NameSet := List.foldl NameSet.insert ∅ [``LeanRidgelet.l2_theorem_four_encoding_and_perturbative_readout, ``LeanRidgelet.l2_theorem_five_normalized_finite_width_approximation, ``LeanRidgelet.l2_corollary_one_discretizable_ridgelet_null_elements, ``LeanRidgelet.l2_proposition_two_exact_finite_null_relations, ``LeanRidgelet.fs_svdJacobian, ``LeanRidgelet.fs_hyperbolicHelgasonInversion, ``LeanRidgelet.fs_spdHelgasonInversion] /-- Completed proof terms that intentionally expose a paper-facing consequence of a named placeholder. Keep this separate from `permittedSorryDeclarations`: entries here must contain no source-level `sorry`, and each one must be a short derivation from a listed root placeholder. Empty since 2026-09-08. The affine irreducibility chain that used to be listed here depends on no placeholder since 2026-08-15, and the quadratic endpoint `quadratic_reconstruction_nonzero` that was listed from 2026-08-19 was removed together with its root on 2026-09-08; every member of the former is checked by an `assert_no_sorry` below, and the fixed-shape endpoint that replaced the latter is checked the same way. -/ private def permittedSorryDependents : NameSet := List.foldl NameSet.insert ∅ [] /-- Reviewed proposition-valued fields of project-defined structures and classes. Keep this empty unless a proof field is mathematically part of a genuine data structure rather than a device for hiding an unfinished theorem. Every addition requires manual review. -/ private def permittedProofFields : NameSet := {} private def isProjectModule (name : Name) : Bool := name.toString.startsWith "LeanRidgelet" /-- Audit transitive axioms and proposition-valued fields of project declarations. -/ elab "audit_ridgelet_assumptions" : command => do let env ← getEnv let mut names : Array Name := #[] for importedModule in env.header.modules, data in env.header.moduleData do if isProjectModule importedModule.module then names := names ++ data.constNames let mut unexpectedAxioms : Array (Name × Name) := #[] for name in names do let axioms ← liftTermElabM <| Lean.collectAxioms name for axiomName in axioms do unless permittedAxioms.contains axiomName || (axiomName == ``sorryAx && (permittedSorryDeclarations.contains name || permittedSorryDependents.contains name)) do unexpectedAxioms := unexpectedAxioms.push (name, axiomName) unless unexpectedAxioms.isEmpty do let details := String.intercalate "\n" <| unexpectedAxioms.toList.map fun (name, axiomName) => s!" {name}: {axiomName}" throwError m!"Unexpected axioms in LeanRidgelet declarations:\n{details}" let mut unexpectedProofFields : Array (Name × Name) := #[] for name in names do if let some info := getStructureInfo? env name then for fieldName in info.fieldNames do if let some fieldInfo := env.find? fieldName then let isProofField ← liftTermElabM <| forallTelescopeReducing fieldInfo.type fun _ resultType => isProp resultType if isProofField && !permittedProofFields.contains fieldName then unexpectedProofFields := unexpectedProofFields.push (name, fieldName) unless unexpectedProofFields.isEmpty do let details := String.intercalate "\n" <| unexpectedProofFields.toList.map fun (name, fieldName) => s!" {name}.{fieldName}" throwError m!"Unreviewed proposition-valued structure/class fields:\n{details}" logInfo m!"Assumption audit passed for {names.size} LeanRidgelet declarations." audit_ridgelet_assumptions -- Representative public endpoints remain visible in the audit log. assert_no_sorry LeanRidgelet.Fourier.angular_plancherel_schwartz_inner assert_no_sorry LeanRidgelet.Fourier.angularFourierDistribution_angularFourierInvDistribution assert_no_sorry LeanRidgelet.Fourier.angularFourierDistribution_toTemperedDistributionCLM_eq assert_no_sorry LeanRidgelet.ha_reconstruction_of_hasSchurProperty assert_no_sorry LeanRidgelet.ha_reconstruction_of_hasSchurProperty_of_intertwiner assert_no_sorry LeanRidgelet.ha_normalizedRidgelet_rightInverse assert_no_sorry LeanRidgelet.UnitaryRepresentation.adjoint_coe assert_no_sorry LeanRidgelet.adjointIntertwiner assert_no_sorry LeanRidgelet.adjointIntertwiner_toContinuousLinearMap assert_no_sorry LeanRidgelet.adjointReconstructionOperator assert_no_sorry LeanRidgelet.adjointReconstructionOperator_apply assert_no_sorry LeanRidgelet.inner_adjointReconstructionOperator assert_no_sorry LeanRidgelet.ha_adjoint_reconstruction assert_no_sorry LeanRidgelet.ha_adjoint_reconstruction_of_ne_zero assert_no_sorry MeasureTheory.integrable_real_eq_zero_of_integral_fourierChar_inner assert_no_sorry MeasureTheory.integrable_complex_eq_zero_of_integral_fourierChar_inner assert_no_sorry MeasureTheory.exists_fourierCharacter_finset_approx_indicator_eLpNorm assert_no_sorry MeasureTheory.exists_finsetSum_fourierCharacterLpMultiplier_approx_indicatorLp assert_no_sorry MeasureTheory.ContinuousLinearMap.commutes_indicatorLp_of_commutes_fourierCharacter assert_no_sorry LeanRidgelet.affineMackey_commutes_indicator_of_commutes_translation assert_no_sorry UnitaryRepresentation.lpPointwiseLinearIsometryEquivMonoidHom assert_no_sorry UnitaryRepresentation.lpPointwise assert_no_sorry UnitaryRepresentation.lpPointwise_apply_ae assert_no_sorry UnitaryRepresentation.prodOfCommute assert_no_sorry UnitaryRepresentation.prodOfCommute_isTopologicallyIrreducible_of_finiteDimensional assert_no_sorry ContinuousLinearMap.zero_compLpL assert_no_sorry ContinuousLinearMap.id_compLpL assert_no_sorry ContinuousLinearMap.comp_compLpL assert_no_sorry ContinuousLinearMap.sub_compLpL assert_no_sorry ContinuousLinearMap.finsetSum_compLpL assert_no_sorry ContinuousLinearMap.compLpL_injective assert_no_sorry ContinuousLinearMap.lpCoordinateEmbedding assert_no_sorry ContinuousLinearMap.lpCoordinateProjection assert_no_sorry ContinuousLinearMap.rankOne_compLpL_eq_coordinate_comp assert_no_sorry ContinuousLinearMap.sum_lpCoordinateEmbedding_comp_projection_eq_id assert_no_sorry ContinuousLinearMap.exists_eq_compLpL_of_matrixCoefficient_scalar assert_no_sorry Matrix.realToComplexStarMonoidHom assert_no_sorry Matrix.orthogonalComplexificationMatrix assert_no_sorry Matrix.standardComplexOrthogonalRepresentation assert_no_sorry Matrix.standardComplexOrthogonalRepresentation_apply assert_no_sorry Matrix.standardComplexOrthogonalRepresentation_isTopologicallyIrreducible assert_no_sorry LeanRidgelet.affineDataLpUnitaryRepresentation_apply_ae_vector assert_no_sorry LeanRidgelet.compLpL_intertwines_affineData assert_no_sorry LeanRidgelet.lpPointwise_commute_affineData assert_no_sorry LeanRidgelet.fullyConnectedLpUnitaryRepresentation assert_no_sorry LeanRidgelet.fullyConnectedLpUnitaryRepresentation_apply_ae assert_no_sorry LeanRidgelet.fullyConnectedLpUnitaryRepresentation_isTopologicallyIrreducible_of assert_no_sorry LeanRidgelet.standardOrthogonalAffineLpUnitaryRepresentation assert_no_sorry LeanRidgelet.standardOrthogonalAffineLpUnitaryRepresentation_apply_ae assert_no_sorry LeanRidgelet.standardOrthogonalAffineLpUnitaryRepresentation_isTopologicallyIrreducible_of assert_no_sorry UnitaryRepresentation.isInvariant_iff_starProjection_commutes assert_no_sorry UnitaryRepresentation.Commutes.adjoint assert_no_sorry UnitaryRepresentation.complex_isTopologicallyIrreducible assert_no_sorry UnitaryRepresentation.one_complex_isTopologicallyIrreducible assert_no_sorry UnitaryRepresentation.ofCircleCharacter_isStronglyContinuous assert_no_sorry UnitaryRepresentation.ofCircleCharacter_isTopologicallyIrreducible assert_no_sorry QuotientGroup.leftCosetSection assert_no_sorry QuotientGroup.mk_leftCosetSection assert_no_sorry QuotientGroup.leftCosetSectionCocycleOf assert_no_sorry QuotientGroup.leftCosetSectionCocycleOf_one assert_no_sorry QuotientGroup.leftCosetSectionCocycleOf_mul assert_no_sorry QuotientGroup.leftCosetSectionCocycle assert_no_sorry QuotientGroup.leftCosetSectionCocycle_one assert_no_sorry QuotientGroup.leftCosetSectionCocycle_mul assert_no_sorry QuotientGroup.leftCosetSectionMultiplierOf assert_no_sorry QuotientGroup.leftCosetSectionMultiplierOf_one assert_no_sorry QuotientGroup.leftCosetSectionMultiplierOf_mul assert_no_sorry QuotientGroup.leftCosetSectionMultiplier assert_no_sorry QuotientGroup.leftCosetSectionMultiplier_one assert_no_sorry QuotientGroup.leftCosetSectionMultiplier_mul assert_no_sorry UnitaryRepresentation.exists_nonzero_orthogonal_cutoffs_of_isSelfAdjoint_not_scalar assert_no_sorry UnitaryRepresentation.exists_nontrivial_spectralSubspace_of_isSelfAdjoint_not_scalar assert_no_sorry UnitaryRepresentation.exists_scalar_of_isSelfAdjoint_of_commutes assert_no_sorry UnitaryRepresentation.hasSchurProperty_of_isTopologicallyIrreducible assert_no_sorry UnitaryRepresentation.isTopologicallyIrreducible_of_hasSchurProperty assert_no_sorry UnitaryRepresentation.isTopologicallyIrreducible_iff_hasSchurProperty assert_no_sorry UnitaryRepresentation.conjugate assert_no_sorry UnitaryRepresentation.linearIsometryEquiv_conjugate_apply assert_no_sorry UnitaryRepresentation.IsStronglyContinuous.conjugate assert_no_sorry UnitaryRepresentation.conjugateIntertwiningMap assert_no_sorry UnitaryRepresentation.conjugateInverseIntertwiningMap assert_no_sorry UnitaryRepresentation.conjugate_symm assert_no_sorry UnitaryRepresentation.conjugate_isTopologicallyIrreducible assert_no_sorry UnitaryRepresentation.conjugate_isTopologicallyIrreducible_iff assert_no_sorry LeanRidgelet.ha_reconstruction_of_intertwiner assert_no_sorry LeanRidgelet.ha_reconstruction_formula assert_no_sorry LeanRidgelet.invariantLpUnitaryRepresentation_apply_ae assert_no_sorry LeanRidgelet.quasiRegularAction_eLpNorm_two assert_no_sorry LeanRidgelet.quasiInvariantLpUnitaryRepresentation_apply_ae assert_no_sorry LeanRidgelet.twistedQuasiInvariantLpLinearIsometryEquiv assert_no_sorry LeanRidgelet.twistedQuasiInvariantLpLinearIsometryEquivMonoidHom assert_no_sorry LeanRidgelet.twistedQuasiInvariantLpUnitaryRepresentation assert_no_sorry LeanRidgelet.twistedQuasiInvariantLpUnitaryRepresentation_apply_ae assert_no_sorry LeanRidgelet.exists_quasiInvariantLpUnitaryRepresentation assert_no_sorry LeanRidgelet.bochnerSynthesis_intertwines assert_no_sorry LeanRidgelet.bochnerRidgelet_intertwines assert_no_sorry MeasureTheory.integral_eq_integral_smul_comp_smul_of_map_eq_withDensity assert_no_sorry NNReal.smul_inv_sqrt_smul assert_no_sorry MeasureTheory.measure_preimage_eq_nnreal_smul assert_no_sorry MeasureTheory.tendsto_measure_symmDiff_preimage_nhds_zero_of_map_eq_nnreal_smul assert_no_sorry UnitaryRepresentation.isStronglyContinuous_of_const_density assert_no_sorry LinearMap.det_adjoint assert_no_sorry LinearEquiv.det_skewProd assert_no_sorry MeasureTheory.Measure.map_affineEquiv_symm_addHaar_eq_withDensity assert_no_sorry MeasureTheory.integral_comp_linearEquiv_symm assert_no_sorry MeasureTheory.fourier_comp_linearEquiv_symm assert_no_sorry MeasureTheory.fourier_comp_sub assert_no_sorry MeasureTheory.affineEquiv_symm_apply assert_no_sorry MeasureTheory.fourier_comp_affineEquiv_symm assert_no_sorry MeasureTheory.fourier_weighted_comp_affineEquiv_symm assert_no_sorry MeasureTheory.unimodularMultiplierLinearIsometryEquiv assert_no_sorry MeasureTheory.unimodularMultiplierLinearIsometryEquiv_apply_ae assert_no_sorry LeanRidgelet.bochnerSynthesis_quasi_intertwines assert_no_sorry LeanRidgelet.bochnerRidgelet_quasi_intertwines assert_no_sorry LeanRidgelet.bochnerSynthesisIntertwiningMap assert_no_sorry LeanRidgelet.bochnerRidgeletIntertwiningMap assert_no_sorry LeanRidgelet.bochnerSynthesisQuasiIntertwiningMap assert_no_sorry LeanRidgelet.bochnerRidgeletQuasiIntertwiningMap assert_no_sorry LeanRidgelet.bochnerReconstructionQuasiIntertwiningMap assert_no_sorry LeanRidgelet.deepFeature assert_no_sorry LeanRidgelet.isJointEquivariant_deepFeature assert_no_sorry LeanRidgelet.deepRidgelet_reconstruction_formula assert_no_sorry LeanRidgelet.deepRidgelet_normalized_rightInverse assert_no_sorry LeanRidgelet.fullyConnectedFeature assert_no_sorry LeanRidgelet.fullyConnectedInputParameterTransform assert_no_sorry LeanRidgelet.fullyConnectedFeature_input_invariant assert_no_sorry LeanRidgelet.fullyConnectedOutputParameterTransform assert_no_sorry LeanRidgelet.fullyConnectedFeature_output_equivariant assert_no_sorry LeanRidgelet.deepFeature_mapFirst assert_no_sorry LeanRidgelet.deepFeature_mapLast assert_no_sorry LeanRidgelet.deepFullyConnectedFeature assert_no_sorry LeanRidgelet.deepFullyConnectedFeature_endpoint_equivariant assert_no_sorry LeanRidgelet.l2NetworkSynthesisMachine assert_no_sorry LeanRidgelet.l2RidgeletIntertwiningMap assert_no_sorry LeanRidgelet.norm_l2NetworkSynthesisMachine_le assert_no_sorry LeanRidgelet.l2_jointReconstructionOperator_eq assert_no_sorry LeanRidgelet.groupConvolutionalFeature assert_no_sorry LeanRidgelet.groupConvolutionalFeature_equivariant assert_no_sorry LeanRidgelet.groupConvolutionalSynthesis_eq_orbit assert_no_sorry LeanRidgelet.groupConvolutionalRidgelet_eq_base assert_no_sorry LeanRidgelet.groupConvolutional_reconstruction assert_no_sorry LeanRidgelet.groupConvolutional_synthesis_ridgelet assert_no_sorry LeanRidgelet.symmetricSubmodule assert_no_sorry LeanRidgelet.quadraticCongrEndo assert_no_sorry LeanRidgelet.quadraticEval assert_no_sorry LeanRidgelet.isSelfAdjoint_congr assert_no_sorry LeanRidgelet.quadraticCongrMap assert_no_sorry LeanRidgelet.quadraticCongr assert_no_sorry LeanRidgelet.inner_quadraticCongr assert_no_sorry LeanRidgelet.quadraticFeature assert_no_sorry LeanRidgelet.quadraticShearVector assert_no_sorry LeanRidgelet.quadraticLinearEquiv assert_no_sorry LeanRidgelet.quadraticSymmetricShear assert_no_sorry LeanRidgelet.quadraticParameterLinearEquiv assert_no_sorry LeanRidgelet.quadraticArgument_invariant assert_no_sorry LeanRidgelet.quadraticFeature_invariant assert_no_sorry LeanRidgelet.quadraticArgument_parameter_injective assert_no_sorry LeanRidgelet.quadraticParameterMulAction assert_no_sorry LeanRidgelet.det_quadraticParameterLinearEquiv assert_no_sorry LeanRidgelet.quadraticParameterLinearEquiv_one assert_no_sorry LeanRidgelet.quadraticParameterLinearEquiv_mul assert_no_sorry LeanRidgelet.quadraticParameterLinearEquiv_inv assert_no_sorry LeanRidgelet.quadraticParameterJacobian assert_no_sorry LeanRidgelet.quadraticParameterJacobian_cocycle assert_no_sorry LeanRidgelet.quadraticParameterJacobian_ne_zero assert_no_sorry LeanRidgelet.quadraticParameterJacobian_eq_blocks assert_no_sorry LeanRidgelet.quadraticParameter_measurable assert_no_sorry LeanRidgelet.quadraticParameter_map_eq_withDensity assert_no_sorry LeanRidgelet.quadraticParameter_group_map_eq_withDensity assert_no_sorry LeanRidgelet.quadraticParameterLpUnitaryRepresentation assert_no_sorry Matrix.symmetricSubmodule assert_no_sorry Matrix.symmetricBasis assert_no_sorry Matrix.congrMap assert_no_sorry Matrix.det_congrMap_diagonal assert_no_sorry Matrix.det_congrMap_transvection assert_no_sorry Matrix.det_congrMap assert_no_sorry ContinuousLinearMap.congrSelfAdjoint assert_no_sorry ContinuousLinearMap.selfAdjointEquivSymmetric assert_no_sorry ContinuousLinearMap.det_congrSelfAdjoint assert_no_sorry MeasureTheory.Measure.map_withDensity_of_map_eq_smul assert_no_sorry MeasureTheory.Measure.map_restrict_of_map_eq_smul assert_no_sorry LeanRidgelet.quadraticSymmetricEquivSelfAdjoint assert_no_sorry LeanRidgelet.det_quadraticCongr assert_no_sorry LeanRidgelet.det_quadraticCongr_apply assert_no_sorry LeanRidgelet.quadraticSymmetricDet_smul assert_no_sorry LeanRidgelet.preimage_smul_quadraticNondegenerate assert_no_sorry LeanRidgelet.quadraticRelativeWeight assert_no_sorry LeanRidgelet.quadraticRelativeWeight_smul assert_no_sorry LeanRidgelet.quadraticRelativeParameterJacobian assert_no_sorry LeanRidgelet.quadraticRelativeParameterJacobian_cocycle assert_no_sorry LeanRidgelet.quadraticRelative_synthesis_radonNikodym_balance assert_no_sorry LeanRidgelet.quadraticRelative_ridgelet_radonNikodym_balance assert_no_sorry LeanRidgelet.nnnorm_det_quadraticParameterLinearEquiv assert_no_sorry LeanRidgelet.quadraticRelativeMeasure assert_no_sorry LeanRidgelet.quadraticRelative_map_restrict assert_no_sorry LeanRidgelet.quadraticRelativeParameter_group_map_eq_withDensity assert_no_sorry LeanRidgelet.quadraticRelativeParameterLpUnitaryRepresentation assert_no_sorry LeanRidgelet.quadraticVectorFeature_jointInvariant assert_no_sorry LeanRidgelet.quadraticRelativeBochnerSynthesis_intertwines assert_no_sorry LeanRidgelet.quadraticRelativeBochnerRidgelet_intertwines assert_no_sorry LeanRidgelet.quadraticReconstructionOperator_eq_smul_id assert_no_sorry LeanRidgelet.quadraticNormalizedRidgelet_rightInverse assert_no_sorry LeanRidgelet.quadratic_reconstruction assert_no_sorry LeanRidgelet.QuadraticMachine assert_no_sorry LeanRidgelet.QuadraticRidgelet assert_no_sorry LeanRidgelet.quadraticReconstructionScalar assert_no_sorry LeanRidgelet.quadraticReconstructionOperator_eq_scalar_smul_id assert_no_sorry LeanRidgelet.quadraticReconstruction_apply assert_no_sorry LeanRidgelet.quadraticReconstructionScalar_ne_zero assert_no_sorry LeanRidgelet.inner_quadraticReconstruction assert_no_sorry LeanRidgelet.quadratic_reconstruction_nonzero_of_apply_ne_zero assert_no_sorry LeanRidgelet.QuadraticAnalysisBound assert_no_sorry LeanRidgelet.QuadraticSynthesisBound assert_no_sorry LeanRidgelet.QuadraticFixedShapeParameter assert_no_sorry LeanRidgelet.quadraticFixedShapeFeature assert_no_sorry LeanRidgelet.quadraticFixedShapeEmbedding assert_no_sorry LeanRidgelet.quadraticVectorFeature_quadraticFixedShapeEmbedding assert_no_sorry LeanRidgelet.quadraticFixedShapeEnergy assert_no_sorry LeanRidgelet.quadraticFixedShapeConstant assert_no_sorry LeanRidgelet.quadraticFixedShapeConstant_self assert_no_sorry LeanRidgelet.quadraticFixedShapeEnergy_pos assert_no_sorry LeanRidgelet.quadraticFixedShapeConstant_self_pos assert_no_sorry LeanRidgelet.lintegral_enorm_bochnerRidgelet_quadraticFixedShapeFeature_sq assert_no_sorry LeanRidgelet.memLp_two_bochnerRidgelet_quadraticFixedShapeFeature assert_no_sorry LeanRidgelet.integral_inner_bochnerRidgelet_quadraticFixedShapeFeature assert_no_sorry LeanRidgelet.integral_inner_bochnerSynthesis_bochnerRidgelet_quadraticFixedShapeFeature assert_no_sorry LeanRidgelet.bochnerSynthesis_bochnerRidgelet_quadraticFixedShapeFeature_ae_eq assert_no_sorry LeanRidgelet.quadraticFixedShapeRidgelet assert_no_sorry LeanRidgelet.norm_quadraticFixedShapeRidgeletLinearMap assert_no_sorry LeanRidgelet.quadraticFixedShapeRidgelet_apply_ae assert_no_sorry LeanRidgelet.quadratic_fixedShape_reconstruction_of_ae_eq assert_no_sorry LeanRidgelet.quadratic_fixedShape_reconstruction assert_no_sorry LeanRidgelet.inner_quadraticFixedShapeRidgelet assert_no_sorry LeanRidgelet.quadratic_fixedShape_rightInverse assert_no_sorry LeanRidgelet.quadratic_fixedShape_reconstruction_self assert_no_sorry MeasureTheory.integral_integral_mul_cexp_quadratic_mul_conj assert_no_sorry MeasureTheory.integral_integral_quadraticLevelShift_mul_conj assert_no_sorry MeasureTheory.integral_quadraticLevelShift_mul_conj assert_no_sorry MeasureTheory.memLp_two_quadraticLevelShift assert_no_sorry Real.fourierIntegral_conj assert_no_sorry MeasureTheory.Lp.integrableSubmodule assert_no_sorry MeasureTheory.Lp.denseRange_integrableSubmodule_subtypeL assert_no_sorry LeanRidgelet.affineData_quasiUnitaryPullbackAction_congr_ae assert_no_sorry LeanRidgelet.quadraticRelative_quasiRegularAction_congr_ae assert_no_sorry LeanRidgelet.quadraticSynthesisKernel assert_no_sorry LeanRidgelet.quadraticAnalysisKernel assert_no_sorry LeanRidgelet.quadraticMachine assert_no_sorry LeanRidgelet.quadraticRidgelet assert_no_sorry LeanRidgelet.norm_quadraticMachine_le assert_no_sorry LeanRidgelet.norm_quadraticRidgelet_le assert_no_sorry LeanRidgelet.coeFn_quadraticMachine assert_no_sorry LeanRidgelet.coeFn_quadraticRidgelet assert_no_sorry LeanRidgelet.quasiUnitaryPullbackAction_one_eq assert_no_sorry LeanRidgelet.quadraticRelativeParameterLpUnitaryRepresentation_apply_ae assert_no_sorry LeanRidgelet.quadraticMachine_intertwines assert_no_sorry LeanRidgelet.quadraticRidgelet_intertwines assert_no_sorry LeanRidgelet.quadraticEquivariantMachine assert_no_sorry LeanRidgelet.quadraticEquivariantRidgelet assert_no_sorry LeanRidgelet.quadratic_reconstruction_of_memLp assert_no_sorry LeanRidgelet.quadraticCompositeKernel assert_no_sorry LeanRidgelet.quadraticCompositeOperator assert_no_sorry LeanRidgelet.norm_quadraticCompositeOperator_le assert_no_sorry LeanRidgelet.coeFn_quadraticCompositeOperator assert_no_sorry LeanRidgelet.bochnerRidgelet_quadraticVectorFeature_congr_ae assert_no_sorry LeanRidgelet.quadraticCompositeOperator_intertwines assert_no_sorry LeanRidgelet.quadraticCompositeIntertwiner assert_no_sorry LeanRidgelet.quadraticComposite_reconstruction assert_no_sorry MeasureTheory.eLpNorm_integral_weighted_le assert_no_sorry LeanRidgelet.quadraticArgument_const_add assert_no_sorry LeanRidgelet.hasDerivAt_quadraticAnalysisPairing assert_no_sorry LeanRidgelet.hasDerivAt_bochnerRidgelet_quadraticVectorFeature assert_no_sorry LeanRidgelet.iteratedDeriv_bochnerRidgelet_quadraticVectorFeature assert_no_sorry MeasureTheory.Measure.map_withDensity_measurableEquiv assert_no_sorry MeasureTheory.Measure.exists_map_prodAssoc_symm_eq_smul_prod assert_no_sorry MeasureTheory.Measure.preimage_prodAssoc_symm_prod_univ assert_no_sorry MeasureTheory.Measure.map_prodAssoc_symm_restrict_of_map_eq_smul assert_no_sorry MeasureTheory.Measure.map_prodAssoc_symm_withDensity_of_map_eq_smul assert_no_sorry LeanRidgelet.quadraticBaseLinearEquiv assert_no_sorry LeanRidgelet.quadraticConstShift assert_no_sorry LeanRidgelet.quadraticParameterLinearEquiv_apply_shear assert_no_sorry LeanRidgelet.quadraticParameterLinearEquiv_eq_shear assert_no_sorry LeanRidgelet.exists_quadraticParameterLinearEquiv_shear assert_no_sorry LeanRidgelet.quadraticParameterLinearEquiv_apply_const_add assert_no_sorry LeanRidgelet.quadraticConstSlice assert_no_sorry LeanRidgelet.quadraticConstSlice_comp_smul assert_no_sorry LeanRidgelet.hasDerivAt_quadraticConstSlice_comp_smul assert_no_sorry LeanRidgelet.iteratedDeriv_quadraticConstSlice_comp_smul assert_no_sorry LeanRidgelet.quadraticConstIteratedDeriv assert_no_sorry LeanRidgelet.quadraticConstIteratedDeriv_comp_smul assert_no_sorry LeanRidgelet.eLpNorm_iteratedDeriv_quadraticConstSlice_comp_smul assert_no_sorry LeanRidgelet.lintegral_comp_smul_quadraticRelativeMeasure assert_no_sorry LeanRidgelet.lintegral_enorm_quadraticConstIteratedDeriv_comp_smul assert_no_sorry LeanRidgelet.lintegral_base_enorm_quadraticConstIteratedDeriv_comp_smul assert_no_sorry LeanRidgelet.quadraticBaseDet assert_no_sorry LeanRidgelet.quadraticNondegenerate_eq_preimage assert_no_sorry LeanRidgelet.quadraticRelativeWeight_eq_quadraticBaseWeight assert_no_sorry LeanRidgelet.quadraticBaseRelativeMeasure assert_no_sorry LeanRidgelet.measurable_quadraticBaseWeight assert_no_sorry LeanRidgelet.exists_map_prodAssoc_symm_quadraticRelativeMeasure_eq_smul assert_no_sorry LeanRidgelet.lintegral_quadraticRelativeMeasure_of_map_eq_smul assert_no_sorry LeanRidgelet.exists_lintegral_quadraticRelativeMeasure_eq_mul_lintegral assert_no_sorry LeanRidgelet.aestronglyMeasurable_bochnerRidgelet assert_no_sorry LeanRidgelet.stronglyMeasurable_bochnerRidgelet assert_no_sorry LeanRidgelet.aestronglyMeasurable_bochnerSynthesis assert_no_sorry LeanRidgelet.stronglyMeasurable_bochnerSynthesis assert_no_sorry LeanRidgelet.continuous_uncurry_quadraticArgument assert_no_sorry LeanRidgelet.continuous_uncurry_quadraticVectorFeature assert_no_sorry LeanRidgelet.measurable_uncurry_quadraticArgument assert_no_sorry LeanRidgelet.stronglyMeasurable_uncurry_quadraticVectorFeature assert_no_sorry LeanRidgelet.measurable_uncurry_quadraticVectorFeature assert_no_sorry LeanRidgelet.stronglyMeasurable_bochnerRidgelet_quadraticVectorFeature assert_no_sorry LeanRidgelet.aestronglyMeasurable_bochnerRidgelet_quadraticVectorFeature assert_no_sorry LeanRidgelet.continuous_quadraticVectorFeature assert_no_sorry LeanRidgelet.quadraticFeatureBoundedContinuous assert_no_sorry LeanRidgelet.quadraticFeatureBoundedContinuous_apply assert_no_sorry LeanRidgelet.exists_finite_quadraticNetwork_approx assert_no_sorry LeanRidgelet.secondDifference assert_no_sorry LeanRidgelet.secondDifference_apply assert_no_sorry LeanRidgelet.secondDifference_neg assert_no_sorry LeanRidgelet.hatFunction assert_no_sorry LeanRidgelet.hatFunction_nonneg assert_no_sorry LeanRidgelet.hatFunction_le assert_no_sorry LeanRidgelet.hatFunction_eq_zero_of_le assert_no_sorry LeanRidgelet.hatFunction_zero assert_no_sorry LeanRidgelet.continuous_hatFunction assert_no_sorry LeanRidgelet.hasCompactSupport_hatFunction assert_no_sorry LeanRidgelet.integrable_hatFunction assert_no_sorry LeanRidgelet.secondDifference_relu assert_no_sorry LeanRidgelet.integral_hatFunction_pos assert_no_sorry LeanRidgelet.reluComplex assert_no_sorry LeanRidgelet.hatComplex assert_no_sorry LeanRidgelet.continuous_hatComplex assert_no_sorry LeanRidgelet.norm_hatComplex_le assert_no_sorry LeanRidgelet.secondDifference_reluComplex assert_no_sorry LeanRidgelet.quadraticConstSecondDifference assert_no_sorry LeanRidgelet.quadraticConstSecondDifference_apply assert_no_sorry LeanRidgelet.quadraticConstSecondDifference_eq_slice assert_no_sorry LeanRidgelet.quadraticConstSecondDifference_comp_smul assert_no_sorry LeanRidgelet.quadraticArgument_const_shift assert_no_sorry LeanRidgelet.bochnerRidgelet_secondDifference_feature assert_no_sorry LeanRidgelet.quadraticConstTranslate assert_no_sorry LeanRidgelet.quadraticConstTranslate_apply assert_no_sorry LeanRidgelet.quadraticArgument_quadraticConstTranslate assert_no_sorry LeanRidgelet.integral_comp_quadraticConstTranslate assert_no_sorry LeanRidgelet.integrable_comp_quadraticConstTranslate assert_no_sorry LeanRidgelet.bochnerSynthesis_quadraticConstSecondDifference assert_no_sorry LeanRidgelet.bochnerSynthesis_bochnerRidgelet_reluComplex_secondDifference assert_no_sorry LeanRidgelet.not_bochnerSynthesis_bochnerRidgelet_reluComplex_ae_zero assert_no_sorry LeanRidgelet.quadraticHatFeatureBoundedContinuous assert_no_sorry LeanRidgelet.quadraticHatFeatureBoundedContinuous_apply assert_no_sorry LeanRidgelet.exists_finite_quadraticNetwork_approx_hat assert_no_sorry MeasureTheory.stronglyMeasurable_iteratedDeriv_succ assert_no_sorry MeasureTheory.stronglyMeasurable_iteratedDeriv assert_no_sorry MeasureTheory.parametricDeriv assert_no_sorry MeasureTheory.parametricIteratedDeriv assert_no_sorry MeasureTheory.parametricDeriv_slice assert_no_sorry MeasureTheory.parametricIteratedDeriv_slice assert_no_sorry MeasureTheory.parametricIteratedDeriv_zero assert_no_sorry MeasureTheory.parametricIteratedDeriv_succ assert_no_sorry MeasureTheory.parametricIteratedDeriv_succ' assert_no_sorry MeasureTheory.measurable_parametricDeriv_of_continuous assert_no_sorry MeasureTheory.measurable_parametricIteratedDeriv_succ_of_continuous assert_no_sorry MeasureTheory.contDiff_parametricDeriv assert_no_sorry MeasureTheory.continuous_parametricIteratedDeriv assert_no_sorry MeasureTheory.measurable_parametricIteratedDeriv assert_no_sorry MeasureTheory.measurable_parametricIteratedDeriv_succ assert_no_sorry LeanRidgelet.quadraticParameterPair assert_no_sorry LeanRidgelet.quadraticConstPair assert_no_sorry LeanRidgelet.continuous_quadraticParameterPair assert_no_sorry LeanRidgelet.quadraticConstPair_slice assert_no_sorry LeanRidgelet.quadraticConstIteratedDeriv_eq_parametric assert_no_sorry LeanRidgelet.iteratedDeriv_quadraticConstSlice_eq_parametric assert_no_sorry LeanRidgelet.contDiff_quadraticConstPair assert_no_sorry LeanRidgelet.aestronglyMeasurable_iteratedDeriv_quadraticConstSlice_succ assert_no_sorry LeanRidgelet.stronglyMeasurable_quadraticConstSlice assert_no_sorry LeanRidgelet.aestronglyMeasurable_iteratedDeriv_quadraticConstSlice assert_no_sorry LeanRidgelet.continuous_quadraticConstIteratedDeriv assert_no_sorry LeanRidgelet.measurable_quadraticConstIteratedDeriv assert_no_sorry LeanRidgelet.measurable_quadraticConstIteratedDeriv_succ assert_no_sorry LeanRidgelet.measurable_quadraticConstIteratedDeriv_of_eq assert_no_sorry LeanRidgelet.measurable_quadraticConstIteratedDeriv_bochnerRidgelet assert_no_sorry MeasureTheory.eLpNorm_two_sq_eq_lintegral_enorm_sq assert_no_sorry MeasureTheory.lintegral_enorm_mul_le_eLpNorm_two_mul_eLpNorm_two assert_no_sorry MeasureTheory.lpLinearMapOfPointwise assert_no_sorry MeasureTheory.coeFn_lpLinearMapOfPointwise assert_no_sorry MeasureTheory.lpOperatorOfPointwise assert_no_sorry MeasureTheory.lpOperatorOfPointwise_apply assert_no_sorry MeasureTheory.coeFn_lpOperatorOfPointwise assert_no_sorry MeasureTheory.norm_lpOperatorOfPointwise_le assert_no_sorry LeanRidgelet.quadraticConstIteratedDeriv_zero assert_no_sorry LeanRidgelet.quadraticConstIteratedDeriv_apply assert_no_sorry LeanRidgelet.quadraticConstIteratedDeriv_bochnerRidgelet assert_no_sorry LeanRidgelet.quadraticSobolevSeminorm assert_no_sorry LeanRidgelet.quadraticSobolevSeminorm_zero assert_no_sorry LeanRidgelet.eLpNorm_quadraticConstIteratedDeriv_le_quadraticSobolevSeminorm assert_no_sorry LeanRidgelet.eLpNorm_le_quadraticSobolevSeminorm assert_no_sorry LeanRidgelet.quadraticSobolevSeminorm_mono assert_no_sorry LeanRidgelet.MemQuadraticSobolev assert_no_sorry LeanRidgelet.MemQuadraticSobolev.memLp assert_no_sorry LeanRidgelet.quadraticSobolevSeminorm_comp_smul assert_no_sorry LeanRidgelet.MemQuadraticSobolev.comp_smul assert_no_sorry LeanRidgelet.quadraticBaseSobolevSeminorm assert_no_sorry LeanRidgelet.quadraticBaseSobolevSeminorm_eq_lintegral assert_no_sorry LeanRidgelet.quadraticBaseSobolevSeminorm_comp_smul assert_no_sorry LeanRidgelet.exists_quadraticSobolevSeminorm_eq_mul_quadraticBaseSobolevSeminorm assert_no_sorry LeanRidgelet.quadraticSobolevSeminorm_bochnerRidgelet assert_no_sorry LeanRidgelet.memQuadraticSobolev_bochnerRidgelet assert_no_sorry LeanRidgelet.enorm_bochnerSynthesis_le_quadraticSobolevSeminorm_mul assert_no_sorry LeanRidgelet.QuadraticCompositeEndomorphism assert_no_sorry LeanRidgelet.eLpNorm_bochnerSynthesis_bochnerRidgelet_le assert_no_sorry LeanRidgelet.quadraticComposite_intertwines_of_coeFn assert_no_sorry LeanRidgelet.exists_quadraticCompositeIntertwiner_of_bounds assert_no_sorry LeanRidgelet.quadratic_reconstruction_adjoint assert_no_sorry LeanRidgelet.bochnerSynthesis_eq_adjoint_bochnerRidgelet assert_no_sorry LeanRidgelet.quadratic_bochner_reconstruction_adjoint assert_no_sorry LeanRidgelet.QuadraticGammaMachine assert_no_sorry LeanRidgelet.QuadraticGammaRidgelet assert_no_sorry LeanRidgelet.quadratic_gamma_reconstruction assert_no_sorry LeanRidgelet.quadratic_gamma_reconstruction_of_ne_zero assert_no_sorry LeanRidgelet.exists_ne_zero_of_quadraticCompositeEndomorphism assert_no_sorry LeanRidgelet.measurable_quadraticConstIteratedDeriv_le_of_contDiff assert_no_sorry LeanRidgelet.quadraticSobolevSeminorm_comp_smul_of_contDiff assert_no_sorry LeanRidgelet.memQuadraticSobolev_of_contDiff assert_no_sorry LeanRidgelet.memQuadraticSobolev_bochnerRidgelet_of_stronglyMeasurable assert_no_sorry LeanRidgelet.QuadraticSobolevCarrier assert_no_sorry LeanRidgelet.norm_quadraticSobolevCarrier assert_no_sorry LeanRidgelet.MemQuadraticSobolev.memLp_quadraticConstIteratedDeriv assert_no_sorry LeanRidgelet.quadraticSobolevJet assert_no_sorry LeanRidgelet.quadraticSobolevJet_component assert_no_sorry LeanRidgelet.norm_quadraticSobolevJet assert_no_sorry LeanRidgelet.quadraticSobolevJets assert_no_sorry LeanRidgelet.quadraticSobolevSpace assert_no_sorry LeanRidgelet.isClosed_quadraticSobolevSpace assert_no_sorry LeanRidgelet.instCompleteSpaceQuadraticSobolevSpace assert_no_sorry LeanRidgelet.quadraticSobolevJet_mem_quadraticSobolevSpace assert_no_sorry LeanRidgelet.contDiff_comp_quadraticParameterSMul assert_no_sorry LeanRidgelet.contDiff_quadraticConstSlice assert_no_sorry LeanRidgelet.quadraticConstIteratedDeriv_const_smul assert_no_sorry LeanRidgelet.radonNikodymWeight_quadraticRelativeParameterJacobian_const assert_no_sorry LeanRidgelet.quadraticConstIteratedDeriv_quasiRegularAction assert_no_sorry LeanRidgelet.quadraticRelativeParameterLpIsometry assert_no_sorry LeanRidgelet.quadraticRelativeParameterLpIsometry_apply assert_no_sorry LeanRidgelet.quadraticSobolevCarrierAction assert_no_sorry LeanRidgelet.quadraticSobolevCarrierAction_component assert_no_sorry LeanRidgelet.norm_quadraticSobolevCarrierAction assert_no_sorry LeanRidgelet.quadraticSobolevCarrierAction_one assert_no_sorry LeanRidgelet.quadraticSobolevCarrierAction_mul assert_no_sorry LeanRidgelet.contDiff_quasiRegularAction assert_no_sorry LeanRidgelet.coeFn_quadraticRelativeParameterLpIsometry_toLp assert_no_sorry LeanRidgelet.quadraticSobolevSeminorm_quasiRegularAction assert_no_sorry LeanRidgelet.memQuadraticSobolev_quasiRegularAction assert_no_sorry LeanRidgelet.quadraticSobolevCarrierAction_quadraticSobolevJet assert_no_sorry LeanRidgelet.quadraticSobolevCarrierAction_mem_quadraticSobolevSpace assert_no_sorry LeanRidgelet.quadraticSobolevSpaceAction assert_no_sorry LeanRidgelet.quadraticSobolevSpaceAction_coe assert_no_sorry LeanRidgelet.norm_quadraticSobolevSpaceAction assert_no_sorry LeanRidgelet.quadraticSobolevSpaceActionMonoidHom assert_no_sorry LeanRidgelet.quadraticSobolevContRepresentation assert_no_sorry LeanRidgelet.quadraticSobolevContRepresentation_apply assert_no_sorry LeanRidgelet.eLpNorm_pow_smul_angularFourier_quadraticConstSlice assert_no_sorry LeanRidgelet.quadraticBaseSobolevSeminorm_eq_angularFourier assert_no_sorry LeanRidgelet.angularFourierIntegralInner_comp_const_add assert_no_sorry LeanRidgelet.eLpNorm_pow_smul_angularFourier_bochnerRidgelet_slice assert_no_sorry LeanRidgelet.memLp_two_pow_smul_angularFourier_bochnerRidgelet_slice assert_no_sorry MeasureTheory.Integrable.eLpNorm_fourier assert_no_sorry MeasureTheory.eLpNorm_iteratedDeriv_eq_eLpNorm_pow_smul_fourier assert_no_sorry MeasureTheory.memLp_two_pow_smul_fourier assert_no_sorry SchwartzMap.iteratedDeriv_eq_iterate_derivCLM assert_no_sorry SchwartzMap.integrable_iteratedDeriv assert_no_sorry SchwartzMap.memLp_two_iteratedDeriv assert_no_sorry SchwartzMap.eLpNorm_iteratedDeriv_eq_eLpNorm_pow_smul_fourier assert_no_sorry SchwartzMap.memLp_two_pow_smul_fourier assert_no_sorry LeanRidgelet.Fourier.angularFourierIntegralInner_iteratedDeriv assert_no_sorry LeanRidgelet.Fourier.lintegral_enorm_pow_smul_angularFourierIntegralInner_sq assert_no_sorry LeanRidgelet.Fourier.eLpNorm_pow_smul_angularFourierIntegralInner assert_no_sorry LeanRidgelet.Fourier.memLp_two_pow_smul_angularFourierIntegralInner assert_no_sorry LeanRidgelet.Fourier.eLpNorm_pow_smul_angularFourierIntegralInner_of_schwartz assert_no_sorry LeanRidgelet.Fourier.memLp_two_pow_smul_angularFourierIntegralInner_of_schwartz assert_no_sorry MeasureTheory.exists_fin_measurable_partition_subset_ball assert_no_sorry MeasureTheory.integrable_of_lipschitzWith assert_no_sorry MeasureTheory.exists_finsetSum_approx_integral_of_lipschitz assert_no_sorry MeasureTheory.exists_finsetSum_approx_integral_boundedContinuous_of_lipschitz assert_no_sorry MeasureTheory.eLpNorm_rpow_toReal_eq_lintegral assert_no_sorry MeasureTheory.lintegral_eLpNorm_rpow_prodMk_left assert_no_sorry MeasureTheory.MemLp.prodMk_left assert_no_sorry MeasureTheory.enorm_integral_mul_conj_le assert_no_sorry MeasureTheory.integrable_mul_conj assert_no_sorry MeasureTheory.integrable_mul_conj_kernel_ae assert_no_sorry MeasureTheory.enorm_integral_mul_conj_kernel_le_ae assert_no_sorry MeasureTheory.aestronglyMeasurable_integral_mul_conj_kernel assert_no_sorry MeasureTheory.eLpNorm_integral_mul_conj_kernel_le assert_no_sorry MeasureTheory.memLp_integral_mul_conj_kernel assert_no_sorry MeasureTheory.eLpNorm_prod_swap assert_no_sorry MeasureTheory.MemLp.prod_swap assert_no_sorry MeasureTheory.eLpNorm_integral_feature_analysis_le assert_no_sorry MeasureTheory.memLp_integral_feature_analysis assert_no_sorry MeasureTheory.eLpNorm_integral_feature_composite_le assert_no_sorry MeasureTheory.memLp_integral_feature_composite assert_no_sorry MeasureTheory.hilbertSchmidtKernelLinearMap assert_no_sorry MeasureTheory.coeFn_hilbertSchmidtKernelLinearMap assert_no_sorry MeasureTheory.norm_hilbertSchmidtKernelLinearMap_le assert_no_sorry MeasureTheory.hilbertSchmidtKernelOperator assert_no_sorry MeasureTheory.coeFn_hilbertSchmidtKernelOperator assert_no_sorry MeasureTheory.norm_hilbertSchmidtKernelOperator_le assert_no_sorry LeanRidgelet.bochnerSynthesis_affineFeature_eq_euclideanDualRidgeletTransform assert_no_sorry LeanRidgelet.bochnerRidgelet_affineFeature_eq_euclideanRidgeletTransform assert_no_sorry LeanRidgelet.bochnerSynthesis_affineFeature_eq_classicalSynthesisIntegral assert_no_sorry LeanRidgelet.affineBochner_reconstruction_of_euclidean assert_no_sorry LeanRidgelet.networkSynthesis_ae_eq_bochnerSynthesis_affineFeature assert_no_sorry LeanRidgelet.isAddHaarMeasure_volume_ridgeParameter assert_no_sorry LeanRidgelet.quasiMeasurePreserving_affineData_inv assert_no_sorry LeanRidgelet.quasiUnitaryPullbackAction_affineData_congr_ae assert_no_sorry LeanRidgelet.affineSchwartzParameterAction assert_no_sorry LeanRidgelet.networkSynthesis_parameterSchwartzRealization_ae_intertwines assert_no_sorry LeanRidgelet.euclideanRidgeletTransform_intertwines assert_no_sorry LeanRidgelet.classicalRidgeletIntegral_eq_euclideanRidgeletTransform assert_no_sorry LeanRidgelet.classicalRidgeletIntegral_intertwines assert_no_sorry LeanRidgelet.bochnerSynthesis_quasi_intertwines_of_character assert_no_sorry LeanRidgelet.bochnerRidgelet_quasi_intertwines_of_character assert_no_sorry LeanRidgelet.bochnerReconstruction_quasi_intertwines_of_character assert_no_sorry LeanRidgelet.bochnerReconstruction_commutes_of_character assert_no_sorry LeanRidgelet.character_eq_one_of_balance_of_mul_self_eq_one assert_no_sorry LeanRidgelet.measurableSet_truncationAnnulus assert_no_sorry LeanRidgelet.ae_parameter_fst_ne_zero assert_no_sorry LeanRidgelet.truncatedDualRidgeletTransform_eq_integral_indicator assert_no_sorry LeanRidgelet.tendsto_truncatedDualRidgeletTransform_of_integrable assert_no_sorry LeanRidgelet.det_affineParameterLinearEquiv assert_no_sorry LeanRidgelet.affineData_group_map_eq_withDensity assert_no_sorry LeanRidgelet.affineParameter_group_map_eq_withDensity assert_no_sorry LeanRidgelet.affineDataLpUnitaryRepresentation assert_no_sorry LeanRidgelet.affineParameterLpUnitaryRepresentation assert_no_sorry LinearEquiv.exists_apply_eq_of_ne_zero assert_no_sorry LinearEquiv.contragredientHom assert_no_sorry LinearEquiv.exists_symm_adjoint_apply_eq_of_ne_zero assert_no_sorry MeasureTheory.setOf_ne_zero_ae_eq_univ assert_no_sorry Units.instPolishSpaceOfNormedRing assert_no_sorry SemidirectProduct.homeomorphProd assert_no_sorry SemidirectProduct.instMeasurableSpace assert_no_sorry SemidirectProduct.instBorelSpace assert_no_sorry SemidirectProduct.instSecondCountableTopology assert_no_sorry SemidirectProduct.instPolishSpace assert_no_sorry SemidirectProduct.isTopologicalGroupOfContinuous assert_no_sorry AffineEquiv.semidirectProductEquiv assert_no_sorry AffineEquiv.continuous_continuousLinearMultiplicativeAction assert_no_sorry AffineEquiv.continuousLinearUnitsEquivLinearEquiv assert_no_sorry AffineEquiv.topologicalSemidirectProductEquiv assert_no_sorry AffineEquiv.det_topologicalSemidirectProductEquiv_linear assert_no_sorry AffineEquiv.topologicalSemidirectProductInverseContinuousMap assert_no_sorry AffineEquiv.continuous_topologicalSemidirectProductInverseContinuousMap assert_no_sorry UnitaryRepresentation.IsStronglyContinuous.restrict assert_no_sorry UnitaryRepresentation.restrict_isTopologicallyIrreducible_iff_of_surjective assert_no_sorry LeanRidgelet.affineDualOrbit_transitive assert_no_sorry LeanRidgelet.affineDualLittleGroup assert_no_sorry LeanRidgelet.affineTranslationCharacter assert_no_sorry LeanRidgelet.affineTranslationCharacter_linear_symm_apply assert_no_sorry LeanRidgelet.affineTranslationCharacter_linear_apply assert_no_sorry LeanRidgelet.affineTopologicalDualAction assert_no_sorry LeanRidgelet.continuous_affineTopologicalDualAction assert_no_sorry LeanRidgelet.affineTopologicalDualLittleGroup assert_no_sorry LeanRidgelet.affineTopologicalDualOrbit_transitive assert_no_sorry LeanRidgelet.affineTopologicalMackeySubgroup assert_no_sorry LeanRidgelet.instIsClosedAffineTopologicalMackeySubgroup assert_no_sorry LeanRidgelet.instSecondCountableTopologyAffineTopologicalMackeyQuotient assert_no_sorry LeanRidgelet.affineTopologicalDualOrbitMulAction assert_no_sorry LeanRidgelet.affineTopologicalDualOrbit_continuousSMul assert_no_sorry LeanRidgelet.affineTopologicalDualOrbit_isPretransitive assert_no_sorry LeanRidgelet.isOpenMap_affineTopologicalMackeyOrbitMap assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotientEquivDualOrbit assert_no_sorry LeanRidgelet.continuous_affineTopologicalMackeyQuotientOrbitMap assert_no_sorry LeanRidgelet.isOpenMap_affineTopologicalMackeyQuotientOrbitMap assert_no_sorry LeanRidgelet.continuous_affineTopologicalMackeyQuotientEquivDualOrbit assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotientHomeomorphDualOrbit assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotientHomeomorphDualOrbit_smul assert_no_sorry LeanRidgelet.affineTopologicalMackeyCharacter assert_no_sorry LeanRidgelet.affineTopologicalMackeyUnitaryRepresentation_isStronglyContinuous assert_no_sorry LeanRidgelet.affineTopologicalMackeyUnitaryRepresentation_isTopologicallyIrreducible assert_no_sorry LeanRidgelet.affineDualOrbit_ae_eq_univ assert_no_sorry LeanRidgelet.measurableSet_affineDualOrbit assert_no_sorry LeanRidgelet.affineDualOrbitSubtypeMeasure assert_no_sorry LeanRidgelet.affineDualOrbitSubtypeMeasure_map_subtypeVal assert_no_sorry LeanRidgelet.affineTopologicalDualJacobian assert_no_sorry LeanRidgelet.affineTopologicalDualJacobian_eq_inv assert_no_sorry LeanRidgelet.affineDualOrbitSubtypeMeasure_map_inv_smul assert_no_sorry LeanRidgelet.affineDualOrbitSubtype_quasiMeasurePreserving assert_no_sorry LeanRidgelet.affineDualOrbitSubtype_measurePreserving assert_no_sorry LeanRidgelet.affineDualOrbitRestrictionLpLinearIsometry assert_no_sorry LeanRidgelet.affineDualOrbitRestrictionLpLinearIsometry_apply_ae assert_no_sorry LeanRidgelet.affineDualOrbitRestrictionLpLinearIsometry_surjective assert_no_sorry LeanRidgelet.affineDualOrbitSubtypeLpEquiv assert_no_sorry LeanRidgelet.affineDualOrbitSubtypeLpEquiv_apply assert_no_sorry LeanRidgelet.affineDualOrbitSubtypeLpEquiv_symm_apply_ae assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotientMeasure assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotient_measurePreserving assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotient_symm_measurePreserving assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotientJacobian assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotientMeasure_map_inv_smul assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotientJacobian_cocycle assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotientMeasure_map_eq_withDensity assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotientRadonNikodymWeight assert_no_sorry LeanRidgelet.affineTopologicalMackeySection assert_no_sorry LeanRidgelet.affineTopologicalMackeySection_rightInverse assert_no_sorry LeanRidgelet.affineTopologicalMackeySectionCocycle assert_no_sorry LeanRidgelet.affineTopologicalMackeySectionPhase assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotientHomeomorphDualOrbit_eq_out assert_no_sorry LeanRidgelet.affineTopologicalMackeySectionPhase_eq_quotientPhase assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotientPhase assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotientPhase_cocycle assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotientPhase_norm_one assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotientPhase_one assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotientPhase_translation assert_no_sorry LeanRidgelet.affineTopologicalMackeySectionPhase_cocycle assert_no_sorry LeanRidgelet.affineTopologicalMackeySectionPhase_one assert_no_sorry LeanRidgelet.continuous_affineTopologicalMackeySectionPhase assert_no_sorry LeanRidgelet.continuous_uncurry_affineTopologicalMackeySectionPhase assert_no_sorry LeanRidgelet.affineTopologicalMackeySectionPhase_norm_one assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotientQuasiRegularLpUnitaryRepresentation assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotientQuasiRegularLpUnitaryRepresentation_apply_ae_explicit assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotientCharacterTwistedLpUnitaryRepresentation assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotientCharacterTwistedLpUnitaryRepresentation_apply_ae_explicit assert_no_sorry LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation assert_no_sorry LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_apply_ae_explicit assert_no_sorry LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_eq_quotient assert_no_sorry LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_indicator_covariant assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotientLpLinearIsometry assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotientLpLinearIsometry_apply_ae assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotientLpLinearIsometry_surjective assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotientLpEquiv assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotientLpEquiv_apply assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotientLpEquiv_symm_apply_ae assert_no_sorry LeanRidgelet.affineDualOrbitMeasure assert_no_sorry LeanRidgelet.affineDualOrbitMeasure_eq_volume assert_no_sorry LeanRidgelet.affineDualOrbitLpEquiv assert_no_sorry LeanRidgelet.affineTopologicalOrbitLpUnitaryRepresentation assert_no_sorry LeanRidgelet.affineTopologicalOrbitLpUnitaryRepresentation_apply_ae assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotientLpUnitaryRepresentation assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotientLpUnitaryRepresentation_apply_ae assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotientCharacterTwistedLpUnitaryRepresentation_eq_transported assert_no_sorry LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_eq_transported assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotientIntertwiningMap assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotientInverseIntertwiningMap assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotientLpUnitaryRepresentation_isStronglyContinuous assert_no_sorry LeanRidgelet.affineTopologicalMackeyQuotientLpUnitaryRepresentation_isTopologicallyIrreducible_iff assert_no_sorry LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_isStronglyContinuous assert_no_sorry LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_isTopologicallyIrreducible_iff assert_no_sorry LeanRidgelet.instIsOpenPosMeasureAffineDualOrbitSubtypeMeasure assert_no_sorry LeanRidgelet.instIsOpenPosMeasureAffineTopologicalMackeyQuotientMeasure assert_no_sorry LeanRidgelet.affineMackeyRegularSectionSMul assert_no_sorry LeanRidgelet.affineMackeyRegularSectionSMul_apply assert_no_sorry LeanRidgelet.affineMackeyRegularSectionToLp_coeFn_ae assert_no_sorry LeanRidgelet.affineMackeyRegularSectionToLp_smul assert_no_sorry LeanRidgelet.affineMackeyRegularSectionSMul_ne_zero assert_no_sorry LeanRidgelet.affineMackeyRegularSection_eq_zero_of_smul_eq_zero assert_no_sorry LeanRidgelet.affineMackeyInducingFiber_eq_bot_iff assert_no_sorry LeanRidgelet.affineMackeyInducingFiber_eq_top_of_ne_zero assert_no_sorry LeanRidgelet.affineMackey_regularSection_eq_zero_of_inducingFiber_eq_bot assert_no_sorry LeanRidgelet.affineMackey_eq_bot_of_inducingFiber_eq_bot assert_no_sorry LeanRidgelet.affineMackey_eq_top_of_regularSection_ne_zero assert_no_sorry LeanRidgelet.affineMackey_closedSubspace_extreme_iff_inducingFiber_extreme assert_no_sorry MeasureTheory.nontrivial_Lp_of_exists_measurableSet assert_no_sorry MeasureTheory.indicatorMemLp assert_no_sorry MeasureTheory.indicatorLpLinearMap assert_no_sorry MeasureTheory.indicatorLpLinearMap_apply_ae assert_no_sorry MeasureTheory.indicatorLp assert_no_sorry MeasureTheory.indicatorLp_apply_ae assert_no_sorry MeasureTheory.indicatorLp_comp_self assert_no_sorry MeasureTheory.indicatorLp_univ assert_no_sorry MeasureTheory.indicatorLp_empty assert_no_sorry MeasureTheory.indicatorLp_isSelfAdjoint assert_no_sorry MeasureTheory.indicatorLp_isStarProjection assert_no_sorry MeasureTheory.indicatorLp_mem_of_starProjection_commute assert_no_sorry MeasureTheory.ae_eq_zero_of_mem_orthogonal_of_indicatorLp_mem assert_no_sorry MeasureTheory.lmul_eq_mulLeft assert_no_sorry MeasureTheory.continuous_algebraNorm assert_no_sorry MeasureTheory.algebraNorm_units_ne_zero assert_no_sorry MeasureTheory.unitsHaarDensity assert_no_sorry MeasureTheory.unitsHaarDensity_mul assert_no_sorry MeasureTheory.unitsHaarDensity_one assert_no_sorry MeasureTheory.exists_unitsHaarDensity_le_of_isCompact assert_no_sorry MeasureTheory.map_mul_left_withDensity_unitsHaarDensity assert_no_sorry MeasureTheory.Measure.unitsHaar assert_no_sorry MeasureTheory.Measure.unitsHaar_apply assert_no_sorry MeasureTheory.units_val_image_preimage_mul_left assert_no_sorry MeasureTheory.Measure.isMulLeftInvariant_unitsHaar assert_no_sorry MeasureTheory.Measure.isFiniteMeasureOnCompacts_unitsHaar assert_no_sorry MeasureTheory.Measure.isOpenPosMeasure_unitsHaar assert_no_sorry MeasureTheory.Measure.isHaarMeasure_unitsHaar assert_no_sorry MeasureTheory.Measure.exists_haar_eq_smul_unitsHaar assert_no_sorry MeasureTheory.Measure.exists_map_units_val_haar_restrict_le assert_no_sorry MeasureTheory.map_mul_left_withDensity_monoidHom assert_no_sorry SemidirectProduct.prodMeasure assert_no_sorry SemidirectProduct.prodMeasure_apply assert_no_sorry SemidirectProduct.homeomorphProd_symm_comp_mul_left assert_no_sorry SemidirectProduct.isMulLeftInvariant_prodMeasure assert_no_sorry SemidirectProduct.isFiniteMeasureOnCompacts_prodMeasure assert_no_sorry SemidirectProduct.isOpenPosMeasure_prodMeasure assert_no_sorry SemidirectProduct.isHaarMeasure_prodMeasure assert_no_sorry SemidirectProduct.exists_haar_eq_smul_prodMeasure assert_no_sorry SemidirectProduct.exists_map_right_haar_restrict_le assert_no_sorry MeasureTheory.map_snd_restrict_prod_le assert_no_sorry LinearMap.exists_map_restrict_addHaar_le_smul_addHaar assert_no_sorry MeasureTheory.exists_map_continuousMulEquiv_haar_eq_smul_haar assert_no_sorry MeasureTheory.exists_map_continuousMulEquiv_haar_restrict_eq_smul_haar_restrict assert_no_sorry ContinuousLinearMap.contragredientUnit assert_no_sorry ContinuousLinearMap.contragredientUnit_mul assert_no_sorry ContinuousLinearMap.contragredientUnit_involutive assert_no_sorry ContinuousLinearMap.continuous_contragredientUnit assert_no_sorry ContinuousLinearMap.contragredientUnits assert_no_sorry ContinuousLinearMap.evalLinearMap assert_no_sorry ContinuousLinearMap.evalLinearMap_surjective assert_no_sorry ContinuousLinearMap.exists_map_contragredientOrbit_haar_restrict_le assert_no_sorry MeasureTheory.withDensity_restrict_le_smul_restrict assert_no_sorry LeanRidgelet.affineLinearDeterminantCharacter assert_no_sorry LeanRidgelet.affineLinearDeterminantCharacter_ne_zero assert_no_sorry LeanRidgelet.continuous_affineLinearDeterminantCharacter_real assert_no_sorry LeanRidgelet.exists_affineLinearDeterminantCharacter_le_of_isCompact assert_no_sorry LeanRidgelet.affine_map_orbitMap_haar_restrict_le assert_no_sorry LeanRidgelet.affineTopologicalMackeyOrbitMap_inv assert_no_sorry LeanRidgelet.affine_map_adjointOrbitMap_haar_restrict_le assert_no_sorry LeanRidgelet.affineMackeyLiftPhase assert_no_sorry LeanRidgelet.affineMackeyLiftPhase_norm_one assert_no_sorry LeanRidgelet.continuous_affineMackeyLiftPhase assert_no_sorry LeanRidgelet.affineMackeyLiftPhase_mul assert_no_sorry LeanRidgelet.affineMackeyLiftFun assert_no_sorry LeanRidgelet.norm_affineMackeyLiftFun assert_no_sorry LeanRidgelet.affineMackeyLiftFun_inv_mul assert_no_sorry LeanRidgelet.measurable_affineMackeyLiftFun assert_no_sorry MeasureTheory.integral_norm_restrict_le_norm_mul_rpow assert_no_sorry MeasureTheory.integral_L2_coeFn_ae_of_restrict_of_aefinStronglyMeasurable assert_no_sorry MeasureTheory.integral_L2_coeFn_ae_of_restrict assert_no_sorry LeanRidgelet.affine_map_quotientMk_inv_haar_restrict_le assert_no_sorry LeanRidgelet.locallyIntegrable_affineMackeyLiftFun_inv_of_bound assert_no_sorry LeanRidgelet.locallyIntegrable_affineMackeyLiftFun_inv assert_no_sorry LeanRidgelet.affineMackeySmoothingKernel assert_no_sorry LeanRidgelet.affineMackeySmoothingIntegrand assert_no_sorry LeanRidgelet.measurable_uncurry_affineMackeySmoothingIntegrand assert_no_sorry LeanRidgelet.affineMackeySmoothingIntegrand_ae_eq assert_no_sorry LeanRidgelet.integrable_uncurry_affineMackeySmoothingIntegrand assert_no_sorry LeanRidgelet.affineMackeySmoothingIntegral assert_no_sorry LeanRidgelet.affineMackeySmoothingIntegral_quotientMk assert_no_sorry LeanRidgelet.continuous_affineMackeySmoothingIntegral assert_no_sorry LeanRidgelet.affineMackeySmoothedVector_exists_continuousRepresentative assert_no_sorry LeanRidgelet.affineMackey_regularSection_dense assert_no_sorry LeanRidgelet.affineMackey_systemInvariant_closedSubspace_eq_bot_or_top assert_no_sorry LeanRidgelet.affineMackey_exists_scalar_of_isSelfAdjoint assert_no_sorry LeanRidgelet.affineMackey_scalar_of_commutes_indicators assert_no_sorry ContinuousLinearMap.adjointEvalLinearMap assert_no_sorry ContinuousLinearMap.adjointEvalLinearMap_surjective assert_no_sorry ContinuousLinearMap.exists_map_adjointOrbit_haar_restrict_le assert_no_sorry LeanRidgelet.affineDualOrbitIntertwiningMap assert_no_sorry LeanRidgelet.affineDualOrbitInverseIntertwiningMap assert_no_sorry LeanRidgelet.affineTopologicalOrbitLpUnitaryRepresentation_isStronglyContinuous assert_no_sorry LeanRidgelet.affineTopologicalOrbitLpUnitaryRepresentation_isTopologicallyIrreducible_iff assert_no_sorry LeanRidgelet.affine_eq_translation_mul_linear assert_no_sorry LeanRidgelet.affineDataLpUnitaryRepresentation_translation_apply_ae assert_no_sorry LeanRidgelet.affineDataLpUnitaryRepresentation_linear_apply_ae assert_no_sorry LeanRidgelet.affineTopologicalLpUnitaryRepresentation assert_no_sorry LeanRidgelet.affineTopologicalJacobian assert_no_sorry LeanRidgelet.affineTopologicalInverse_map_eq_smul assert_no_sorry LeanRidgelet.affineTopologicalLpUnitaryRepresentation_apply_ae assert_no_sorry LeanRidgelet.affineTopologicalLpUnitaryRepresentation_isStronglyContinuous assert_no_sorry LeanRidgelet.affineTopologicalLpUnitaryRepresentation_isTopologicallyIrreducible_iff assert_no_sorry LeanRidgelet.affineDataSchwartzAction assert_no_sorry LeanRidgelet.affineDataSchwartzAction_apply assert_no_sorry LeanRidgelet.affineDataLpUnitaryRepresentation_schwartz assert_no_sorry LeanRidgelet.affineDataLpUnitaryRepresentation_fourier_schwartz_ae assert_no_sorry LeanRidgelet.affineFourierLpUnitaryRepresentation assert_no_sorry LeanRidgelet.affineTopologicalFourierLpUnitaryRepresentation assert_no_sorry LeanRidgelet.affineFrequencyPhase_cocycle assert_no_sorry LeanRidgelet.affineTopologicalFourierLpUnitaryRepresentation_isStronglyContinuous assert_no_sorry LeanRidgelet.affinePlancherelIntertwiningMap assert_no_sorry LeanRidgelet.affinePlancherelInverseIntertwiningMap assert_no_sorry LeanRidgelet.affinePlancherelIntertwiningMap_intertwines assert_no_sorry LeanRidgelet.affineFourierLpUnitaryRepresentation_isTopologicallyIrreducible_iff assert_no_sorry LeanRidgelet.affineFourierLpUnitaryRepresentation_schwartz_ae assert_no_sorry LeanRidgelet.affineDualPullbackLpUnitaryRepresentation assert_no_sorry LeanRidgelet.affineDualPullbackLpUnitaryRepresentation_apply_ae assert_no_sorry LeanRidgelet.affineFrequencyLinearIsometryEquiv assert_no_sorry LeanRidgelet.affineFrequencyPhase_translation assert_no_sorry LeanRidgelet.affineFrequencyLinearIsometryEquiv_apply_ae assert_no_sorry LeanRidgelet.affineFrequencyLinearIsometryEquiv_eq_fourierRepresentation assert_no_sorry LeanRidgelet.affineFourierLpUnitaryRepresentation_apply_ae assert_no_sorry LeanRidgelet.affineBochnerSynthesis_intertwines assert_no_sorry LeanRidgelet.affineBochnerRidgelet_intertwines assert_no_sorry LeanRidgelet.fourierDilationTransformCore_norm_sq assert_no_sorry LeanRidgelet.continuous_fourierDilationTransformCore assert_no_sorry LeanRidgelet.fiberDistribution_coe assert_no_sorry LeanRidgelet.fiberBaseCoordinate_coe assert_no_sorry LeanRidgelet.angularFourierDistribution_ridgeletFunctionCore assert_no_sorry LeanRidgelet.ridgeletSpectrum_coe assert_no_sorry LeanRidgelet.ridgeletFunction_coe assert_no_sorry LeanRidgelet.angularFourierDistribution_ridgeletFunction assert_no_sorry LeanRidgelet.unitarySynthesis_comp_unitaryRidgelet assert_no_sorry LeanRidgelet.unitaryMoorePenroseInverse_rightInverse assert_no_sorry LeanRidgelet.hasSum_unitaryRidgelet_coefficients assert_no_sorry LeanRidgelet.hasSum_unitaryRidgelet_kernelBasis assert_no_sorry LeanRidgelet.hasSum_fiberRidgelet_coefficients assert_no_sorry LeanRidgelet.eq_fiberCoefficient_of_hasSum_fiberRidgelet assert_no_sorry LeanRidgelet.mem_fourierDilationCompatibilityDomain_iff_memLp assert_no_sorry LeanRidgelet.networkSynthesis_parameterSchwartzRealization_fourierPairing_ae assert_no_sorry LeanRidgelet.fourierDilationTransform_ridgeletOperator_apply_ae assert_no_sorry LeanRidgelet.mem_ker_networkSynthesis_iff_fourierDilation assert_no_sorry LeanRidgelet.normalizedGaussianRightInverse_rightInverse assert_no_sorry LeanRidgelet.l2_proposition_one_activation_hilbert_structure assert_no_sorry LeanRidgelet.l2_theorem_one_bounded_synthesis assert_no_sorry LeanRidgelet.l2_lemma_one_ridgelet_fiber_representation assert_no_sorry LeanRidgelet.l2_theorem_two_reconstruction assert_no_sorry LeanRidgelet.l2_lemma_two_adjoint assert_no_sorry LeanRidgelet.l2_theorem_three_null_space_and_general_solution assert_no_sorry LeanRidgelet.l1_ridgelet_pointwise_convergent_L1_bounded assert_no_sorry LeanRidgelet.l1_hasFourierAwayFromOrigin_add_polynomial assert_no_sorry LeanRidgelet.integral_pow_mul_angularFourier1D_eq_zero assert_no_sorry LeanRidgelet.l1_truncatedPower_hasFourierAwayFromOrigin assert_no_sorry LeanRidgelet.truncatedPowerFourier_pairing assert_no_sorry LeanRidgelet.l1_dualRidgeletTransform_pairing assert_no_sorry LeanRidgelet.l1_weakRidgeletTransform_eq_euclidean assert_no_sorry LeanRidgelet.l1_plancherel_identity assert_no_sorry LeanRidgelet.l1_ridgeletTransform_L2_extension assert_no_sorry MeasureTheory.Lp.dense_setOf_integrable assert_no_sorry MeasureTheory.tendsto_integral_mul_smoothing_of_vanishing_moments assert_no_sorry MeasureTheory.tendsto_integral_weight_norm_sub_comp_sub_right assert_no_sorry MeasureTheory.tendsto_integral_weight_norm_smoothing_sub assert_no_sorry LeanRidgelet.hasFourierAwayFromOrigin_pairing_extension assert_no_sorry LeanRidgelet.truncatedDualRidgeletTransform_eq_section_pairing assert_no_sorry LeanRidgelet.integrable_weight_truncatedReconstructionSection assert_no_sorry LeanRidgelet.integral_pow_mul_truncatedReconstructionSection_eq_zero assert_no_sorry LeanRidgelet.angularFourier1D_truncatedReconstructionSection assert_no_sorry LeanRidgelet.norm_truncatedSpectralFactor_le_of_ne assert_no_sorry LeanRidgelet.truncatedSpectralWindow_eq assert_no_sorry LeanRidgelet.integrableOn_fourierData_truncatedReconstructionSection assert_no_sorry LeanRidgelet.truncatedDualRidgeletTransform_eq_spectral_pairing assert_no_sorry LeanRidgelet.tendsto_truncatedDualRidgeletTransform assert_no_sorry LeanRidgelet.ae_integral_angularFourier_mul_exp assert_no_sorry LeanRidgelet.l1_reconstruction_formula assert_no_sorry LeanRidgelet.l1_reconstruction_formula_radon assert_no_sorry LeanRidgelet.l1_parseval_relation assert_no_sorry MeasureTheory.Integrable.integral_inner_fourier assert_no_sorry MeasureTheory.MemLp.integrable_mul_conj assert_no_sorry LeanRidgelet.Fourier.integral_angularFourierIntegralInner_mul_conj assert_no_sorry LeanRidgelet.Fourier.integral_angularFourierIntegralInner_mul_exp assert_no_sorry MeasureTheory.Integrable.fourierInv_fourier_ae_eq assert_no_sorry MeasureTheory.measurePreserving_prodSwapRight assert_no_sorry MeasureTheory.quasiMeasurePreserving_skewSubLeft assert_no_sorry LeanRidgelet.l1_reconstruction_formula_L2 assert_no_sorry LeanRidgelet.eLpNorm_truncatedDualRidgeletTransform_sub_le assert_no_sorry LeanRidgelet.setIntegral_annulus_ridgeletTransform_mul_conj assert_no_sorry LeanRidgelet.tendsto_setIntegral_compl_annulus_norm_sq assert_no_sorry LeanRidgelet.integrable_weight_indicator_euclideanRidgeletTransform assert_no_sorry LeanRidgelet.integral_norm_euclideanRidgeletTransform_bias_le assert_no_sorry LeanRidgelet.norm_truncatedDualRidgeletTransform_le assert_no_sorry LeanRidgelet.aestronglyMeasurable_truncatedDualRidgeletTransform assert_no_sorry MeasureTheory.eLpNorm_two_le_of_forall_indicator_pairing_le assert_no_sorry MeasureTheory.MemLp.norm_integral_mul_conj_le assert_no_sorry MeasureTheory.tendsto_intervalIntegral_sin_div_atTop assert_no_sorry MeasureTheory.abs_intervalIntegral_sin_div_le assert_no_sorry MeasureTheory.tendsto_intervalIntegral_sin_div_atTop_left assert_no_sorry MeasureTheory.abs_sinDivTail_le assert_no_sorry MeasureTheory.tendsto_sinDivTail_nhds_zero assert_no_sorry MeasureTheory.intervalIntegral_sin_mul_div_eq assert_no_sorry MeasureTheory.setIntegral_hilbert_eq_Ioi assert_no_sorry MeasureTheory.intervalIntegral_hilbert_eq_fourier assert_no_sorry MeasureTheory.setIntegral_hilbert_eq_fourier_tail assert_no_sorry MeasureTheory.pvHilbertTransform_schwartz assert_no_sorry MeasureTheory.pvHilbertTransform_schwartz_eq_fourierInv assert_no_sorry LeanRidgelet.lambdaOperatorPow_eq_fourier_multiplier assert_no_sorry LeanRidgelet.lambda_symbol_even assert_no_sorry LeanRidgelet.lambda_symbol_odd assert_no_sorry MeasureTheory.integral_eq_integral_prod_toSphere assert_no_sorry MeasureTheory.integrable_prod_toSphere_of_integrable assert_no_sorry MeasureTheory.integral_eq_integral_toSphere_integral_Ioi assert_no_sorry MeasureTheory.schwartz_norm_le_one_add_norm_rpow assert_no_sorry MeasureTheory.continuous_radonTransform_schwartz assert_no_sorry MeasureTheory.radonTransform_eq_radonSchwartzSection assert_no_sorry MeasureTheory.fourier_radonSchwartzSection assert_no_sorry MeasureTheory.integral_volumeIoiPow assert_no_sorry MeasureTheory.integrable_toSphere_integral_Ioi assert_no_sorry LeanRidgelet.l1_radon_filtered_backprojection assert_no_sorry LeanRidgelet.l1_relu_network_universal_approximation assert_no_sorry LeanRidgelet.l1_truncatedPower_admissible_exists assert_no_sorry LeanRidgelet.isAdmissiblePair_bumpRidgelet assert_no_sorry LeanRidgelet.admissibilityConstant_bumpRidgelet_ne_zero assert_no_sorry LeanRidgelet.integral_pow_mul_bumpRidgelet assert_no_sorry LeanRidgelet.integrable_weight_bumpRidgelet assert_no_sorry LeanRidgelet.angularFourier1D_bumpRidgelet assert_no_sorry LeanRidgelet.hasFourierAwayFromOrigin_lambdaOperatorPow assert_no_sorry mem_lizorkinSpace_iff_fourier_flat assert_no_sorry Real.iteratedDeriv_fourier_zero assert_no_sorry integral_polynomial_mul_eq_zero_of_mem_lizorkinSpace assert_no_sorry LeanRidgelet.bumpRidgeletSchwartz_mem_lizorkinSpace assert_no_sorry LeanRidgelet.lambdaOperatorPow_eq_angular assert_no_sorry LeanRidgelet.l1_structure_theorem_admissible_pairs assert_no_sorry LeanRidgelet.l1_construction_of_admissible_pairs assert_no_sorry LeanRidgelet.l1_isAdmissiblePair_lambdaOperatorPow assert_no_sorry LeanRidgelet.l1_truncatedPower_isAdmissiblePair_of_window assert_no_sorry LeanRidgelet.integrable_lambdaOperatorPow_of_even assert_no_sorry LeanRidgelet.integrable_lambdaOperatorPow assert_no_sorry LeanRidgelet.l1_truncatedPower_admissible assert_no_sorry LeanRidgelet.angularFourier1D_gaussianWindow assert_no_sorry Real.gaussianSchwartz assert_no_sorry Real.exists_polynomial_iteratedDeriv_gaussian assert_no_sorry Real.abs_pow_mul_exp_neg_sq_div_two_le assert_no_sorry LeanRidgelet.integral_iteratedDeriv_schwartz_eq_zero assert_no_sorry MeasureTheory.integrableOn_schwartz_oddDiff assert_no_sorry MeasureTheory.pvHilbertTransform_schwartz_eq_oddIntegral assert_no_sorry MeasureTheory.coord_mul_pvHilbertTransform assert_no_sorry MeasureTheory.memLp_two_pvHilbertTransform assert_no_sorry MeasureTheory.integrable_pvHilbertTransform_of_integral_eq_zero assert_no_sorry LeanRidgelet.l1_polynomial_not_isAdmissiblePair assert_no_sorry LeanRidgelet.l1_step_not_isAdmissiblePair_lambdaOperatorPow assert_no_sorry LeanRidgelet.hasFourierAwayFromOrigin_angularFourierInv assert_no_sorry LeanRidgelet.angularFourier1D_lambdaOperatorPow assert_no_sorry LeanRidgelet.l1_structure_theorem_sufficiency assert_no_sorry LeanRidgelet.l1_structure_theorem_sufficiency_physical assert_no_sorry LeanRidgelet.isAdmissiblePair_of_backprojection_ae assert_no_sorry LeanRidgelet.hasFourierAwayFromOrigin_ae_eq assert_no_sorry LeanRidgelet.hasFourierAwayFromOrigin_reflectedConjConvolution assert_no_sorry LeanRidgelet.angularFourier1D_mul_conj_angularFourier1D assert_no_sorry LeanRidgelet.integrable_abs_pow_mul_angularFourier1D assert_no_sorry LeanRidgelet.coe_angularSchwartz assert_no_sorry LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_hasSchurProperty assert_no_sorry LeanRidgelet.affineTopologicalMackeySectionInducedLpUnitaryRepresentation_isTopologicallyIrreducible assert_no_sorry LeanRidgelet.affineDataLpUnitaryRepresentation_isTopologicallyIrreducible #print axioms LeanRidgelet.Fourier.angular_plancherel_schwartz_inner #print axioms LeanRidgelet.fourierDilationTransformCore_norm_sq #print axioms LeanRidgelet.hasSum_fiberRidgelet_coefficients #print axioms LeanRidgelet.eq_fiberCoefficient_of_hasSum_fiberRidgelet #print axioms LeanRidgelet.normalizedGaussianRightInverse_rightInverse #print axioms LeanRidgelet.l2_theorem_three_null_space_and_general_solution #print axioms LeanRidgelet.l2_theorem_four_encoding_and_perturbative_readout #print axioms LeanRidgelet.l2_theorem_five_normalized_finite_width_approximation #print axioms LeanRidgelet.l2_corollary_one_discretizable_ridgelet_null_elements #print axioms LeanRidgelet.l2_proposition_two_exact_finite_null_relations #print axioms LeanRidgelet.quadratic_fixedShape_reconstruction #print axioms LeanRidgelet.quadratic_fixedShape_reconstruction_self end LeanRidgelet.Audit