| Name | Category | Theorems |
|---|
I 📖 | CompOp | 44 mathmath: sqrt_eq_ite, im_le_neg_norm_iff_eq_neg_I_mul_norm, map_apply, LinearMap.IsSymmetric.inner_map_polarization, re_add_im, norm_I_of_ne_zero, sub_conj, re_add_im_ax, im_inner_eq_norm_sub_i_smul_mul_self_sub_norm_add_i_smul_mul_self_div_four, I_mul_I, I_re_ax, LinearMap.extendTo𝕜'_apply, conj_I_ax, I_eq_zero_or_im_I_eq_one, LinearMap.extendTo𝕜_apply, inner_eq_sum_norm_sq_div_four, im_eq_conj_sub, sqrt_eq_real_add_ite, I_im, sqrt_neg_one, I_to_real, ContinuousLinearMap.extendTo𝕜_apply, mul_im_I_ax, integral_coe_re_add_coe_im, sqrt_neg_I, conj_I, sqrt_I, I_mul_re, ContinuousLinearMap.extendTo𝕜'_apply, I_re, setIntegral_re_add_im, conj_eq_re_sub_im, integral_re_add_im, norm_le_im_iff_eq_I_mul_norm, I_im', I_mul_I_of_nonzero, I_mul_I_ax, span_one_I, sqrt_neg_of_nonneg, conj_neg_I, inv_I, I_to_complex, div_I, real_inner_I_smul_self
|
algebraMapCoe 📖 | CompOp | — |
cauSeqIm 📖 | CompOp | — |
cauSeqRe 📖 | CompOp | — |
conjAe 📖 | CompOp | 2 mathmath: conjCLE_coe, conjAe_coe
|
conjCLE 📖 | CompOp | 3 mathmath: conjCLE_norm, conjCLE_apply, conjCLE_coe
|
conjLIE 📖 | CompOp | 1 mathmath: conjLIE_apply
|
conjToRingEquiv 📖 | CompOp | — |
copy_of_normedField 📖 | CompOp | — |
im 📖 | CompOp | 91 mathmath: sqrt_eq_ite, im_le_neg_norm_iff_eq_neg_I_mul_norm, map_apply, re_add_im, LinearMap.IsSymmetric.im_inner_self_apply, sub_conj, pos_iff, re_add_im_ax, is_real_TFAE, abs_im_div_norm_le_one, im_inner_eq_norm_sub_i_smul_mul_self_sub_norm_add_i_smul_mul_self_div_four, nonpos_iff, AEMeasurable.im, norm_sq_eq_def_ax, im_eq_zero_iff_isSelfAdjoint, mul_im_ax, im_ofReal_pow, inner_self_im, imLm_coe, div_im, im_to_real, ext_iff, InnerProductSpace.Core.inner_im_symm, I_eq_zero_or_im_I_eq_one, le_iff_re_im, im_eq_conj_sub, conj_im_ax, im_mul_ofReal, neg_iff, sqrt_eq_real_add_ite, inv_im, one_im, ofReal_im, abs_im_le_norm, nonneg_iff, smul_im, MeasureTheory.Integrable.re_im_iff, Measurable.im, norm_im_le_norm, I_im, ofNat_mul_im, isCauSeq_im, mul_im_I_ax, im_tsum, natCast_im, MeasureTheory.AEStronglyMeasurable.im, integral_coe_re_add_coe_im, lt_iff_re_im, im_eq_zero_of_le, conj_im, hasSum_iff, measurable_im, ofNat_im, norm_sq_eq_def, ratCast_im, I_mul_re, conj_eq_iff_im, MeasureTheory.MemLp.im, mul_im, im_sq_le_normSq, LinearMap.IsSymmetric.im_inner_apply_self, im_to_complex, norm_to_complex, mul_re, to_complex_nonneg_iff, im_ofReal_mul, im_eq_complex_im, ofReal_im_ax, InnerProductSpace.Core.inner_self_im, continuous_im, div_re, setIntegral_re_add_im, conj_eq_re_sub_im, normSq_apply, mul_re_ax, LinearMap.im_inner_adjoint_mul_self_eq_zero, integral_re_add_im, norm_le_im_iff_eq_I_mul_norm, hasSum_im, I_im', intCast_im, inner_im_symm, MeasureTheory.memLp_re_im_iff, imCLM_apply, lipschitzWith_im, integral_im, im_le_norm, Matrix.IsHermitian.im_star_dotProduct_mulVec_self, MeasureTheory.Integrable.im, zero_im, im_eq_zero
|
imCLM 📖 | CompOp | 2 mathmath: imCLM_coe, imCLM_apply
|
imLm 📖 | CompOp | 2 mathmath: imLm_coe, imCLM_coe
|
map 📖 | CompOp | 8 mathmath: map_from_real, map_apply, map_same_eq_id, sqrt_map, Complex.sqrt_map, map_nonneg_iff, toContinuousLinearMap_complexLinearIsometryEquiv, map_to_real
|
normSq 📖 | CompOp | 25 mathmath: normSq_to_real, normSq_neg, continuous_normSq, div_im, normSq_inv, normSq_nonneg, inv_im, normSq_mul, normSq_eq_def', normSq_pos, mul_self_norm, normSq_div, im_sq_le_normSq, re_sq_le_normSq, normSq_zero, normSq_eq_zero, normSq_to_complex, normSq_add, div_re, sqrt_normSq_eq_norm, normSq_apply, normSq_one, normSq_sub, normSq_conj, inv_re
|
ofReal 📖 | CompOp | 183 mathmath: sqrt_eq_ite, im_le_neg_norm_iff_eq_neg_I_mul_norm, measurable_ofReal, pos_iff_exists_ofReal, map_apply, ofRealCLM_apply, cfcₙ_norm_nonneg, div_re_ofReal, ofReal_inj, Matrix.IsHermitian.det_abs, ofRealLI_apply, re_add_im, algebraMap_eq_ofReal, sub_conj, re_sqrt_ofReal, norm_smul_inv_norm', CFC.abs_eq_cfcₙ_coe_norm, inner_eq_norm_mul_iff, Submodule.starProjection_singleton, ofReal_re, is_real_TFAE, Filter.tendsto_ofReal_iff', mul_conj, hasSum_ofReal, difference_quotients_converge_uniformly, ofReal_balance, norm_smul_inv_norm, nonpos_iff_exists_ofReal, realRingEquiv_symm_apply, Submodule.reflection_singleton_apply, ofReal_comp_balance, ofReal_sub, inner_self_eq_norm_sq_to_K, norm_ofReal, InnerProductSpace.Core.inner_smul_ofReal_right, ofReal_injective, LinearMap.IsSymmetric.coe_re_inner_self_apply, ofReal_nonneg, LinearMap.extendTo𝕜'_apply, Matrix.IsHermitian.charpoly_cfc_eq, im_ofReal_pow, inner_eq_norm_mul_iff_div, LinearMap.IsSymmetric.card_filter_eigenvalues_eq, LinearMap.IsSymmetric.hasEigenvalue_iSup_of_finiteDimensional, Polynomial.ofReal_eval, ofReal_natCast, conj_ofReal, inner_self_ofReal_re, summable_ofReal, ofReal_le_ofReal, conj_mul, ofReal_mul, Matrix.IsHermitian.trace_eq_sum_eigenvalues, IsSelfAdjoint.hasEigenvector_of_isMaxOn, conj_eq_iff_re, isUniformEmbedding_ofReal, LinearMap.extendTo𝕜_apply, inner_eq_sum_norm_sq_div_four, exists_norm_eq_mul_self, real_smul_eq_coe_smul, add_conj, im_eq_conj_sub, ofReal_add, MeasureTheory.L2.integral_inner_eq_sq_eLpNorm, ofReal_neg, ofReal_zpow, im_mul_ofReal, inner_smul_real_right, sqrt_eq_real_add_ite, ofReal_prod, ofReal_mul_pos_iff, ofReal_finsupp_sum, Submodule.smul_starProjection_singleton, ofReal_finsuppProd, norm_le_re_iff_eq_norm, ofReal_im, Matrix.IsHermitian.roots_charpoly_eq_eigenvalues, Matrix.IsHermitian.cfcAux_apply, ofReal_zero, exists_dual_vector, LinearMap.IsSymmetric.hasEigenvalue_eigenvalues, tendsto_ofReal_cobounded_cobounded, re_eq_add_conj, InnerProductSpace.gramSchmidtOrthonormalBasis_apply_of_orthogonal, LinearMap.IsSymmetric.coe_reApplyInnerSelf_apply, exists_dual_vector'', LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply, sqrt_of_nonneg, inner_product_apply_eigenvector, continuous_ofReal, exists_norm_mul_eq_self, ofReal_pow, InnerProductSpace.Core.inner_smul_ofReal_left, ofReal_alg, conj_eq_iff_real, Matrix.IsHermitian.det_eq_prod_eigenvalues, Matrix.IsHermitian.spectrum_eq_image_range, ContinuousLinearMap.extendTo𝕜_apply, Matrix.IsHermitian.spectral_theorem, coord_norm', ofReal_intCast, complexRingEquiv_symm_apply, ofReal_eq_zero, re_mul_ofReal, inner_self_ofReal_norm, exists_dual_vector', nonneg_iff_exists_ofReal, ofReal_expect, ofReal_nonpos, InnerProductSpace.gramSchmidt_def'', ofReal_one, inner_smul_real_left, ofReal_eq_re_of_isSelfAdjoint, Matrix.IsHermitian.coe_re_apply_self, ofReal_div, integral_coe_re_add_coe_im, LinearMap.IsSymmetric.apply_eigenvectorBasis, sqrt_neg_I, inner_eq_ofReal_norm_sq_left_iff, Function.RCLike.hasTemperateGrowth_ofReal, MeasureTheory.Integrable.ofReal, InnerProductSpace.Core.inner_self_ofReal_re, inv_def, sqrt_I, LinearMap.IsSymmetric.hasEigenvalue_iInf_of_finiteDimensional, re_eq_ofReal_of_isSelfAdjoint, MeasureTheory.L2.inner_indicatorConstLp_one_indicatorConstLp_one, CFC.quasispectrum_abs, CFC.spectrum_abs, ofReal_nnratCast, ofReal_pos, Polynomial.aeval_ofReal, IsSelfAdjoint.hasEigenvector_of_isMinOn, real_smul_ofReal, Matrix.IsHermitian.coe_re_diag, ofReal_real_eq_id, Matrix.IsHermitian.roots_charpoly_eq_eigenvalues₀, LinearMap.IsSymmetric.trace_eq_sum_eigenvalues, norm_coe_norm, ofReal_tsum, lipschitzWith_ofReal, ofReal_eq_complex_ofReal, ofReal_mul_neg_iff, re_ofReal_pow, IsSelfAdjoint.hasEigenvector_of_isLocalExtrOn, re_le_neg_norm_iff_eq_neg_norm, neg_iff_exists_ofReal, integral_ofReal, Matrix.IsHermitian.star_mul_self_mul_eq_diagonal, im_ofReal_mul, ContinuousLinearMap.extendTo𝕜'_apply, ContinuousLinearEquiv.coord_norm', LinearMap.IsSymmetric.exists_eigenvalues_eq, ofReal_ofNat, re_ofReal_mul, setIntegral_re_add_im, SchwartzMap.smulLeftCLM_ofReal, intervalIntegral_ofReal, IsSelfAdjoint.eq_smul_self_of_isLocalExtrOn, conj_eq_re_sub_im, InnerProductSpace.Core.re_inner_smul_ofReal_smul_self, Matrix.IsHermitian.charpoly_eq, tendsto_ofReal_atBot_cobounded, Matrix.IsHermitian.conjStarAlgAut_star_eigenvectorUnitary, integral_re_add_im, norm_le_im_iff_eq_I_mul_norm, real_smul_eq_coe_mul, ofReal_inv, ofRealAm_coe, re_eq_self_of_le, LinearMap.IsSymmetric.hasEigenvector_eigenvectorBasis, LinearMap.IsSymmetric.coe_re_inner_apply_self, InnerProductSpace.Core.ofReal_normSq_eq_inner_self, ofReal_sum, norm_of_nonneg', inner_eq_ofReal_norm_sq_right_iff, tendsto_ofReal_atTop_cobounded, MeasureTheory.MemLp.ofReal, ofReal_ratCast, norm_of_nonneg, ofReal_lt_ofReal, norm_inner_div_norm_mul_norm_eq_one_iff, ofReal_lt_zero
|
ofRealAm 📖 | CompOp | 4 mathmath: ofRealCLM_coe, Subalgebra.SeparatesPoints.rclike_to_real, ofRealAm_coe, restrict_toContinuousMap_eq_toContinuousMapStar_restrict
|
ofRealCLM 📖 | CompOp | 4 mathmath: map_from_real, ofRealCLM_apply, ofRealCLM_norm, ofRealCLM_coe
|
ofRealLI 📖 | CompOp | 1 mathmath: ofRealLI_apply
|
re 📖 | CompOp | 175 mathmath: conj_re, sqrt_eq_ite, one_re, map_apply, geometric_hahn_banach_point_open, reCLM_apply, div_re_ofReal, separate_convex_open_set, re_add_im, InnerProductSpace.Core.inner_mul_inner_self_le, Submodule.re_inner_starProjection_eq_normSq, LinearMap.IsPositive.re_inner_nonneg_right, re_sqrt_ofReal, pos_iff, ofReal_re, re_add_im_ax, is_real_TFAE, norm_sub_mul_self, Matrix.IsHermitian.eigenvalues_eq, ConvexOn.univ_sSup_of_countable_affine_eq, ofNat_re, nonpos_iff, smul_re, abs_re_le_norm, geometric_hahn_banach_closed_point, norm_sq_eq_def_ax, intCast_re, inner_mul_inner_self_le, mul_im_ax, InnerProductSpace.Core.norm_eq_sqrt_re_inner, abs_re_div_norm_le_one, norm_sub_sq, I_re_ax, re_nonneg_of_nonneg, LinearMap.IsSymmetric.coe_re_inner_self_apply, complexRingEquiv_apply, re_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two, re_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two, inner_re_zero_right, re_monotone, ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_left, LowerSemicontinuousOn.isClosed_re_epigraph, LinearMap.IsSymmetric.hasEigenvalue_iSup_of_finiteDimensional, inner_re_zero_left, inner_self_ofReal_re, div_im, ext_iff, re_eq_norm_of_mul_conj, conj_eq_iff_re, ConvexOn.sSup_of_countable_affine_eq, ofNat_mul_re, le_iff_re_im, ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_right, measurable_re, real_inner_eq_re_inner, add_conj, ofReal_re_ax, InnerProductSpace.Core.inner_self_eq_norm_mul_norm, geometric_hahn_banach_point_point, LinearMap.extendTo𝕜'_apply_re, re_to_real, neg_iff, sqrt_eq_real_add_ite, InnerProductSpaceable.inner_.norm_sq, ConvexOn.sSup_of_nat_affine_eq, natCast_re, InnerProductSpace.Core.inner_self_nonneg, inner_re_symm, norm_le_re_iff_eq_norm, nonneg_iff, continuous_re, zero_re, InnerProductSpace.Core.inner_re_symm, re_eq_add_conj, ContinuousLinearMap.reApplyInnerSelf_apply, inner_self_eq_norm_mul_norm, Matrix.IsHermitian.sort_roots_charpoly_eq_eigenvalues₀, LinearMap.re_inner_adjoint_mul_self_nonneg, MeasureTheory.Integrable.re_im_iff, ConvexOn.convex_re_epigraph, sqrt_of_nonneg, LinearMap.isPositive_iff_complex, inner_self_eq_norm_sq, lipschitzWith_re, Measurable.re, MeasureTheory.AEStronglyMeasurable.re, ContinuousLinearMap.IsPositive.re_inner_nonneg_left, ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_left, InnerProductSpace.norm_sq_eq_re_inner, hasSum_re, PreInnerProductSpace.Core.re_inner_nonneg, re_mul_ofReal, norm_re_le_norm, re_inner_self_pos, geometric_hahn_banach_open, InnerProductSpace.Core.inner_mul_symm_re_eq_norm, re_le_re, reLm_coe, MeasureTheory.MemLp.re, ratCast_re, ofReal_eq_re_of_isSelfAdjoint, Matrix.IsHermitian.coe_re_apply_self, MeasureTheory.Integrable.re, integral_coe_re_add_coe_im, lt_iff_re_im, ConvexOn.univ_sSup_affine_eq, norm_add_sq, norm_sq_re_conj_add, norm_add_mul_self, InnerProductSpace.Core.inner_self_ofReal_re, hasSum_iff, LinearMap.IsSymmetric.hasEigenvalue_iInf_of_finiteDimensional, re_eq_ofReal_of_isSelfAdjoint, Matrix.PosSemidef.re_dotProduct_nonneg, re_le_norm, ContinuousLinearMap.isPositive_iff_complex, norm_sq_eq_def, Matrix.IsHermitian.coe_re_diag, I_mul_re, conj_re_ax, inner_mul_symm_re_eq_norm, Submodule.re_inner_starProjection_nonneg, realRingEquiv_apply, mul_im, re_ofReal_pow, re_inner_self_nonpos, norm_sq_re_add_conj, InnerProductSpace.Core.cauchy_schwarz_aux', re_eq_complex_re, norm_to_complex, re_sq_le_normSq, mul_re, re_le_neg_norm_iff_eq_neg_norm, to_complex_nonneg_iff, inner_self_re_eq_norm, I_re, AEMeasurable.re, re_ofReal_mul, norm_add_pow_two, norm_eq_sqrt_re_inner, iInter_halfSpaces_eq, inner_self_nonneg, LinearMap.IsSymmetric.re_trace_eq_sum_eigenvalues, normSq_add, div_re, setIntegral_re_add_im, geometric_hahn_banach_compact_closed, geometric_hahn_banach_point_closed, re_inner_eq_norm_add_mul_self_sub_norm_sub_mul_self_div_four, norm_sub_pow_two, conj_eq_re_sub_im, InnerProductSpace.Core.re_inner_smul_ofReal_smul_self, integral_re, normSq_apply, ConvexOn.exists_affine_le_of_lt, ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_right, re_inner_le_norm, mul_re_ax, integral_re_add_im, re_to_complex, isCauSeq_re, ConvexOn.sSup_affine_eq, LinearMap.IsSymmetric.coe_re_inner_apply_self, geometric_hahn_banach_closed_compact, re_extendTo𝕜'ₗ, MeasureTheory.memLp_re_im_iff, normSq_sub, re_tsum, ContinuousLinearMap.IsPositive.re_inner_nonneg_right, ConvexOn.univ_sSup_of_nat_affine_eq, geometric_hahn_banach_open_open, inv_re, Matrix.PosDef.re_dotProduct_pos, LinearMap.IsPositive.re_inner_nonneg_left, geometric_hahn_banach_open_point
|
reCLM 📖 | CompOp | 4 mathmath: reCLM_apply, reCLM_norm, reCLM_coe, map_to_real
|
reLm 📖 | CompOp | 2 mathmath: reCLM_coe, reLm_coe
|
realLinearIsometryEquiv 📖 | CompOp | 2 mathmath: realLinearIsometryEquiv_symm_apply, realLinearIsometryEquiv_apply
|
realRingEquiv 📖 | CompOp | 4 mathmath: realRingEquiv_symm_apply, realLinearIsometryEquiv_symm_apply, realRingEquiv_apply, realLinearIsometryEquiv_apply
|
toDecidableEq 📖 | CompOp | 5 mathmath: LinearMap.IsSymmetric.directSum_decompose_apply, LinearMap.IsSymmetric.card_filter_eigenvalues_eq, LinearMap.IsSymmetric.directSum_isInternal_of_commute, LinearMap.IsSymmetric.direct_sum_isInternal, LinearMap.IsSymmetric.eigenvectorBasis_def
|
toDenselyNormedField 📖 | CompOp | 1751 mathmath: Matrix.l2_opNorm_toEuclideanCLM, OrthonormalBasis.singleton_repr, Pi.comul_eq_adjoint, instSeparatingDual, TensorProduct.mapInclIsometry_apply, ContinuousLinearMap.rayleigh_smul, InnerProductSpace.Core.inner_smul_right, conj_re, Submodule.starProjection_apply_eq_isComplProjection, WithLp.prod_inner_apply, sqrt_eq_ite, ContinuousAt.inner, Orthonormal.linearIndependent, im_le_neg_norm_iff_eq_neg_I_mul_norm, SchwartzMap.lineDerivOpCLM_eq, MeasureTheory.lpNorm_conj, AddChar.card_addChar_le, TensorProduct.enorm_lid, InnerProductSpace.Core.inner_add_left, Matrix.frobenius_nnnorm_mul, pos_iff_exists_ofReal, TensorProduct.inner_tmul, ContinuousLinearMap.isPositive_iff_eq_sum_rankOne, one_re, continuousOn_stereoToFun, InnerProductSpace.isPositive_rankOne_self, MeasureTheory.condExpL1_smul, Orthonormal.inner_left_finsupp, norm_cfcₙHom, map_apply, OrthonormalBasis.orthogonalProjection_eq_sum, LinearMap.IsSymmetric.inner_map_polarization, geometric_hahn_banach_point_open, ContinuousLinearMap.integral_compLp, tendsto_birkhoffAverage_apply_sub_birkhoffAverage', LinearMap.adjoint_adjoint, Affine.Simplex.orthogonalProjectionSpan_map, TensorProduct.ext_iff_inner_left, EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal, InnerProductSpace.toLinearIsometry_toDual, ofRealCLM_apply, normSq_to_real, IsometricContinuousFunctionalCalculus.isGreatest_nnnorm_spectrum, IsSelfAdjoint.commute_cfcHom, InnerProductSpace.span_gramSchmidtNormed, cfcₙ_norm_nonneg, hasFDerivAt_iff_hasGradientAt, reCLM_apply, cfcₙHom_apply_mem_elemental, IsHilbertSum.surjective_isometry, curveIntegral_smul, div_re_ofReal, ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric, Submodule.reflection_trans_reflection, inner_vsub_right_eq_zero_symm, separate_convex_open_set, Submodule.orthogonalDecomposition_symm_apply, OrthogonalFamily.linearIsometry_apply_single, ContinuousLinearMap.isStarProjection_iff_isSymmetricProjection, InnerProductSpace.rankOne_one_left_eq_innerSL, Submodule.IsOrtho.starProjection_comp_starProjection, LinearMap.IsSymmetric.restrictScalars, ClosedSubmodule.toSubmodule_orthogonal_eq, Convex.convex_isRCLikeNormedField, EuclideanSpace.orthonormal_single, Matrix.posSemidef_iff_eq_conjTranspose_mul_self, ofRealLI_apply, LinearMap.IsPositive.ne_zero_iff, ContinuousLinearMapWOT.le_nhds_iff_forall_inner_apply_le_nhds, curveIntegrable_segment, LinearMap.isPositive_adjoint_comp_self, Submodule.toLinearEquiv_orthogonalDecomposition_symm, OrthonormalBasis.repr_injective, LinearMap.IsSymmetric.isFinitelySemisimple, re_add_im, InnerProductSpace.Core.inner_mul_inner_self_le, ContinuousLinearMap.IsPositive.inner_left_eq_inner_right, Matrix.spectrum_toEuclideanLin, MeasureTheory.norm_condExpL2_le, InnerProductSpace.isIdempotentElem_rankOne_self, Matrix.cstar_nnnorm_def, lp.inner_eq_tsum, ContinuousLinearMap.continuous_integral_comp_L1, ContinuousLinearMapWOT.tendsto_iff_forall_inner_apply_tendsto, star_def, OrthonormalBasis.sum_inner_mul_inner, Matrix.l2_opNorm_mulVec, Submodule.re_inner_starProjection_eq_normSq, conjCLE_norm, ordinaryHypergeometric_radius_top_of_neg_nat₃, inner_self_eq_one_of_norm_eq_one, MeasureTheory.inner_condExpL2_left_eq_right, algebraMap_eq_ofReal, Submodule.reflection_orthogonal_apply, SchwartzMap.integral_clm_comp_lineDerivOp_right_eq_neg_left, inner_apply', MeasureTheory.MemLp.const_inner, MeasureTheory.integral_fintype_prod_volume_eq_pow, LinearMap.IsSymmetric.diagonalization_apply_self_apply, EuclideanGeometry.orthogonalProjection_congr, LinearMap.IsPositive.re_inner_nonneg_right, flip_innerSL_real, Matrix.le_iff, Orientation.volumeForm_robust_neg, Submodule.starProjection_orthogonal', norm_I_of_ne_zero, LinearMap.IsSymmetric.im_inner_self_apply, ContinuousLinearMap.IsPositive.toLinearMap, Submodule.toLinearEquiv_orthogonalDecomposition, sub_conj, OrthonormalBasis.toBasis_tensorProduct, re_sqrt_ofReal, TensorProduct.congrIsometry_refl_refl, norm_smul_inv_norm', MeasureTheory.condExpL2_ae_eq_zero_of_ae_eq_zero, pos_iff, MeasureTheory.isTightMeasureSet_iff_inner_tendsto, AddChar.wInner_cWeight_self, TensorProduct.enorm_comm, innerSL_apply_apply, Submodule.isOrtho_sup_right, HasGradientAt.continuousOn, CFC.abs_eq_cfcₙ_coe_norm, LinearIsometry.rTensor_def, LinearMap.adjoint_innerₛₗ_apply, inner_sum, EuclideanSpace.inner_single_left, EuclideanSpace.basisFun_toBasis, Unitary.conjStarAlgEquiv_unitaryLinearIsometryEquiv, inner_eq_norm_mul_iff, map_same_eq_id, LinearMap.adjoint_eq_toCLM_adjoint, ClosedSubmodule.orthogonal_gc, LinearMap.isPositive_id, Submodule.orthogonalProjection_mem_subspace_eq_self, EuclideanSpace.norm_sq_eq, ContinuousLinearMap.IsPositive.inner_nonneg_right, wInner_sub_right, GaussianFourier.integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace, InnerProductSpace.span_gramSchmidtNormed_range, Submodule.orthogonal_disjoint, LinearMap.isSelfAdjoint_toContinuousLinearMap_iff, Submodule.starProjection_add_starProjection_orthogonal, Matrix.spectrum_toLpLin, OrthonormalBasis.orthogonalProjection_eq_sum_rankOne, Submodule.mem_orthogonal_singleton_iff_inner_right, InnerProductSpace.Core.inner_smul_left, ContinuousMap.setOfIdeal_ofSet_eq_interior, InnerProductSpace.toDual_symm_apply, MeasureTheory.integral_fintype_prod_eq_prod, IsHilbertSum.linearIsometryEquiv_symm_apply, Submodule.starProjection_singleton, conj_nat_cast, EuclideanSpace.basisFun_apply, EuclideanGeometry.reflection_symm, Submodule.isOrtho_iff_inner_eq, EuclideanGeometry.orthogonalProjection_contLinear, curveIntegralFun_smul, ClosedSubmodule.mem_orthogonal', ofReal_re, MeasureTheory.charFun_toDual_symm_eq_charFunDual, EuclideanGeometry.dist_orthogonalProjection_eq_iff_oangle_eq, OrthogonalFamily.orthonormal_sigma_orthonormal, re_add_im_ax, PreInnerProductSpace.Core.smul_left, Differentiable.fderiv_norm_rpow, normSq_neg, curveIntegrable_fun_neg_iff, toStarOrderedRing, Submodule.reflection_symm, MeasureTheory.integral_const_mul, OrthonormalBasis.det_eq_neg_det_of_opposite_orientation, LinearMap.IsSymmetric.orthogonalFamily_eigenspaces, TensorProduct.ext_iff_inner_right_threefold', CurveIntegrable.zero, is_real_TFAE, OrthonormalBasis.det_to_matrix_orthonormalBasis_of_opposite_orientation, curveIntegrable_smul_iff, TensorProduct.toLinearEquiv_lidIsometry, OrthonormalBasis.toBasis_singleton, ContDiffOn.inner, EuclideanGeometry.reflection_map, ContinuousLinearMap.adjoint_id, InnerProductSpace.smul_left, ClosedSubmodule.inf_orthogonal, ContinuousLinearMap.isPositive_natCast, tendsto_birkhoffAverage_apply_sub_birkhoffAverage, abs_im_div_norm_le_one, norm_sub_mul_self, ContinuousLinearMap.isStarNormal_iff_norm_eq_adjoint, Submodule.starProjection_comp_starProjection_eq_zero_iff, SchwartzMap.laplacianCLM_eq, LinearIsometryEquiv.conjStarAlgEquiv_apply, LinearMap.toMatrixOrthonormal_reindex, MeasureTheory.integral_div, Filter.tendsto_ofReal_iff', inner_smul_left_eq_star_smul, mul_conj, norm_conj, borelSpace, im_inner_eq_norm_sub_i_smul_mul_self_sub_norm_add_i_smul_mul_self_div_four, LinearMap.IsSymmetricProjection.ext_iff, ConvexOn.univ_sSup_of_countable_affine_eq, hasSum_ofReal, InnerProductSpace.inner_left_rankOne_apply, continuous_normSq, ClosedSubmodule.orthogonal_injective, SchwartzMap.fderivCLM_apply, Submodule.norm_starProjection_apply_le, ContinuousLinearMap.norm_extendTo𝕜, HasFDerivAt.norm_sq, LinearIsometry.map_starProjection', ofNat_re, polynomialFunctions.starClosure_topologicalClosure, innerₛₗ_apply_apply, OrthonormalBasis.repr_self, ofReal_balance, Submodule.symmetric_isOrtho, OrthogonalFamily.norm_sq_diff_sum, norm_smul_inv_norm, ContinuousLinearMap.eq_adjoint_iff, MeasureTheory.L2.inner_def, nonpos_iff, smul_re, nonpos_iff_exists_ofReal, wInner_of_isEmpty, LinearMap.IsSymmetric.directSum_decompose_apply, InnerProductSpace.rankOne_apply, EuclideanSpace.nndist_eq, Unitary.coe_linearIsometryEquiv_apply, OrthonormalBasis.toBasis_adjustToOrientation, Submodule.reflection_singleton_apply, SchwartzMap.compCLMOfContinuousLinearEquiv_apply, intervalIntegral.integral_div, EuclideanGeometry.inter_eq_singleton_orthogonalProjection, isClosed_setOf_tendsto_birkhoffAverage, OrthonormalBasis.measurePreserving_repr, Submodule.reflection_apply, ofReal_comp_balance, abs_re_le_norm, curveIntegralFun_segment, reCLM_norm, geometric_hahn_banach_closed_point, MeasureTheory.AEStronglyMeasurable.inner_const, Submodule.orthogonal_eq_bot_iff, TensorProduct.adjoint_map, curveIntegral_neg, AEMeasurable.im, HasGradientAt.continuousAt, LinearIsometryEquiv.lTensor_apply, InnerProductSpace.gramSchmidt_def, ContinuousLinearMap.isPositive_self_comp_adjoint, ofReal_sub, LinearMap.adjoint_toContinuousLinearMap, Affine.Simplex.orthogonalProjectionSpan_eq_point, Unitary.linearIsometryEquiv_coe_apply, norm_sq_eq_def_ax, MeasureTheory.MemLp.condExpL2_ae_eq_condExp, ContinuousLinearMap.toSesqForm_apply_coe, LinearIsometryEquiv.adjoint_eq_symm, TensorProduct.mapIsometry_id_id, ordinaryHypergeometricSeries_radius_eq_one, MeasureTheory.setIntegral_prod_mul, Matrix.toEuclideanLin_apply, inner_self_eq_norm_sq_to_K, IsContDiffImplicitAt.hasFDerivAt, Submodule.IsOrtho.orthogonalProjection_comp_subtypeL, LinearMap.IsPositive.isPositive_smul_iff, intCast_re, LinearIsometryEquiv.trans_smul, MeasureTheory.charFunDual_eq_charFun_map_one, EuclideanGeometry.orthogonalProjection_map, im_eq_zero_iff_isSelfAdjoint, IsHilbertSum.hasSum_linearIsometryEquiv_symm, Submodule.IsOrtho.map_iff, MeasureTheory.integral_fintype_prod_eq_pow, norm_ofReal, inner_mul_inner_self_le, InnerProductSpace.Core.inner_smul_ofReal_right, conjCLE_apply, EuclideanSpace.norm_single, mul_im_ax, Orthonormal.inner_left_fintype, InnerProductSpace.Core.norm_eq_sqrt_re_inner, wInner_cWeight_eq_expect, Submodule.coe_orthogonalDecomposition_symm, MeasureTheory.aestronglyMeasurable_condExpL2, I_mul_I, Submodule.orthogonalProjection_bot, ContinuousLinearMap.adjointAux_norm, toIsStrictOrderedModule, abs_re_div_norm_le_one, Submodule.range_starProjection, norm_sub_sq, toIsStrictOrderedRing, LinearIsometryEquiv.inner_map_eq_flip, EuclideanGeometry.angle_orthogonalProjection_self, binomialSeries_radius_eq_one, Pi.counit_eq_adjoint, ProbabilityTheory.covarianceBilin_apply_basisFun_self, LinearMap.toMatrixOrthonormal_apply_apply, I_re_ax, MeasureTheory.charFun_apply_real, instCStarRing, Submodule.exists_add_mem_mem_orthogonal, GaussianFourier.integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace, HasGradientWithinAt.continuousWithinAt, InnerProductSpace.Core.inner_neg_left, LinearMap.IsSymmetric.coe_re_inner_self_apply, AddChar.wInner_cWeight_eq_zero_iff_ne, hasStrictDerivAt_exp_smul_const, ofReal_nonneg, ContinuousMap.setOfIdeal_ofSet_of_isOpen, EuclideanGeometry.dist_orthogonalProjection_eq_iff_angle_eq, SchwartzMap.smulLeftCLM_compCLMOfContinuousLinearEquiv, Module.Basis.mulOpposite_is_orthonormal_iff, EuclideanSpace.instFactEqNatFinrankFin, differentiable_euclidean, Finsupp.sum_inner, MeasureTheory.integral_fin_nat_prod_volume_eq_prod, MeasureTheory.condExpL2_indicator_ae_eq_smul, ClosedSubmodule.orthogonal_closure'', contDiffWithinAt_euclidean, hasStrictDerivAt_exp_smul_const', Real.fourier_iteratedFDeriv, re_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two, LinearIsometryEquiv.adjoint_toLinearMap_eq_symm, InnerProductSpace.toDualMap_apply_apply, Submodule.le_orthogonal_orthogonal, LinearMap.eq_adjoint_iff_basis_left, LinearMap.IsSymmetricProjection.isIdempotentElem, EuclideanSpace.volume_closedBall_fin_three, re_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two, LinearMap.extendTo𝕜'_apply, curveIntegral_fun_smul, NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis_map_eq, Submodule.instHasOrthogonalProjectionOfCompleteSpace, MeasureTheory.MemLp.inner_const, OrthogonalFamily.linearIsometry_apply_dfinsupp_sum_single, curveIntegral_fun_zero, LinearMap.nonneg_iff_isPositive, coe_innerSL_apply, inner_eq_zero_of_right, LinearMap.IsSymmetric.inner_map_self_eq_zero, OrthonormalBasis.prod_apply, inner_re_zero_right, MeasureTheory.integral_condExpL2_eq, integral_smul_const, range_cfcₙHom, toPosMulReflectLT, TensorProduct.lidIsometry_apply, MeasureTheory.StronglyMeasurable.inner, Orientation.volumeForm_def, EuclideanSpace.dist_single_same, LinearMap.IsPositive.inner_nonneg_left, hasGradientAtFilter_iff_isLittleO, ContinuousLinearMap.instCStarRingId, NormedSpace.eq_zero_iff_forall_dual_eq_zero, hasGradientAt_iff_isLittleO, MeasureTheory.setIntegral_condExpL2_indicator, InnerProductSpace.nnnorm_rankOne, PreInnerProductSpace.Core.conj_inner_symm, stereographic_apply_neg, OrthonormalBasis.orthogonalProjection_apply_eq_sum, InnerProductSpace.Core.norm_inner_symm, HasGradientWithinAt.differentiableWithinAt, ContinuousLinearMap.setIntegral_compLp, LinearMap.trace_eq_sum_inner, Matrix.gram_zero, InnerProductSpace.isSymmetricProjection_rankOne_self, ProbabilityTheory.complexMGF_mul_I, norm_ofNat, hasGradientWithinAt_iff_hasFDerivWithinAt, norm_inner_eq_norm_iff, re_monotone, ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_left, im_ofReal_pow, LinearIsometryEquiv.smul_apply, inner_eq_norm_mul_iff_div, Submodule.topologicalClosure_eq_self, FiniteDimensional.RCLike.properSpace_submodule, range_stereographic_symm, FiniteDimensional.rclike_to_real, WeakDual.CharacterSpace.continuousMapEval_bijective, PiLp.volume_preserving_toLp, LowerSemicontinuousOn.isClosed_re_epigraph, EuclideanGeometry.orthogonalProjection_apply', isOpenEmbedding_stereographic_symm, LinearMap.IsSymmetric.hasEigenvalue_iSup_of_finiteDimensional, Polynomial.ofReal_eval, wInner_neg_right, MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le, inner_self_im, ofReal_natCast, Matrix.PosSemidef.posSemidef_sqrt, unitary.linearIsometryEquiv_coe_symm_apply, ContinuousLinearMap.isPositive_def, LinearMap.IsSymmetric.hasStrictFDerivAt_reApplyInnerSelf, SchwartzMap.toBoundedContinuousFunctionCLM_apply, conj_ofReal, curveIntegral_segment, OrthonormalBasis.coe_ofRepr, Submodule.starProjection_top', EuclideanGeometry.Sphere.isTangent_iff_isTangentAt_orthogonalProjection, OrthonormalBasis.toBasis_mulOpposite, Submodule.adjoint_subtypeL, hasStrictFDerivAt_exp, inner_re_zero_left, IsCoercive.range_eq_top, EuclideanSpace.nnnorm_single, LinearMap.isSymmetric_adjoint_mul_self, InnerProductSpace.Core.cauchy_schwarz_aux, inner_self_ofReal_re, conjLIE_apply, Submodule.reflection_orthogonalComplement_singleton_eq_neg, summable_ofReal, Complex.orthonormalBasisOneI_repr_apply, conj_mul, Affine.Triangle.dist_circumcenter_reflection_orthocenter, MeasureTheory.norm_condExpL2_coe_le, MeasureTheory.setLIntegral_nnnorm_condExpL2_indicator_le, MeasureTheory.mem_lpMeas_iff_aestronglyMeasurable, InnerProductSpace.trace_rankOne, imLm_coe, NormedSpace.eq_iff_forall_dual_eq, ContinuousLinearEquiv.integral_comp_comm, Submodule.isIdempotentElem_starProjection, div_im, hasFDerivAt_norm_rpow, dist_birkhoffAverage_apply_birkhoffAverage, LinearIsometry.inner_map_map, Matrix.eigenvalues_conjTranspose_mul_self_nonneg, sum_inner, ofReal_mul, im_to_real, instContinuousMapUniqueHom, ContinuousLinearMap.IsPositive.conj_adjoint, Matrix.toEuclideanCLM_toLp, WeakDual.CharacterSpace.homeoEval_naturality, InnerProductSpace.Core.inner_neg_right, ContinuousLinearMap.isPositive_id, conjCLE_coe, contDiffOn_stereoToFun, ext_iff, Unitary.coe_symm_linearIsometryEquiv_apply, hasStrictFDerivAt_exp_smul_const', range_cfcₙ, LinearMap.adjoint_rTensor, hasGradientAt_iff_isLittleO_nhds_zero, normSq_inv, LinearMap.IsPositive.add, HilbertBasis.hasSum_orthogonalProjection, LinearMap.adjoint_inner_right, MeasureTheory.mem_lpMeas_indicatorConstLp, InnerProductSpace.adjoint_rankOne, stereoInvFun_apply, InnerProductSpace.rankOne_eq_zero, mul_wInner_left, TensorProduct.ext_iff_inner_left_threefold', Convex.toWeakSpace_closure, Submodule.isOrtho_sSup_right, LinearIsometry.lTensor_apply, ClosedSubmodule.bot_orthogonal_eq_top, Submodule.norm_sq_eq_add_norm_sq_starProjection, re_eq_norm_of_mul_conj, InnerProductSpace.inner_right_rankOne_apply, HilbertBasis.hasSum_repr, innerSL_inj, MeasureTheory.condExpIndSMul_smul, TensorProduct.ext_iff_inner_left_threefold, MeasureTheory.lintegral_nnnorm_condExpL2_le, conj_eq_iff_re, StrongDual.toLp_of_not_memLp, AffineSubspace.signedInfDist_eq_signedDist_of_mem, LinearMap.IsSymmetric.coe_toSelfAdjoint, TensorProduct.inner_lid_lid, EuclideanSpace.volume_closedBall_fin_two, OrthonormalBasis.toBasis_map, Matrix.piLp_ofLp_toEuclideanLin, LinearMap.IsSymmetric.diagonalization_symm_apply, maximal_orthonormal_iff_basis_of_finiteDimensional, TensorProduct.norm_comm, rank_le_two, curveIntegral_segment_const, instMulPosReflectLE, ContinuousLinearMap.isPositive_toLinearMap_iff, Affine.Simplex.signedInfDist_apply_self, ConvexOn.sSup_of_countable_affine_eq, reCLM_coe, InnerProductSpace.rankOne_eq_rankOne_iff_comm, InnerProductSpace.toDual_apply, ofNat_mul_re, OrthonormalBasis.tensorProduct_repr_tmul_apply', HasDerivWithinAt.inner, DifferentiableAt.inner, NormedSpace.exp_continuousMap_eq, InnerProductSpace.Core.inner_im_symm, OrthonormalBasis.sum_sq_norm_inner_right, LinearIsometryEquiv.reflections_generate, AffineSubspace.signedInfDist_eq_signedDist_orthogonalProjection, Submodule.map_orthogonal_equiv, isUniformEmbedding_ofReal, Matrix.l2_opNNNorm_mulVec, Orthonormal.inner_left_right_finset, SchwartzMap.lineDerivOp_compCLMOfContinuousLinearEquiv, ClosedSubmodule.top_orthogonal_eq_bot, EuclideanGeometry.reflection_reflection, Submodule.norm_orthogonalProjection_apply_le, Finsupp.inner_sum, conj_I_ax, nnnorm_nnratCast, HasFDerivWithinAt.inner, TensorProduct.norm_assoc, TensorProduct.nnnorm_tmul, InnerProductSpace.comp_rankOne, OrthonormalBasis.starProjection_eq_sum_rankOne, I_eq_zero_or_im_I_eq_one, InnerProductSpace.toDualMap_apply, normSq_nonneg, Orthonormal.inner_products_summable, InnerProductSpace.gramSchmidt_orthogonal, ContinuousLinearMap.adjoint_inner_left, TensorProduct.inner_mapIncl_mapIncl, InnerProductSpace.gramSchmidt_pairwise_orthogonal, le_iff_re_im, InnerProductSpace.AlgebraOfCoalgebra.mul_def, Matrix.l2_opNorm_diagonal, LinearMap.extendTo𝕜_apply, Matrix.l2_opNorm_conjTranspose_mul_self, ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_right, Affine.Simplex.mongePlane_def, ProbabilityTheory.complexMGF_id_mul_I, inner_neg_right, ContinuousLinearMap.IsPositive.isSymmetric, OrthonormalBasis.singleton_apply, OrthonormalBasis.equiv_apply, uniqueNonUnitalContinuousFunctionalCalculus, sqrt_one, inner_eq_sum_norm_sq_div_four, MeasureTheory.lpMeasToLpTrimLie_symm_indicator, LinearIsometryEquiv.conjStarAlgEquiv_trans, LinearMap.IsSymmetric.continuous, ContinuousMap.ideal_isMaximal_iff, integral_conj, LinearIsometry.extend_apply, InnerProductSpace.rank_rankOne, LinearMap.isSymmetric_sum, Submodule.isOrtho_top_left, IsometricContinuousFunctionalCalculus.toNonUnital, InnerProductSpace.toDual_apply_apply, exists_norm_eq_mul_self, Affine.Simplex.vectorSpan_isOrtho_altitude_direction, ContinuousLinearMap.adjointAux_apply, ContinuousLinearMap.nonneg_iff_isPositive, real_smul_eq_coe_smul, ContinuousLinearMap.inner_map_map_iff_adjoint_comp_self, measurable_re, Submodule.linearEquiv_det_reflection, LinearMap.isSymmetric_linearIsometryEquiv_conj_iff, ProperCone.innerDual_singleton, real_inner_eq_re_inner, nnnorm_ofNat, add_conj, Submodule.IsOrtho.map, EuclideanGeometry.reflection_eq_self_iff, ofReal_re_ax, differentiable_inner, InnerProductSpace.Core.inner_self_eq_norm_mul_norm, CFC.exp_eq_normedSpace_exp, im_eq_conj_sub, Submodule.toLinearMap_starProjection_eq_isComplProjection, InnerProductSpace.rankOne_def, TensorProduct.nnnorm_map, InnerProductSpace.Core.inner_self_eq_zero, conj_im_ax, stereoToFun_apply, ContinuousLinearMap.adjointAux_inner_left, SchwartzMap.convolution_apply, Submodule.sub_starProjection_mem_orthogonal, inner_self_conj, dist_birkhoffAverage_birkhoffAverage, LinearIsometryEquiv.conjStarAlgEquiv_ext_iff, OrthonormalBasis.repr_apply_apply, ContinuousLinearMap.IsStarNormal.ker_adjoint_eq_ker, Matrix.l2_opNNNorm_conjTranspose, ofReal_add, ClosedSubmodule.orthogonal_eq_inter, MeasureTheory.L2.integral_inner_eq_sq_eLpNorm, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed, SchwartzMap.compCLMOfAntilipschitz_apply, SchwartzMap.fourierInv_apply_eq, LinearIsometryEquiv.conjStarAlgEquiv_refl, CurveIntegrable.fun_zero, MeasureTheory.L2.inner_indicatorConstLp_one, ofReal_neg, MeasureTheory.L2.inner_indicatorConstLp_indicatorConstLp, LinearMap.IsSymmetric.toSelfAdjoint_apply, conj_div, EuclideanSpace.edist_single_same, EuclideanGeometry.orthogonalProjection_subtype, ofReal_zpow, im_mul_ofReal, Submodule.coe_orthogonalDecomposition, EuclideanGeometry.two_zsmul_oangle_self_orthogonalProjection, Submodule.finrank_orthogonal_span_singleton, Matrix.nonneg_iff_posSemidef, summable_conj, geometric_hahn_banach_point_point, wInner_zero_right, LinearMap.isPositive_natCast, inner_smul_real_right, TensorProduct.toLinearEquiv_congrIsometry, hasFDerivAt_exp_smul_const', Submodule.isOrtho_iSup_left, IsCoercive.bounded_below, Commute.cfcₙHom, Submodule.mem_orthogonal', LinearMap.toMatrixOrthonormal_symm_apply, ContinuousLinearMap.IsStarNormal.orthogonal_range, IsContDiffImplicitAt.implicitFunction_apply, Matrix.posDef_gram_iff_linearIndependent, wInner_sub_left, LinearMap.toMatrix_innerₛₗ_apply, Matrix.permMatrix_l2_opNorm_le, ContinuousLinearMap.IsStarNormal.adjoint_apply_eq_zero_iff, TensorProduct.toLinearEquiv_commIsometry, wInner_one_eq_inner, IsRCLikeNormedField.out, Matrix.eigenvalues_self_mul_conjTranspose_nonneg, Submodule.norm_sq_eq_add_norm_sq_projection, LinearMap.extendTo𝕜'_apply_re, inner_zero_left, re_to_real, Submodule.orthogonal_gc, neg_iff, curveIntegral_restrictScalars, Submodule.starProjection_isSymmetric, sqrt_eq_real_add_ite, Submodule.starProjection_apply, Submodule.HasOrthogonalProjection.map_linearIsometryEquiv', inv_im, Matrix.l2_opNorm_conjTranspose, ContinuousLinearMap.rayleighQuotient_add, Matrix.instNonnegSpectrumClass, LinearMap.isSelfAdjoint_iff', ofReal_prod, contDiffAt_euclidean, innerSLFlip_apply_apply, ofReal_mul_pos_iff, Affine.Triangle.dist_orthocenter_reflection_circumcenter, OrthogonalFamily.hasSum_linearIsometry, ofReal_finsupp_sum, finrank_euclideanSpace, EuclideanGeometry.oangle_orthogonalProjection_self, LinearMap.IsPositive.isSelfAdjoint, InnerProductSpaceable.inner_.norm_sq, Submodule.top_orthogonal_eq_bot, ConvexOn.sSup_of_nat_affine_eq, Submodule.fst_orthogonalDecomposition_apply, IsContDiffImplicitAt.implicitFunctionData_pt, HilbertBasis.dense_span, inner_add_left, Submodule.orthogonal_orthogonal_eq_closure, Submodule.smul_starProjection_singleton, one_im, toZeroLEOneClass, with_gaugeSeminormFamily, TensorProduct.ext_iff_inner_right, natCast_re, LinearEquiv.isPositive_symm_iff, InnerProductSpace.enorm_rankOne, InnerProductSpace.Core.inner_self_nonneg, Orthonormal.inner_finsupp_eq_sum_right, ofReal_finsuppProd, InnerProductSpace.continuousLinearMapOfBilin_zero, inner_re_symm, ContinuousLinearMap.toLinearMap_innerSL_apply, Submodule.orthogonalFamily_self, NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_norm_quasispectrum, LinearMap.IsSymmetric.adjoint_eq, LinearMap.isPositive_sum, Submodule.starProjection_norm_le, contDiffOn_euclidean, HasGradientAt.hasFDerivAt, norm_le_re_iff_eq_norm, AffineSubspace.abs_signedInfDist_eq_dist_of_mem_affineSpan_insert, PiLp.volume_preserving_ofLp, Real.fourier_fderiv, MeasureTheory.AEStronglyMeasurable.inner, Submodule.inner_orthogonalProjection_eq_of_mem_right, Submodule.reflection_reflection, ContinuousMap.adjoin_id_eq_span_one_union, SchwartzMap.instLineDerivSMul, Submodule.isOrtho_iff_le, MeasureTheory.condExp_smul, HasFDerivWithinAt.norm_sq, CFC.abs_algebraMap, ordinaryHypergeometric_radius_top_of_neg_nat₂, ClosedSubmodule.iInf_orthogonal, Matrix.isHermitian_gram, integral_inner, ofReal_im, LinearMap.IsSymmetric.isSymmetric_smul_iff, Matrix.isStrictlyPositive_iff_posDef, LinearMap.isPositive_linearIsometryEquiv_conj_iff, OrthonormalBasis.equiv_self_rfl, abs_im_le_norm, finrank_le_two, InnerProductSpace.coe_gramSchmidtBasis, MeasureTheory.integral_charFun_Icc, Submodule.reflection_inv, toCompleteSpace, nonneg_iff, Affine.Simplex.orthogonalProjection_circumcenter, ofReal_zero, Matrix.ofLp_toEuclideanCLM, summable_pow_div_add, Submodule.norm_starProjection, ClosedSubmodule.sup_orthogonal, LinearMap.IsSymmetric.orthogonalFamily_eigenspaces', hasDerivAt_exp_smul_const, continuous_re, Unitary.linearIsometryEquiv_coe_symm_apply, exists_dual_vector, ContinuousLinearMap.rayleighQuotient_le_norm, OrthonormalBasis.det_to_matrix_orthonormalBasis, instContinuousStar, LinearMap.isPositive_toContinuousLinearMap_iff, OrthogonalFamily.summable_of_lp, AddChar.wInner_cWeight_eq_one_iff_eq, ProbabilityTheory.covarianceBilin_eq_covarianceBilinDual, Affine.Simplex.exists_forall_dist_eq_iff_exists_excenterExists_and_eq_excenter, norm_inner_eq_norm_tfae, curveIntegral_fun_add, Submodule.isCompl_orthogonal_of_hasOrthogonalProjection, Submodule.reflection_mul_reflection, curveIntegral_fun_neg, zero_re, inner_tmul_eq, Matrix.instFiniteElemRealSpectrum, InnerProductSpace.Core.inner_re_symm, InnerProductSpace.gramSchmidt_triangular, Submodule.starProjection_map_apply, smul_im, LinearMap.star_eq_adjoint, Matrix.l2_opNNNorm_mul, tendsto_ofReal_cobounded_cobounded, differentiableWithinAt_euclidean, InnerProductSpace.Core.toNormedSpaceCore, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot', MeasureTheory.integral_prod_mul, Affine.Simplex.orthogonalProjection_eq_circumcenter_of_exists_dist_eq, LinearPMap.adjointDomainMkCLM_apply, Matrix.isPositive_toEuclideanLin_iff, TensorProduct.enorm_tmul, Polynomial.aeval_conj, Submodule.starProjection_bot, re_eq_add_conj, ContDiff.inner, HasGradientAt.differentiableAt, Submodule.orthogonal_closure, LinearMap.IsSymmetric.orthogonalFamily_eigenspace_inf_eigenspace, TensorProduct.inner_assoc_assoc, InnerProductSpace.Core.norm_inner_le_norm, ContinuousLinearMap.reApplyInnerSelf_apply, Affine.Simplex.direction_mongePlane, wInner_const_left, wInner_cWeight_const_left, LinearMap.le_def, MeasureTheory.integral_condExpL2_eq_of_fin_meas_real, EuclideanSpace.toLp_single, inner_self_eq_norm_mul_norm, hasStrictFDerivAt_norm_sq, Submodule.starProjection_unit_singleton, LinearMap.adjoint_toSpanSingleton, OrthonormalBasis.coe_toBasis, Submodule.reflection_sub, inner_apply, LinearMap.IsSymmetric.natCast, ClosedSubmodule.mem_orthogonal, Matrix.posDef_iff_eq_conjTranspose_mul_self, MeasureTheory.condExpIndL1_smul', LinearMap.re_inner_adjoint_mul_self_nonneg, InnerProductSpace.nullSubmodule_le_ker_toDualMap_left, MeasureTheory.Integrable.re_im_iff, normSq_mul, LinearMap.isPositive_self_comp_adjoint, hasSum_conj, circleIntegral.integral_smul, orthonormal_subtype_iff_ite, ContinuousLinearMap.instStarModuleId, EuclideanGeometry.orthogonalProjection_affineSpan_singleton, LinearIsometryEquiv.toLinearEquiv_lTensor, exists_dual_vector'', norm_wInner_le, LinearIsometryEquiv.toLinearEquiv_smul, curveIntegralFun_neg, binomialSeries_radius_eq_top_of_nat, Matrix.l2_opNNNorm_def, HasGradientAtFilter.isBigO_sub, ContinuousLinearMap.adjointAux_adjointAux, Measurable.im, Submodule.coe_inner, hasDerivAt_exp, Submodule.orthogonalProjection_apply_eq_linearProjOfIsCompl, norm_im_le_norm, UniformSpace.Completion.Continuous.inner, MeasureTheory.condExpL2_indicator_of_measurable, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot, inner_zero_right, LinearMap.eq_adjoint_iff, inner_self_eq_zero, MeasureTheory.AEStronglyMeasurable.const_inner, Orthonormal.inner_right_finsupp, ConvexOn.convex_re_epigraph, LinearMap.norm_extendTo𝕜'_apply_sq, OrthonormalBasis.tensorProduct_apply', EuclideanSpace.basisFun_repr, ContinuousLinearMap.integral_comp_id_comm', SchwartzMap.integral_pow_mul_iteratedFDeriv_le, OrthonormalBasis.sum_sq_norm_inner_left, LinearMap.isPositive_iff_complex, inner_self_eq_norm_sq, ContinuousLinearMap.isSelfAdjoint_iff', Submodule.sndL_comp_coe_orthogonalDecomposition, OrthonormalBasis.equiv_apply_euclideanSpace, continuous_ofReal, exists_norm_mul_eq_self, stereographic_neg_apply, isSelfAdjoint_starProjection, InnerProductSpace.gramSchmidt_def', MeasureTheory.condExpL2_indicator_eq_toSpanSingleton_comp, lipschitzWith_re, Measurable.re, ofReal_pow, OrthonormalBasis.det_adjustToOrientation, InnerProductSpace.Core.inner_smul_ofReal_left, Complex.orthonormalBasisOneI_repr_symm_apply, LocallyConvexSpace.toPolynormableSpace, curveIntegralFun_fun_zero, ofReal_alg, IsContDiffImplicitAt.implicitFunctionData_rightFun_apply, Submodule.sInf_orthogonal, OrthonormalBasis.inner_eq_zero, curveIntegralFun_def', MeasureTheory.instCompleteSpaceSubtypeAEEqFunMemAddSubgroupLpSubmoduleLpMeasOfFactLeMeasurableSpace, Submodule.isOrtho_span, ContinuousLinearMap.norm_extendTo𝕜'_bound, MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le_real, conj_tsum, inner_add_add_self, I_im, ContinuousLinearMap.le_def, hasGradientAt_iff_tendsto, InnerProductSpace.Core.inner_sub_sub_self, LinearMap.isPositive_zero, ContinuousLinearMap.IsPositive.re_inner_nonneg_left, MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_integral_rclike_tendsto, inner_add_right, LinearIsometry.orthonormal_comp_iff, continuous_inner, sqrt_neg_one, nnnorm_inner_le_nnnorm, NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_nnnorm_quasispectrum, Matrix.coe_toEuclideanCLM_eq_toEuclideanLin, InnerProductSpace.Core.inner_zero_right, wInner_const_right, InnerProductSpace.rankOne_def', EuclideanGeometry.eq_or_eq_reflection_of_dist_eq, Submodule.isClosed_orthogonal, EuclideanSpace.norm_eq, ContinuousLinearMap.IsPositive.inner_nonneg_left, ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_left, HasFDerivAt.inner, MeasureTheory.L2.eLpNorm_inner_lt_top, LinearMap.adjoint_lTensor, conj_eq_iff_real, norm_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul, OrthonormalBasis.map_apply, ofNat_mul_im, LinearMap.toMatrixOrthonormal_apply, MeasureTheory.condExpL1CLM_lpMeas, Submodule.isSymmetricProjection_starProjection, OrthogonalFamily.inner_sum, ClosedSubmodule.mem_orthogonal_toSubmodule_iff, EuclideanSpace.inner_eq_star_dotProduct, OrthonormalBasis.sum_repr_symm, isCauSeq_im, InnerProductSpace.norm_sq_eq_re_inner, Affine.Simplex.orthogonalProjectionSpan_faceOpposite_eq_point_rev, Orthonormal.inner_left_sum, Pi.orthonormalBasis.toBasis, LinearIsometry.map_starProjection, Orientation.inner_mul_areaForm_sub', inner_sub_left, Matrix.posSemidef_gram, ContinuousLinearMap.isSelfAdjoint_toLinearMap_iff, EuclideanGeometry.dist_orthogonalProjection_eq_infNndist, Submodule.inf_orthogonal, InnerProductSpace.innerSL_norm, hasFDerivAt_exp_zero, toWeakSpace_closedConvexHull_eq, Submodule.IsOrtho.le, Submodule.reflection_map, InnerProductSpace.span_gramSchmidt_Iic, LinearMap.IsSymmetric.direct_sum_isInternal, Submodule.det_reflection, TensorProduct.inner_comm_comm, Submodule.inner_orthogonalProjection_eq_of_mem_left, ContinuousLinearMap.extendTo𝕜_apply, ContinuousLinearMap.IsPositive.add, EuclideanSpace.volume_ball_fin_three, InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis, CurveIntegrable.fun_neg, ContinuousLinearMap.norm_extendTo𝕜', MeasureTheory.L2.inner_indicatorConstLp_eq_setIntegral_inner, LinearPMap.isSelfAdjoint_def, IsContDiffImplicitAt.bijective, ProbabilityTheory.covarianceBilin_apply_basisFun, hasGradientAt_iff_hasFDerivAt, Submodule.toLinearMap_orthogonalProjection_eq_linearProjOfIsCompl, curveIntegrable_neg_iff, maximal_orthonormal_iff_orthogonalComplement_eq_bot, Submodule.reflection_orthogonal, inner_eq_zero_of_left, Submodule.isOrtho_top_right, HilbertBasis.repr_symm_single, HilbertBasis.repr_apply_apply, TensorProduct.assocIsometry_apply, Matrix.toLin_conjTranspose, instStarModuleReal, Orthonormal.inner_finsupp_eq_sum_left, mul_im_I_ax, continuous_conj, LinearIsometryEquiv.rTensor_apply, LinearIsometryEquiv.inner_map_map, EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangent, InnerProductSpace.isStarProjection_rankOne_self, norm_natCast, coord_norm', contDiffAt_inner, LinearIsometry.integral_comp_comm, OrthonormalBasis.measurePreserving_repr_symm, lp.summable_inner, MeasureTheory.measureReal_abs_gt_le_integral_charFun, DifferentiableOn.inner, ClosedSubmodule.orthogonal_eq_top_iff, EuclideanSpace.piLpCongrLeft_single, hasFDerivAt_exp_smul_const, Differentiable.inner, EuclideanGeometry.dist_reflection, PreInnerProductSpace.Core.re_inner_nonneg, ofReal_intCast, InnerProductSpaceable.add_left, normSq_eq_def', ofReal_eq_zero, hasFDerivWithinAt_euclidean, ClosedSubmodule.mem_orthogonal_iff, EuclideanGeometry.orthogonalProjection_eq_orthogonalProjection_iff_vsub_mem, re_mul_ofReal, LinearMap.IsSymmetricProjection.hasOrthogonalProjection_range, Submodule.starProjection_orthogonal, ContinuousLinearMap.instNonnegSpectrumClassRealId, ContinuousMap.setOfIdeal_eq_compl_singleton, ofRealCLM_norm, stereographic_target, inner_self_ofReal_norm, Unitary.norm_map, LinearMap.instStarModuleId, Submodule.starProjection_apply_mem, LinearIsometryEquiv.symm_conjStarAlgEquiv_apply_apply, InnerProductSpace.rankOne_comp_rankOne, parallelogram_law, Submodule.orthogonal_closure', LinearIsometry.toLinearMap_rTensor, norm_re_le_norm, Matrix.toEuclideanLin_eq_toLin, Matrix.isHermitian_iff_isSymmetric, re_inner_self_pos, convex_RCLike_iff_convex_real, Submodule.le_orthogonal_iff_le_orthogonal, curveIntegral_zero, Matrix.finite_real_spectrum, InnerProductSpace.laplacian_eq_iteratedFDeriv_stdOrthonormalBasis, Submodule.IsOrtho.comap_iff, InnerProductSpace.rankOne_comp, inner_eq_neg_one_iff_of_norm_eq_one, Submodule.mem_orthogonal, exists_dual_vector', EuclideanSpace.basisFun_inner, MeasureTheory.integrable_condExpL2_of_isFiniteMeasure, inner_smul_right, Real.fourierIntegral_fderiv, InnerProductSpace.toMatrix_rankOne, EuclideanSpace.ofLp_single, LinearMap.polar_AbsConvex, differentiableAt_euclidean, EuclideanGeometry.dist_orthogonalProjection_eq_infDist, OrthonormalBasis.reindex_toBasis, nonneg_iff_exists_ofReal, geometric_hahn_banach_open, EuclideanGeometry.orthogonalProjection_mem, conj_wInner_symm, InnerProductSpace.isSymmetric_rankOne_self, ofReal_expect, Commute.cfcHom, inner_eq_one_iff_of_norm_eq_one, LinearIsometryEquiv.symm_rTensor, LinearMap.isSymmetricProjection_iff, Matrix.toEuclideanLin_conjTranspose_eq_adjoint, LinearMap.eq_adjoint_iff_basis, cfc_apply_mem_elemental, TensorProduct.commIsometry_symm, isStarProjection_starProjection, unitary.norm_map, ofReal_nonpos, SchwartzMap.tsupport_fderivCLM_subset, MeasureTheory.Integrable.inner_const, ContinuousLinearMap.integral_comp_L1_comm, curveIntegralFun_add, LinearEquiv.isSymmetric_symm_iff, InnerProductSpace.gramSchmidt_def'', OrthonormalBasis.equiv_symm, nnnorm_cfcₙHom, EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp, InnerProductSpace.Core.inner_mul_symm_re_eq_norm, MeasureTheory.integral_fin_nat_prod_eq_prod, OrthonormalBasis.orthonormal_adjustToOrientation, Continuous.inner_, curveIntegralFun_sub, ofReal_one, toIsOrderedAddMonoid, OrthogonalFamily.eq_ite, Continuous.inner, re_le_re, differentiableOn_euclidean, reLm_coe, SchwartzMap.convolution_continuous_left, ContinuousLinearMap.adjoint_toSpanSingleton, InnerProductSpace.mem_span_gramSchmidt, inner_smul_real_left, natCast_im, MeasureTheory.integrable_condExpL2_indicator, EuclideanGeometry.dist_orthogonalProjection_eq_zero_iff, nnnorm_conj, ratCast_re, range_mfderiv_coe_sphere, ofReal_div, ClosedSubmodule.inf_orthogonal_eq_bot, Submodule.reflection_eq_self_iff, stereographic_source, wInner_one_const_right, Commute.cfc, lt_iff_re_im, Matrix.posSemidef_iff_eq_sum_vecMulVec, ConvexOn.univ_sSup_affine_eq, Matrix.ofLp_toEuclideanLin_apply, SchwartzMap.integralCLM_apply, InnerProductSpace.rankOne_one_right_eq_toSpanSingleton, norm_two, EuclideanSpace.volume_ball_fin_two, norm_add_sq, norm_sq_re_conj_add, NormedSpace.polar_ball, EuclideanSpace.inner_basisFun_real, innerSLFlip_apply, EuclideanGeometry.Sphere.IsTangentAt.eq_orthogonalProjection, Submodule.ker_starProjection, sqrt_neg_I, InnerProductSpace.toContinuousLinearMap_toDualMap, MeasureTheory.MemLp.condExpL2_ae_eq_condExp', normSq_pos, InnerProductSpace.Core.inner_sub_left, Affine.Triangle.dist_circumcenter_reflection_orthocenter_finset, IsSelfAdjoint.commute_cfcₙHom, inner_eq_ofReal_norm_sq_left_iff, norm_add_mul_self, LinearIsometryEquiv.symm_conjStarAlgEquiv, Submodule.topologicalClosure_eq_top_iff, conj_im, Function.RCLike.hasTemperateGrowth_ofReal, MeasureTheory.Integrable.ofReal, EuclideanSpace.volume_ball, LinearMap.IsSymmetric.zero, TensorProduct.enorm_assoc, conj_I, OrthonormalBasis.repr_symm_single, contDiff_inner, Submodule.reflection_bot, innerSL_apply_norm, InnerProductSpace.toDual_apply_eq_toDualMap_apply, IsContDiffImplicitAt.contDiffAt, InnerProductSpace.Core.inner_self_ofReal_re, ContinuousLinearMap.isPositive_def', LinearMap.adjoint_inner_left, Matrix.frobenius_norm_mul, Matrix.star_dotProduct_gram_mulVec, hasStrictFDerivAt_exp_zero, hasSum_iff, measurable_im, curveIntegral_eq_intervalIntegral_deriv, inv_def, sqrt_I, OrthogonalFamily.range_linearIsometry, EuclideanGeometry.reflection_eq_iff_orthogonalProjection_eq, Submodule.ker_orthogonalProjection, LinearMap.IsSymmetric.hasEigenvalue_iInf_of_finiteDimensional, innerSL_real_flip, Submodule.reflection_map_apply, nnnorm_two, TensorProduct.dist_tmul_le, SchwartzMap.integral_smul_lineDerivOp_right_eq_neg_left, Submodule.sup_orthogonal_of_hasOrthogonalProjection, MeasureTheory.L2.inner_indicatorConstLp_one_indicatorConstLp_one, TensorProduct.norm_lid, MeasureTheory.lpTrimToLpMeas_ae_eq, MeasureTheory.charFun_eq_charFunDual_toDualMap, Matrix.instIsOrderedAddMonoid, CFC.quasispectrum_abs, Submodule.starProjection_orthogonalComplement_singleton_eq_zero, Submodule.isOrtho_iSup_right, TensorProduct.toLinearEquiv_assocIsometry, Submodule.IsOrtho.disjoint, SchwartzMap.compCLM_apply, EuclideanGeometry.orthogonalProjection_orthogonalProjection, norm_nnratCast, toMatrix_innerSL_apply, OrthonormalBasis.equiv_apply_basis, ClosedSubmodule.sInf_orthogonal, Orientation.volumeForm_robust', Submodule.HasOrthogonalProjection.exists_orthogonal, ModelWithCorners.convex_range', CFC.spectrum_abs, Submodule.starProjection_top, Submodule.iInf_orthogonal, ofReal_nnratCast, NormedSpace.sInter_polar_eq_closedBall, Affine.Simplex.orthogonalProjection_eq_circumcenter_of_dist_eq, lp.hasSum_inner, isBoundedBilinearMap_inner, TensorProduct.nnnorm_assoc, ofReal_pos, re_le_norm, OrthonormalBasis.norm_le_card_mul_iSup_norm_inner, wInner_zero_left, Polynomial.aeval_ofReal, ContinuousLinearMap.orthogonal_range, Submodule.lipschitzWith_starProjection, ContinuousLinearMap.isPositive_iff_complex, instSymmEqInnerOfNat, ordinaryHypergeometricSeries_eq_zero_iff, InnerProductSpace.span_gramSchmidt, EuclideanGeometry.hasFDerivAt_inversion, ofNat_im, torusIntegral_smul, OrthonormalBasis.span_apply, inner_sub_right, ClosedSubmodule.orthogonal_toSubmodule_eq, ContinuousLinearMap.isStarProjection_iff_isIdempotentElem_and_isStarNormal, ContinuousLinearMap.isPositive_iff, TensorProduct.mapIsometry_apply, InnerProductSpace.Core.inner_add_right, inv_pos, ContinuousMap.adjoin_id_eq_span_one_add, LinearMap.IsSymmetric.sub, ProbabilityTheory.covarianceBilin_map, IsHilbertSum.linearIsometryEquiv_symm_apply_dfinsupp_sum_single, real_smul_ofReal, cfcₙ_norm_sq_nonneg, SchwartzMap.instFourierSMul, SchwartzMap.fourierTransformCLM_apply, AffineSubspace.signedInfDist_singleton, norm_sq_eq_def, LinearIsometryEquiv.smul_trans, SchwartzMap.fderivCLM_fourier_eq, MeasureTheory.L2.mem_L1_inner, SchwartzMap.derivCLM_apply, TensorProduct.toLinearMap_mapIsometry, ratCast_im, Unitary.inner_map_map, I_mul_re, TensorProduct.enorm_map, uniformEquicontinuous_birkhoffAverage, wInner_neg_left, LinearMap.IsSymmetric.id, OrthonormalBasis.toMatrix_orthonormalBasis_mem_unitary, conj_eq_iff_im, ContinuousLinearMap.adjoint_comp, SchwartzMap.integral_clm_comp_deriv_right_eq_neg_left, Commute.cfcₙ, curveIntegralFun_restrictScalars, EuclideanGeometry.Sphere.IsTangent.isTangentAt, InnerProductSpace.toLinearMap_rankOne, ContinuousLinearMap.adjointAux_inner_right, HilbertBasis.repr_self, conj_re_ax, TensorProduct.commIsometry_apply, MeasureTheory.condExpInd_smul', InnerProductSpace.Core.inner_self_of_eq_zero, mul_self_norm, TensorProduct.congrIsometry_symm, LinearMap.isStarProjection_toContinuousLinearMap_iff, ContinuousLinearMap.IsPositive.orthogonalProjection_comp, LinearMap.IsSymmetric.orthogonal_range, MeasureTheory.L2.integrable_inner, dimH_orthogonalProjection_le, MeasureTheory.charFun_map_mul, inner_mul_symm_re_eq_norm, curveIntegral_fun_sub, Submodule.re_inner_starProjection_nonneg, ContDiffWithinAt.inner, Submodule.adjoint_orthogonalProjection, EuclideanGeometry.reflection_apply', hasFDerivWithinAt_iff_hasGradientWithinAt, CurveIntegrable.smul, Submodule.id_eq_sum_starProjection_self_orthogonalComplement, Submodule.isOrtho_bot_right, LinearMap.adjoint_comp, EuclideanGeometry.oangle_self_orthogonalProjection, norm_coe_norm, LinearMap.IsPositive.inner_nonneg_right, Matrix.toEuclideanLin_apply_piLp_toLp, InnerProductSpace.span_gramSchmidt_Iio, LinearIsometryEquiv.lTensor_def, mul_im, IsContDiffImplicitAt.implicitFunctionData_rightFun_pt, IsContDiffImplicitAt.contDiffAt_implicitFunction, Submodule.mem_orthogonal_singleton_iff_inner_left, ofReal_tsum, Submodule.mem_adjoint_iff, normSq_div, im_sq_le_normSq, LinearMap.isSymmetric_iff_isSelfAdjoint, inner_eq_zero_symm, lipschitzWith_ofReal, EuclideanSpace.dist_eq, Submodule.reflection_involutive, SchwartzMap.convolution_flip, Orthonormal.orthogonalFamily, LinearMap.isSymmetric_iff_sesqForm, hasStrictDerivAt_exp, ContinuousLinearMap.IsPositive.adjoint_conj, LinearIsometryEquiv.reflections_generate_dim, LinearMap.isSymmetricProjection_iff_eq_coe_starProjection, IsContDiffImplicitAt.implicitFunctionData_leftFun_apply, LinearMap.isSymmetricProjection_iff_eq_coe_starProjection_range, intervalIntegral.integral_smul_const, MeasureTheory.hausdorffMeasure_orthogonalProjection_le, HilbertBasis.summable_inner_mul_inner, ContinuousLinearMap.isPositive_iff', Submodule.finrank_add_finrank_orthogonal, ContinuousLinearMap.star_eq_adjoint, Submodule.orthogonal_eq_top_iff, Submodule.lipschitzWith_orthogonalProjection, Affine.Simplex.abs_signedInfDist_eq_dist_of_mem_affineSpan_range, volume_euclideanSpace_eq_dirac, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces, wInner_one_const_left, ProperCone.hyperplane_separation_of_notMem, OrthonormalBasis.inner_eq_one, ofReal_mul_neg_iff, orthogonalFamily_iff_pairwise, re_ofReal_pow, re_inner_self_nonpos, norm_sq_re_add_conj, LinearMap.IsSymmetric.im_inner_apply_self, Submodule.inf_orthogonal_eq_bot, Submodule.isOrtho_sSup_left, innerₛₗ_apply, deriv_inner_apply, im_to_complex, Affine.Simplex.orthogonalProjectionSpan_reindex, innerSL_apply, OrthonormalBasis.coe_toBasis_repr, InnerProductSpace.Core.cauchy_schwarz_aux', InnerProductSpace.isIdempotentElem_rankOne_self_iff, stereographic_apply, MeasureTheory.inner_condExpL2_eq_inner_fun, StrongDual.toLp_apply, OrthogonalFamily.norm_sum, HasGradientAtFilter.tendsto_nhds, Submodule.inner_starProjection_left_eq_right, MeasureTheory.mem_lpMeas_self, ContinuousLinearMap.IsPositive.spectrumRestricts, OrthonormalBasis.sum_repr, re_eq_complex_re, TemperedDistribution.derivCLM_toTemperedDistributionCLM_eq, MeasureTheory.integrableOn_condExpL2_of_measure_ne_top, IsCoercive.ker_eq_bot, InnerProductSpaceable.innerProp, norm_to_complex, Submodule.fstL_comp_coe_orthogonalDecomposition, inner_smul_left_eq_smul, imCLM_coe, re_sq_le_normSq, isStarProjection_iff_eq_starProjection_range, ContinuousLinearMap.reApplyInnerSelf_smul, conj_inv, LinearIsometryEquiv.symm_units_smul, IsHilbertSum.linearIsometryEquiv_symm_apply_single, UnitAddTorus.mFourierBasis_repr, HasDerivAt.inner, LinearIsometryEquiv.toLinearIsometry_rTensor, Submodule.starProjection_minimal, EuclideanGeometry.orthogonalProjection_linear, OrthonormalBasis.sum_rankOne_eq_id, fourierBasis_repr, AffineSubspace.signedInfDist_def, Submodule.starProjection_mem_subspace_eq_self, MeasureTheory.BoundedContinuousFunction.inner_toLp, ContinuousLinearMap.adjoint_inner_right, MeasureTheory.integral_fintype_prod_volume_eq_prod, mul_re, TensorProduct.norm_tmul, LinearMap.isPositive_iff, LinearIsometryEquiv.symm_smul_apply, SchwartzMap.tsupport_derivCLM_subset, Affine.Simplex.orthogonalProjectionSpan_eulerPoint_mem_ninePointCircle, normSq_zero, OrthonormalBasis.coe_toBasis_repr_apply, enorm_conj, inner_smul_right_eq_smul, LinearIsometryEquiv.star_eq_symm, orthonormal_iff_ite, wInner_add_left, SchwartzMap.integral_smul_laplacian_right_eq_left, EuclideanGeometry.reflection_involutive, ContinuousOn.inner, re_le_neg_norm_iff_eq_neg_norm, OrthonormalBasis.coe_equiv_euclideanSpace, conjAe_coe, neg_iff_exists_ofReal, wInner_one_eq_sum, InnerProductSpace.Core.inner_add_add_self, inner_self_eq_one_of_norm_one, norm_cfcHom, to_complex_nonneg_iff, EuclideanSpace.dist_sq_eq, integral_ofReal, sqrt_zero, Submodule.orthogonalProjectionFn_eq, TensorProduct.nnnorm_comm, Submodule.IsOrtho.ge, Affine.Simplex.signedInfDist_affineCombination, Submodule.bot_orthogonal_eq_top, signedDist_apply, UniformSpace.Completion.inner_coe, ContinuousLinearMap.IsPositive.conj_starProjection, EuclideanGeometry.angle_self_orthogonalProjection, EuclideanSpace.inner_toLp_toLp, Orthonormal.comp_linearIsometryEquiv, im_ofReal_mul, Submodule.map_orthogonal, Matrix.l2_opNNNorm_diagonal, inner_self_re_eq_norm, ordinaryHypergeometric_radius_top_of_neg_nat₁, Matrix.instCStarRing, normSq_eq_zero, AffineSubspace.direction_perpBisector, instOrderClosedTopology, LinearMap.IsSymmetric.conj_inner_sym, Filter.Tendsto.inner, MeasureTheory.Integrable.const_inner, OrthonormalBasis.same_orientation_iff_det_eq_det, ContinuousLinearMap.extendTo𝕜'_apply, ClosedSubmodule.orthogonal_disjoint, I_re, ContinuousLinearMap.isAdjointPair_inner, TensorProduct.norm_map, dist_birkhoffAverage_birkhoffAverage_le, ContinuousLinearMap.coe_le_coe_iff, AddChar.linearIndependent, instPosMulReflectLE, EuclideanGeometry.orthogonalProjection_eq_self_iff, im_eq_complex_im, EuclideanGeometry.reflection_subtype, Submodule.orthogonal_le_orthogonal_iff, Submodule.orthogonal_le_iff_orthogonal_le, Orientation.finOrthonormalBasis_orientation, ofReal_im_ax, ContinuousLinearEquiv.coord_norm', OrthonormalBasis.toMatrix_orthonormalBasis_self_mul_conjTranspose, ContinuousLinearMap.isPositive_zero, Submodule.snd_orthogonalDecomposition_apply, cfcₙ_apply_mem_elemental, InnerProductSpace.Core.inner_self_im, SchwartzMap.fourier_fderivCLM_eq, Unitary.conjStarAlgAut_symm_unitaryLinearIsometryEquiv, ContinuousLinearMap.integral_comp_id_comm, hasStrictFDerivAt_exp_smul_const, SchwartzMap.fourier_convolution_apply, instNormSMulClassInt, Submodule.starProjection_le_starProjection_iff, ContDiffAt.inner, wInner_cWeight_const_right, ContinuousMap.elemental_id_eq_top, LinearMap.eq_adjoint_iff_basis_right, Submodule.instOrthogonalCompleteSpace, IsSelfAdjoint.commute_cfcₙ, AEMeasurable.re, hasDerivAt_exp_smul_const', instOrderIsoClassContinuousLinearMapIdOfNonUnitalAlgEquivClassOfStarHomClassOfContinuousMapClass, LinearMap.isStarProjection_iff_isSymmetricProjection, LinearIsometryEquiv.toLinearEquiv_rTensor, EuclideanSpace.nnnorm_eq, innerₛₗ_apply_coe, nnnorm_natCast, PiLp.inner_apply, Submodule.orthogonalDecomposition_apply, Submodule.isOrtho_self, LinearIsometryEquiv.toLinearIsometry_lTensor, AddChar.wInner_cWeight_eq_boole, IsContDiffImplicitAt.implicitFunction_def, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm, OrthonormalBasis.toMatrix_orthonormalBasis_conjTranspose_mul_self, range_cfcHom, re_ofReal_mul, norm_add_pow_two, ClosedSubmodule.orthogonal_closure, AddChar.map_neg_eq_conj, hasGradientWithinAt_iff_tendsto, InnerProductSpace.add_left, OrthonormalBasis.toMatrix_orthonormalBasis_mem_orthogonal, EuclideanSpace.inner_single_right, norm_eq_sqrt_re_inner, iInter_halfSpaces_eq, inner_self_nonneg, nnnorm_cfcHom, normSq_to_complex, OrthonormalBasis.orientation_adjustToOrientation, continuous_im, EuclideanGeometry.orthogonalProjection_vsub_mem_direction_orthogonal, MeasureTheory.lpMeasToLpTrim_ae_eq, Submodule.orthogonal_eq_inter, normSq_add, MeasureTheory.eLpNorm_condExpL2_le, div_re, geometric_hahn_banach_compact_closed, SchwartzMap.smulLeftCLM_ofReal, LinearMap.IsPositive.adjoint_eq, fderiv_norm_rpow, ContinuousLinearMap.norm_map_iff_adjoint_comp_self, Matrix.toEuclideanLin_eq_toLin_orthonormal, MeasureTheory.lpMeasToLpTrim_smul, Submodule.starProjection_orthogonal_val, isStarProjection_iff_eq_starProjection, ContinuousLinearMap.norm_adjoint_comp_self, LinearPMap.mem_adjoint_domain_iff, geometric_hahn_banach_point_closed, LinearMap.IsSymmetricProjection.le_iff_range_le_range, intervalIntegral_ofReal, UniformSpace.Completion.continuous_inner, EuclideanGeometry.eq_orthogonalProjection_of_eq_subspace, EuclideanGeometry.orthogonalProjection_apply, IsometricContinuousFunctionalCalculus.isGreatest_norm_spectrum, curveIntegral_def', re_inner_eq_norm_add_mul_self_sub_norm_sub_mul_self_div_four, EuclideanGeometry.Sphere.direction_orthRadius, ContinuousMapZero.elemental_eq_top, ContinuousMapZero.adjoin_id_dense, EuclideanGeometry.eq_reflection_of_eq_subspace, OrthonormalBasis.coe_singleton, LinearIsometry.rTensor_apply, NormedSpace.polar_closedBall, Submodule.norm_orthogonalProjection, Matrix.l2_opNNNorm_conjTranspose_mul_self, Submodule.instHasOrthogonalProjectionTop, AffineSubspace.signedInfDist_apply_self, EuclideanGeometry.orthogonalProjection_vsub_orthogonalProjection, LinearIsometry.toLinearMap_lTensor, EuclideanGeometry.orthogonalProjection_mem_orthogonal, coe_innerₛₗ_apply, ContinuousWithinAt.inner, curveIntegral_add, TensorProduct.nndist_tmul_le, hasDerivAt_exp_zero, MeasureTheory.charFun_map_eq_charFunDual_smul, InnerProductSpace.continuousLinearMapOfBilin_apply, hasGradientWithinAt_iff_isLittleO, Matrix.cstar_norm_def, norm_sub_pow_two, conj_eq_re_sub_im, DFinsupp.inner_sum, InnerProductSpace.Core.re_inner_smul_ofReal_smul_self, Submodule.HasOrthogonalProjection.map_linearIsometryEquiv, inner_matrix_row_row, MeasureTheory.condExpIndSMul_ae_eq_smul, MeasureTheory.intervalIntegrable_charFun, ContinuousMap.idealOf_compl_singleton_isMaximal, MeasureTheory.lpMeas.ae_fin_strongly_measurable', gaugeSeminormFamily_ball, curveIntegral_sub, sqrt_normSq_eq_norm, conj_ofNat, HasGradientAt.fderiv_apply, SchwartzMap.instFourierInvSMul, TemperedDistribution.derivCLM_apply_apply, OrthonormalBasis.tensorProduct_apply, EuclideanGeometry.two_zsmul_oangle_orthogonalProjection_self, tendsto_ofReal_atBot_cobounded, MeasureTheory.condExpIndSMul_smul', Complex.isometryOfOrthonormal_symm_apply, Matrix.instStarOrderedRing, normSq_apply, CurveIntegrable.sub, PreInnerProductSpace.Core.add_left, ofRealCLM_coe, TensorProduct.congrIsometry_apply, ConvexOn.exists_affine_le_of_lt, OrthonormalBasis.det_to_matrix_orthonormalBasis_real, MeasureTheory.integral_prod_smul, inner_sub_sub_self, ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_right, innerSL_apply_coe, ContinuousLinearMap.isPositive_one, ContinuousLinearMap.isPositive_sum, instIsRCLikeNormedField, ordinaryHypergeometricSeries_norm_div_succ_norm, HasStrictFDerivAt.inner, MeasureTheory.ContinuousMap.inner_toLp, gradient_eq_deriv, re_inner_le_norm, Submodule.orthogonalProjection_comp_subtypeL_eq_zero_iff, LinearMap.toMatrix_adjoint, Affine.Simplex.reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter, inner_eq_one_iff_of_norm_one, ProbabilityTheory.charFun_gaussianReal, CFC.abs_smul, conj_smul, HilbertBasis.tsum_inner_mul_inner, EuclideanGeometry.coe_orthogonalProjection_eq_iff_mem, mul_re_ax, ContinuousLinearMap.isPositive_adjoint_comp_self, SchwartzMap.integral_clm_comp_laplacian_right_eq_left, ContinuousLinearMap.integral_comp_comm, EuclideanSpace.single_eq_zero_iff, TensorProduct.nnnorm_lid, LinearMap.im_inner_adjoint_mul_self_eq_zero, instTietzeExtension, ClosedSubmodule.orthogonal_closure', Matrix.l2_opNorm_def, OrthogonalFamily.linearIsometry_apply, Matrix.toEuclideanLin_toLp, continuous_stereoInvFun, Submodule.orthogonalProjection_eq_zero_iff, MeasureTheory.condExpL1CLM_smul, Matrix.l2_opNorm_mul, norm_innerSL_le, norm_inner_symm, OrthonormalBasis.measurePreserving_measurableEquiv, ContinuousLinearMap.IsPositive.isSelfAdjoint, OrthonormalBasis.sum_repr', norm_le_im_iff_eq_I_mul_norm, real_smul_eq_coe_mul, Submodule.coe_orthogonalProjection_apply, Submodule.starProjection_coe_eq_isCompl_projection, ofReal_inv, ContinuousMap.idealOfSet_ofIdeal_isClosed, ofRealAm_coe, normSq_one, re_to_complex, orthonormal_vecCons_iff, SchwartzMap.integral_smul_deriv_right_eq_neg_left, LinearMap.posSemidef_toMatrix_iff, Submodule.starProjection_apply_eq_zero_iff, SchwartzMap.fourier_convolution, Orthonormal.inner_right_fintype, charZero_rclike, EuclideanSpace.nndist_single_same, OrthonormalBasis.abs_det_adjustToOrientation, HasGradientWithinAt.hasFDerivWithinAt, EuclideanSpace.edist_eq, hasFDerivAt_exp, EuclideanSpace.single_apply, isCauSeq_re, Pi.orthonormalBasis_repr, hasSum_conj', IsHilbertSum.linearIsometryEquiv_apply_dfinsupp_sum_single, InnerProductSpace.conj_inner_symm, I_im', Orthonormal.tmul, LinearMap.isAdjointPair_inner, MeasureTheory.condExpIndL1Fin_smul', LinearMap.IsPositive.adjoint_conj, LinearMap.isPositive_one, Affine.Triangle.dist_orthocenter_reflection_circumcenter_finset, Affine.Simplex.affineSpan_pair_eq_altitude_iff, range_cfc, wInner_add_right, Affine.Simplex.direction_altitude, LinearIsometryEquiv.symm_lTensor, DifferentiableWithinAt.inner, Submodule.isOrtho_bot_left, EuclideanGeometry.dist_orthogonalProjection_line_eq_iff_two_zsmul_oangle_eq, HilbertBasis.hasSum_inner_mul_inner, LinearIsometryEquiv.toContinuousLinearEquiv_smul, fderivInnerCLM_apply, Orthonormal.sum_inner_products_le, EuclideanGeometry.orthogonalProjection_eq_iff_mem, ConvexOn.sSup_affine_eq, EuclideanGeometry.dist_orthogonalProjection_line_eq_of_two_zsmul_oangle_eq, Submodule.orthogonalProjection_coe_eq_linearProjOfIsCompl, I_mul_I_of_nonzero, I_mul_I_ax, SchwartzMap.toZeroAtInftyCLM_apply, LinearMap.IsSymmetric.coe_re_inner_apply_self, span_one_I, OrthogonalFamily.summable_iff_norm_sq_summable, CurveIntegrable.add, geometric_hahn_banach_closed_compact, MeasureTheory.eLpNorm_conj, MeasureTheory.lpMeasToLpTrimLie_symm_toLp, LinearIsometryEquiv.conjStarAlgEquiv_apply_apply, DFinsupp.sum_inner, Real.fourierIntegral_iteratedFDeriv, hasStrictDerivAt_exp_zero, Submodule.orthogonalProjection_norm_le, EuclideanSpace.volume_closedBall, intCast_im, ofReal_sum, ContinuousMap.idealOfSet_ofIdeal_eq_closure, finrank_euclideanSpace_fin, Submodule.orthogonalProjection_orthogonal, inner_conj_symm, LinearIsometryEquiv.rTensor_def, MeasureTheory.norm_condExpL2_le_one, AddChar.inv_apply_eq_conj, OrthonormalBasis.repr_reindex, MeasureTheory.condExpL2_comp_continuousLinearMap, inner_im_symm, re_extendTo𝕜'ₗ, InnerProductSpace.symm_toEuclideanLin_rankOne, Submodule.orthogonalProjection_orthogonalComplement_singleton_eq_zero, Submodule.isOrtho_sup_left, MeasureTheory.memLp_re_im_iff, ContinuousLinearMap.adjoint_innerSL_apply, Submodule.IsOrtho.comap, OrthogonalFamily.inner_right_fintype, EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentAt, binomialSeries_radius_ge_one, normSq_sub, InnerProductSpace.Core.toSeminormedSpaceCore, Submodule.orthogonalProjection_eq_linearProjOfIsCompl, Orthonormal.inner_sum, EuclideanGeometry.reflection_apply, intervalIntegral.integral_mul_const, ContinuousLinearMap.IsPositive.re_inner_nonneg_right, wInner_cWeight_eq_smul_wInner_one, ContinuousMap.idealOfSet_isMaximal_iff, ContinuousLinearMap.integral_id_map, MeasureTheory.condExpL2_const_inner, curveIntegrable_restrictScalars_iff, LinearMap.IsSymmetric.intCast, IsCoercive.isClosed_range, InnerProductSpace.Core.inner_zero_left, TensorProduct.ext_iff_inner_right_threefold, curveIntegralFun_def, InnerProductSpaceable.inner_.conj_symm, ContinuousLinearMap.intervalIntegral_comp_comm, inner_eq_ofReal_norm_sq_right_iff, tendsto_ofReal_atTop_cobounded, CurveIntegrable.neg, Matrix.IsHermitian.instContinuousFunctionalCalculus, MeasureTheory.integral_convolution, contDiff_euclidean, fderiv_norm_sq_apply, Submodule.starProjection_eq_self_iff, IsSelfAdjoint.commute_cfc, imCLM_apply, cfcHom_apply_mem_elemental, OrthonormalBasis.tensorProduct_repr_tmul_apply, conj_neg_I, ConvexOn.univ_sSup_of_nat_affine_eq, Matrix.posSemidef_iff_isHermitian_and_spectrum_nonneg, inv_I, TensorProduct.assocIsometry_symm_apply, InnerProductSpace.Core.inner_conj_symm, InnerProductSpace.gramSchmidt_mem_span, MeasureTheory.MemLp.ofReal, LinearMap.IsSymmetric.add, inner_eq_wInner_one, TensorProduct.inner_map_map, geometric_hahn_banach_open_open, MeasureTheory.integral_mul_const, lipschitzWith_im, fderiv_norm_sq, LinearMap.IsSymmetric.orthogonalFamily_iInf_eigenspaces, TensorProduct.toLinearMap_mapInclIsometry, OrthogonalFamily.inner_right_dfinsupp, Orientation.inner_mul_inner_add_areaForm_mul_areaForm', orthonormal_span, ContinuousLinearMap.innerSL_apply_comp, TensorProduct.lidIsometry_symm_apply, ContinuousLinearMap.instStarOrderedRingRCLike, surjective_stereographic, inner_vsub_left_eq_zero_symm, MeasureTheory.FiniteMeasure.tendsto_iff_forall_integral_rclike_tendsto, ContinuousLinearMap.toSesqForm_apply_norm_le, HilbertBasis.hasSum_repr_symm, inner_neg_left, hasFDerivAt_stereoInvFunAux_comp_coe, LinearMap.adjoint_id, inner_smul_left, InnerProductSpace.nullSubmodule_le_ker_toDualMap_right, MeasureTheory.condExpL2_indicator_nonneg, ContinuousLinearMap.adjoint_adjoint, IsContDiffImplicitAt.implicitFunctionData_leftFun_pt, restrict_toContinuousMap_eq_toContinuousMapStar_restrict, im_le_norm, fderiv_inner_apply, norm_inner_le_norm, inner_matrix_col_col, Affine.Simplex.altitude_def, div_I, normSq_conj, OrthonormalBasis.inner_eq_ite, ContinuousLinearMap.orthogonal_ker, InnerProductSpace.norm_rankOne, Submodule.isHilbertSumOrthogonal, inv_re, ofReal_ratCast, real_inner_I_smul_self, LinearIsometry.lTensor_def, Orthonormal.inner_right_sum, TensorProduct.edist_tmul_le, unitary.inner_map_map, LinearMap.IsPositive.conj_adjoint, norm_of_nonneg, Orthonormal.tsum_inner_products_le, Matrix.gram_single, LinearMap.IsSymmetric.pow, InnerProductSpace.Core.inner_sub_right, EuclideanGeometry.orthogonalProjection_mem_subspace_eq_self, curveIntegralFun_zero, Submodule.orthogonalProjectionFn_mem, Orthonormal.inner_eq_zero, LinearMap.IsPositive.re_inner_nonneg_left, zero_im, ContinuousLinearMapWOT.ext_inner_iff, Matrix.permMatrix_l2_opNorm_eq, norm_inner_div_norm_mul_norm_eq_one_iff, MeasureTheory.lpMeas.aestronglyMeasurable, geometric_hahn_banach_open_point, Submodule.mem_iff_norm_starProjection, IsCoercive.antilipschitz, InnerProductSpace.gramSchmidt_inv_triangular, Orthonormal.comp_linearIsometry, hasStrictFDerivAt_euclidean, unitary.linearIsometryEquiv_coe_apply, HilbertBasis.finite_spans_dense, ofReal_lt_zero
|
toNormedAlgebra 📖 | CompOp | 218 mathmath: TemperedDistribution.lineDerivOpCLM_eq, ContDiffBump.ae_convolution_tendsto_right_of_locallyIntegrable, map_apply, IsSelfAdjoint.quasispectrumRestricts, Matrix.IsHermitian.isClosedEmbedding_cfcAux, ofRealCLM_apply, Real.hasFDerivAt_fourierChar_neg_bilinear_left, reCLM_apply, LinearMap.IsSymmetric.restrictScalars, Convex.convex_isRCLikeNormedField, Matrix.IsHermitian.det_abs, ofRealLI_apply, ModularForm.mul_slash, Matrix.IsHermitian.cfc_eq, conjCLE_norm, ContinuousLinearMap.integral_apply, algebraMap_eq_ofReal, SchwartzMap.integral_clm_comp_lineDerivOp_right_eq_neg_left, Unitization.real_cfcₙ_eq_cfc_inr, SchwartzMap.lineDerivOp_fourier_eq, map_same_eq_id, IsConformalMap.is_complex_or_conj_linear, re_add_im_ax, Matrix.PosSemidef.sqrt_eq_zero_iff, MeasureTheory.integral_const_mul, Complex.hasStrictFDerivAt_exp_real, ModularForm.prod_slash, SchwartzMap.laplacianCLM_eq, MeasureTheory.integral_div, isSelfAdjoint_iff_isStarNormal_and_spectrumRestricts, ContinuousLinearMap.norm_extendTo𝕜, smul_re, ModularForm.prod_slash_sum_weights, MeasureTheory.convolution_tendsto_right, cfcₙ_integral, reCLM_norm, cfcₙ_setIntegral, conjCLE_apply, UpperHalfPlane.coe_pos_real_smul, Complex.starConvex_ofReal_slitPlane, toIsStrictOrderedModule, intervalIntegral.hasFDerivAt_integral_of_dominated_loc_of_lip, SchwartzMap.fourier_lineDerivOp_eq, Complex.starConvex_one_slitPlane, TemperedDistribution.instLineDerivLeftSMulReal, SchwartzMap.smulLeftCLM_real_smul, NumberField.mixedEmbedding.fundamentalCone.smul_mem_of_mem, Matrix.PosSemidef.det_sqrt, integral_smul_const, convex_halfSpace_re_le, MeasureTheory.convolution_precompR_apply, Matrix.IsHermitian.charpoly_cfc_eq, FiniteDimensional.rclike_to_real, Polynomial.ofReal_eval, Matrix.PosSemidef.posSemidef_sqrt, conjLIE_apply, imLm_coe, ContDiffBump.convolution_tendsto_right, conjCLE_coe, convex_halfSpace_im_gt, Matrix.PosSemidef.sqrt_eq_one_iff, Real.LogDeriv_exp, Matrix.PosSemidef.sqrt_sq, rank_le_two, reCLM_coe, ContDiffBump.normed_convolution_eq_right, NormedSpace.exp_continuousMap_eq, MeasureTheory.hasFDerivAt_convolution_right_with_param, Matrix.PosSemidef.eq_sqrt_iff_sq_eq, HasCompactSupport.hasFDerivAt_convolution_right, NumberField.mixedEmbedding.convexBodySumFun_smul, NumberField.mixedEmbedding.logMap_real_smul, LinearMap.extendTo𝕜_apply, HasDerivWithinAt.complexToReal_fderiv, integral_conj, ofReal_re_ax, hasFDerivAt_integral_of_dominated_loc_of_lip', MeasureTheory.L2.inner_indicatorConstLp_indicatorConstLp, HasDerivAt.complexToReal_fderiv, inner_smul_real_right, convex_halfSpace_im_lt, MeasureTheory.dist_convolution_le, cfcHom_real_eq_restrict, IsSelfAdjoint.spectrumRestricts, Complex.restrictScalars_one_smulRight, Matrix.IsHermitian.cfcAux_apply, SchwartzMap.fourierInv_lineDerivOp_eq, finrank_le_two, sqrt_map, Matrix.instFiniteElemRealSpectrum, smul_im, SpectrumRestricts.real_iff, Polynomial.aeval_conj, wInner_const_left, QuasispectrumRestricts.real_iff, TemperedDistribution.instLineDerivSMulReal, NumberField.mixedEmbedding.norm_smul, cfc_integral, ConvexOn.convex_re_epigraph, SchwartzMap.integral_pow_mul_iteratedFDeriv_le, realLinearIsometryEquiv_symm_apply, isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts, ofReal_alg, curveIntegralFun_def', ContinuousMultilinearMap.integral_apply, Matrix.PosSemidef.isUnit_sqrt_iff, complexLinearIsometryEquiv_symm_apply, MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_integral_rclike_tendsto, wInner_const_right, convex_halfSpace_re_ge, convex_halfSpace_im_ge, ContinuousLinearMap.extendTo𝕜_apply, Real.logDeriv_exp, convex_halfSpace_re_lt, Complex.restrictScalars_toSpanSingleton, instStarModuleReal, Matrix.PosSemidef.sq_sqrt, Unitization.nnreal_cfcₙ_eq_cfc_inr, ofRealCLM_norm, Complex.sqrt_map, isConformalMap_complex_linear_conj, Matrix.PosSemidef.inv_sqrt, Matrix.finite_real_spectrum, intervalIntegral.hasFDerivAt_integral_of_dominated_of_fderiv_le, cfcₙHom_real_eq_restrict, NumberField.canonicalEmbedding.mem_rat_span_latticeBasis, ContinuousLinearMap.intervalIntegral_apply, LindemannWeierstrass.integral_exp_mul_eval, Matrix.IsHermitian.exists_eigenvector_of_ne_zero, reLm_coe, inner_smul_real_left, integral_coe_re_add_coe_im, hahnEmbedding_isOrderedModule_rat, SchwartzMap.integralCLM_apply, SchwartzMap.lineDerivOp_fourierInv_eq, Matrix.IsHermitian.spectrum_real_eq_range_eigenvalues, NumberField.mixedEmbedding.convexBodyLT_convex, NormedAlgebra.Real.nonempty_algEquiv_or, ModelWithCorners.convex_range', ContDiffBump.convolution_eq_right, Polynomial.aeval_ofReal, Matrix.IsHermitian.cfcAux_id, real_smul_ofReal, SchwartzMap.fderivCLM_fourier_eq, SchwartzMap.derivCLM_apply, map_nonneg_iff, ContDiffBump.dist_normed_convolution_le, SchwartzMap.integral_clm_comp_deriv_right_eq_neg_left, NumberField.mixedEmbedding.logMap_real, Complex.log_eq_integral, hasFDerivAt_integral_of_dominated_of_fderiv_le, Real.logDeriv_sin, NumberField.mixedEmbedding.normAtPlace_smul, ModularForm.prod_fintype_slash, Real.nonempty_algEquiv_or, Complex.starConvex_slitPlane, Matrix.IsHermitian.eigenvalues_mem_spectrum_real, TemperedDistribution.derivCLM_toTemperedDistributionCLM_eq, Orientation.kahler_apply_apply, imCLM_coe, SchwartzMap.tsupport_derivCLM_subset, conjAe_coe, toContinuousLinearMap_complexLinearIsometryEquiv, integral_ofReal, Polynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv, Real.hasFDerivAt_fourierChar_neg_bilinear_right, ofReal_im_ax, SchwartzMap.fourier_fderivCLM_eq, Complex.hasStrictFDerivAt_log_real, Quaternion.coe_ofComplex, NumberField.mixedEmbedding.convexBodySum_convex, convex_halfSpace_im_le, Matrix.PosSemidef.sqrt_mul_self, setIntegral_re_add_im, SchwartzMap.smulLeftCLM_ofReal, curveIntegral_def', NumberField.mixedEmbedding.fundamentalCone.smul_mem_iff_mem, isConformalMap_complex_linear, instNonemptySeedRatReal, TemperedDistribution.derivCLM_apply_apply, integral_re, ofRealCLM_coe, HasStrictDerivAt.complexToReal_fderiv, convex_halfSpace_re_gt, Real.logDeriv_cos, conj_smul, Real.logDeriv_cosh, SchwartzMap.integral_clm_comp_laplacian_right_eq_left, Matrix.IsHermitian.mulVec_eigenvectorBasis, integral_re_add_im, Real.deriv_log_comp_eq_logDeriv, Subalgebra.SeparatesPoints.rclike_to_real, real_smul_eq_coe_mul, ofRealAm_coe, SchwartzMap.fourier_convolution, Complex.log_inv_eq_integral, ContDiffBump.convolution_tendsto_right_of_continuous, isConformalMap_iff_is_complex_or_conj_linear, span_one_I, Matrix.PosDef.posDef_sqrt, LindemannWeierstrass.hasDerivAt_cexp_mul_sumIDeriv, re_extendTo𝕜'ₗ, realLinearIsometryEquiv_apply, Matrix.IsHermitian.instContinuousFunctionalCalculus, imCLM_apply, cfc_setIntegral, MeasureTheory.integral_mul_const, MeasureTheory.FiniteMeasure.tendsto_iff_forall_integral_rclike_tendsto, integral_im, HasCompactSupport.hasFDerivAt_convolution_left, NumberField.mixedEmbedding.convexBodyLT'_convex, Matrix.PosSemidef.sqrt_eq_iff_eq_sq, TemperedDistribution.smulLeftCLM_apply_apply, NumberField.mixedEmbedding.mem_rat_span_latticeBasis, restrict_toContinuousMap_eq_toContinuousMapStar_restrict, Complex.continuousOn_one_add_mul_inv, complexLinearIsometryEquiv_apply, hasFDerivAt_integral_of_dominated_loc_of_lip
|
toPartialOrder 📖 | CompOp | 64 mathmath: pos_iff_exists_ofReal, Matrix.posSemidef_iff_eq_conjTranspose_mul_self, LinearMap.IsPositive.ne_zero_iff, Matrix.le_iff, pos_iff, ContinuousLinearMap.IsPositive.inner_nonneg_right, toStarOrderedRing, nonpos_iff, nonpos_iff_exists_ofReal, LinearMap.IsPositive.isPositive_smul_iff, toIsStrictOrderedModule, toIsStrictOrderedRing, re_nonneg_of_nonneg, ofReal_nonneg, toPosMulReflectLT, LinearMap.IsPositive.inner_nonneg_left, re_monotone, Matrix.PosSemidef.posSemidef_sqrt, ofReal_le_ofReal, Matrix.LE.le.posSemidef, Matrix.posDef_gram_of_linearIndependent, instMulPosReflectLE, le_iff_re_im, Matrix.IsHermitian.posSemidef_iff_eigenvalues_nonneg, Matrix.nonneg_iff_posSemidef, Matrix.posDef_gram_iff_linearIndependent, neg_iff, ofReal_mul_pos_iff, Matrix.IsHermitian.posSemidef_of_eigenvalues_nonneg, toZeroLEOneClass, with_gaugeSeminormFamily, Matrix.isStrictlyPositive_iff_posDef, nonneg_iff, Matrix.isPositive_toEuclideanLin_iff, Matrix.posDef_iff_eq_conjTranspose_mul_self, ContinuousLinearMap.IsPositive.inner_nonneg_left, Matrix.posSemidef_gram, toWeakSpace_closedConvexHull_eq, convex_RCLike_iff_convex_real, LinearMap.polar_AbsConvex, nonneg_iff_exists_ofReal, ofReal_nonpos, toIsOrderedAddMonoid, lt_iff_re_im, Matrix.posSemidef_iff_eq_sum_vecMulVec, ofReal_pos, ContinuousLinearMap.isPositive_iff, inv_pos, map_nonneg_iff, LinearMap.IsPositive.inner_nonneg_right, ContinuousLinearMap.isPositive_iff', ofReal_mul_neg_iff, LinearMap.isPositive_iff, neg_iff_exists_ofReal, to_complex_nonneg_iff, instOrderClosedTopology, instPosMulReflectLE, Matrix.IsHermitian.posDef_iff_eigenvalues_pos, gaugeSeminormFamily_ball, Matrix.IsStrictlyPositive.posDef, LinearMap.posSemidef_toMatrix_iff, Matrix.posSemidef_iff_isHermitian_and_spectrum_nonneg, ofReal_lt_ofReal, ofReal_lt_zero
|
toStarRing 📖 | CompOp | 444 mathmath: Matrix.l2_opNorm_toEuclideanCLM, Pi.comul_eq_adjoint, LinearMap.IsSymmetric.clm_adjoint_eq, conj_re, integrableOn_cfcₙ', MeasureTheory.lpNorm_conj, continuous_cfcₙHomSuperset_left, LinearMap.IsSymmetric.conj_eigenvalue_eq_self, cfcₙL_integral, ContinuousLinearMap.isPositive_iff_eq_sum_rankOne, continuousOn_stereoToFun, InnerProductSpace.isPositive_rankOne_self, Orthonormal.inner_left_finsupp, norm_cfcₙHom, LinearMap.adjoint_adjoint, InnerProductSpace.toLinearIsometry_toDual, IsSelfAdjoint.commute_cfcHom, cfcₙ_norm_nonneg, ContinuousWithinAt.cfcₙ, hasFDerivAt_iff_hasGradientAt, cfcₙHom_apply_mem_elemental, Filter.Tendsto.cfc, InnerProductSpace.rankOne_one_left_eq_innerSL, nnnorm_cfc_lt, Matrix.posSemidef_iff_eq_conjTranspose_mul_self, LinearMap.isPositive_adjoint_comp_self, InnerProductSpace.isIdempotentElem_rankOne_self, Matrix.cstar_nnnorm_def, star_def, integrableOn_cfc', inner_apply', flip_innerSL_real, Matrix.le_iff, norm_cfc_lt_iff, sub_conj, isClosedEmbedding_cfcₙAux, innerSL_apply_apply, CFC.abs_eq_cfcₙ_coe_norm, LinearMap.adjoint_innerₛₗ_apply, EuclideanSpace.inner_single_left, ContinuousLinearMap.innerSL_apply_comp_of_isSymmetric, LinearMap.adjoint_eq_toCLM_adjoint, nnnorm_cfcₙ_lt_iff, ContinuousOn.cfcₙ', OrthonormalBasis.orthogonalProjection_eq_sum_rankOne, InnerProductSpace.Core.inner_smul_left, InnerProductSpace.toDual_symm_apply, conj_nat_cast, IsGreatest.nnnorm_cfcₙ, ContinuousAt.cfc, MeasureTheory.charFun_toDual_symm_eq_charFunDual, PreInnerProductSpace.Core.smul_left, Differentiable.fderiv_norm_rpow, toStarOrderedRing, is_real_TFAE, inner_gradientWithin_right, ContinuousLinearMap.adjoint_id, InnerProductSpace.smul_left, ContinuousLinearMap.isStarNormal_iff_norm_eq_adjoint, LinearMap.toMatrixOrthonormal_reindex, norm_cfc_le_iff, mul_conj, norm_conj, InnerProductSpace.inner_left_rankOne_apply, HasFDerivAt.norm_sq, polynomialFunctions.starClosure_topologicalClosure, innerₛₗ_apply_apply, ContinuousLinearMap.eq_adjoint_iff, Continuous.cfc', InnerProductSpace.rankOne_apply, nonUnitalContinuousFunctionalCalculus, HasDerivAt.hasGradientAt, cfcₙ_integral, IsSelfAdjoint.adjoint_eq, TensorProduct.adjoint_map, cfcₙ_setIntegral, ContinuousLinearMap.isPositive_self_comp_adjoint, LinearMap.adjoint_toContinuousLinearMap, ContinuousLinearMap.toSesqForm_apply_coe, LinearIsometryEquiv.adjoint_eq_symm, LinearIsometryEquiv.trans_smul, im_eq_zero_iff_isSelfAdjoint, conjCLE_apply, Orthonormal.inner_left_fintype, cfcL_integrable, ContinuousLinearMap.adjointAux_norm, Pi.counit_eq_adjoint, LinearMap.toMatrixOrthonormal_apply_apply, instCStarRing, ContinuousOn.cfc, Real.fourier_iteratedFDeriv, LinearIsometryEquiv.adjoint_toLinearMap_eq_symm, InnerProductSpace.toDualMap_apply_apply, LinearMap.eq_adjoint_iff_basis_left, coe_innerSL_apply, range_cfcₙHom, norm_cfcₙ_lt, InnerProductSpace.nnnorm_rankOne, PreInnerProductSpace.Core.conj_inner_symm, InnerProductSpace.isSymmetricProjection_rankOne_self, IsGreatest.norm_cfcₙ, hasGradientWithinAt_iff_hasFDerivWithinAt, ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_left, LinearIsometryEquiv.smul_apply, cfcₙ_comp_norm, Continuous.cfcₙ_of_mem_nhdsSet, Matrix.PosSemidef.posSemidef_sqrt, cfcₙHom_integral, Continuous.cfcₙ, continuousOn_cfc_setProd, LinearMap.IsSymmetric.hasStrictFDerivAt_reApplyInnerSelf, conj_ofReal, Submodule.adjoint_subtypeL, IsGreatest.norm_cfc, LinearMap.isSymmetric_adjoint_mul_self, conjLIE_apply, conj_mul, Matrix.LE.le.posSemidef, InnerProductSpace.trace_rankOne, continuousOn_cfcₙ, hasFDerivAt_norm_rpow, Matrix.eigenvalues_conjTranspose_mul_self_nonneg, instContinuousMapUniqueHom, ContinuousLinearMap.IsPositive.conj_adjoint, Matrix.toEuclideanCLM_toLp, WeakDual.CharacterSpace.homeoEval_naturality, contDiffOn_stereoToFun, Matrix.posDef_gram_of_linearIndependent, range_cfcₙ, LinearMap.adjoint_rTensor, LinearMap.adjoint_inner_right, InnerProductSpace.adjoint_rankOne, InnerProductSpace.rankOne_eq_zero, IsGreatest.nnnorm_cfc, mul_wInner_left, re_eq_norm_of_mul_conj, InnerProductSpace.inner_right_rankOne_apply, HasFDerivWithinAt.hasGradientWithinAt, innerSL_inj, conj_eq_iff_re, cfcₙAux_id, InnerProductSpace.rankOne_eq_rankOne_iff_comm, InnerProductSpace.toDual_apply, conj_I_ax, InnerProductSpace.comp_rankOne, OrthonormalBasis.starProjection_eq_sum_rankOne, InnerProductSpace.toDualMap_apply, ContinuousLinearMap.adjoint_inner_left, InnerProductSpace.AlgebraOfCoalgebra.mul_def, cfcHom_integral, Matrix.l2_opNorm_conjTranspose_mul_self, ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_right, nnnorm_apply_le_nnnorm_cfcₙ, uniqueNonUnitalContinuousFunctionalCalculus, integral_conj, InnerProductSpace.rank_rankOne, IsometricContinuousFunctionalCalculus.toNonUnital, InnerProductSpace.toDual_apply_apply, ContinuousLinearMap.adjointAux_apply, ContinuousLinearMap.inner_map_map_iff_adjoint_comp_self, ProperCone.innerDual_singleton, add_conj, CFC.exp_eq_normedSpace_exp, im_eq_conj_sub, InnerProductSpace.rankOne_def, conj_im_ax, stereoToFun_apply, ContinuousLinearMap.adjointAux_inner_left, inner_self_conj, LinearIsometryEquiv.conjStarAlgEquiv_ext_iff, ContinuousLinearMap.IsStarNormal.ker_adjoint_eq_ker, integrable_cfcₙ, Matrix.l2_opNNNorm_conjTranspose, ClosedSubmodule.orthogonal_eq_inter, conj_div, HasDerivAtFilter.hasGradientAtFilter, Matrix.nonneg_iff_posSemidef, summable_conj, norm_cfcₙ_lt_iff, Commute.cfcₙHom, LinearMap.toMatrixOrthonormal_symm_apply, Matrix.posDef_gram_iff_linearIndependent, LinearMap.toMatrix_innerₛₗ_apply, ContinuousLinearMap.IsStarNormal.adjoint_apply_eq_zero_iff, Matrix.eigenvalues_self_mul_conjTranspose_nonneg, Matrix.l2_opNorm_conjTranspose, LinearMap.isSelfAdjoint_iff', innerSLFlip_apply_apply, InnerProductSpace.enorm_rankOne, Orthonormal.inner_finsupp_eq_sum_right, InnerProductSpace.continuousLinearMapOfBilin_zero, ContinuousLinearMap.toLinearMap_innerSL_apply, LinearMap.IsSymmetric.adjoint_eq, HasGradientAt.hasFDerivAt, Real.fourier_fderiv, ContinuousMap.adjoin_id_eq_span_one_union, HasFDerivWithinAt.norm_sq, Matrix.isHermitian_gram, LinearMap.IsSymmetric.isSymmetric_smul_iff, Matrix.isStrictlyPositive_iff_posDef, Matrix.ofLp_toEuclideanCLM, Filter.Tendsto.cfcₙ, ContinuousLinearMap.toPMap_adjoint_eq_adjoint_toPMap_of_dense, instContinuousStar, ProbabilityTheory.covarianceBilin_eq_covarianceBilinDual, LinearMap.star_eq_adjoint, Matrix.isPositive_toEuclideanLin_iff, nnnorm_cfc_le_iff, Polynomial.aeval_conj, re_eq_add_conj, IsSelfAdjoint.conj_adjoint, wInner_const_left, wInner_cWeight_const_left, hasStrictFDerivAt_norm_sq, LinearMap.adjoint_toSpanSingleton, inner_apply, Matrix.posDef_iff_eq_conjTranspose_mul_self, LinearMap.re_inner_adjoint_mul_self_nonneg, InnerProductSpace.nullSubmodule_le_ker_toDualMap_left, LinearMap.isPositive_self_comp_adjoint, hasSum_conj, ContinuousLinearMap.instStarModuleId, continuous_cfcHomSuperset_left, Continuous.cfc_of_mem_nhdsSet, LinearIsometryEquiv.toLinearEquiv_smul, ContinuousLinearMap.adjointAux_adjointAux, LinearMap.eq_adjoint_iff, cfc_integral, LinearMap.norm_extendTo𝕜'_apply_sq, ContinuousLinearMap.isSelfAdjoint_iff', conj_tsum, Matrix.coe_toEuclideanCLM_eq_toEuclideanLin, wInner_const_right, InnerProductSpace.rankOne_def', ContinuousOn.cfc_of_mem_nhdsSet, ContinuousLinearMap.apply_norm_eq_sqrt_inner_adjoint_left, LinearMap.adjoint_lTensor, conj_eq_iff_real, LinearMap.toMatrixOrthonormal_apply, EuclideanSpace.inner_eq_star_dotProduct, Orthonormal.inner_left_sum, Orientation.inner_mul_areaForm_sub', Matrix.posSemidef_gram, InnerProductSpace.innerSL_norm, hasGradientAt_iff_hasFDerivAt, Matrix.toLin_conjTranspose, instStarModuleReal, Orthonormal.inner_finsupp_eq_sum_left, integrableOn_cfcₙ, norm_cfcₙ_le, continuous_conj, InnerProductSpace.isStarProjection_rankOne_self, spec_cfcₙAux, integrable_cfcₙ', nnnorm_cfc_le, integrable_cfc', LinearMap.instStarModuleId, InnerProductSpace.rankOne_comp_rankOne, nnnorm_apply_le_nnnorm_cfc, Matrix.isHermitian_iff_isSymmetric, Continuous.cfc, InnerProductSpace.rankOne_comp, Real.fourierIntegral_fderiv, InnerProductSpace.toMatrix_rankOne, conj_wInner_symm, InnerProductSpace.isSymmetric_rankOne_self, Commute.cfcHom, Matrix.toEuclideanLin_conjTranspose_eq_adjoint, LinearMap.eq_adjoint_iff_basis, cfc_apply_mem_elemental, nnnorm_cfcₙHom, ContinuousOn.cfcₙ, ContinuousMap.nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom, ContinuousLinearMap.adjoint_toSpanSingleton, nnnorm_conj, cfc_comp_norm, wInner_one_const_right, Commute.cfc, Matrix.posSemidef_iff_eq_sum_vecMulVec, ContinuousOn.cfcₙ_of_mem_nhdsSet, InnerProductSpace.rankOne_one_right_eq_toSpanSingleton, norm_sq_re_conj_add, innerSLFlip_apply, InnerProductSpace.toContinuousLinearMap_toDualMap, IsSelfAdjoint.commute_cfcₙHom, conj_im, conj_I, cfcL_integral, innerSL_apply_norm, InnerProductSpace.toDual_apply_eq_toDualMap_apply, LinearMap.adjoint_inner_left, Matrix.star_dotProduct_gram_mulVec, inv_def, innerSL_real_flip, MeasureTheory.charFun_eq_charFunDual_toDualMap, norm_cfc_le, toMatrix_innerSL_apply, ContinuousLinearMap.orthogonal_range, Continuous.cfcₙ', ContinuousOn.cfc', cfcₙAux_mem_range_inr, ContinuousMap.adjoin_id_eq_span_one_add, ProbabilityTheory.covarianceBilin_map, cfcₙ_norm_sq_nonneg, LinearIsometryEquiv.smul_trans, OrthonormalBasis.toMatrix_orthonormalBasis_mem_unitary, conj_eq_iff_im, ContinuousLinearMap.adjoint_comp, Commute.cfcₙ, InnerProductSpace.toLinearMap_rankOne, ContinuousLinearMap.adjointAux_inner_right, conj_re_ax, ContinuousAt.cfcₙ, nnnorm_cfcₙ_le_iff, Submodule.adjoint_orthogonalProjection, hasFDerivWithinAt_iff_hasGradientWithinAt, LinearMap.adjoint_comp, nnnorm_cfc_lt_iff, LinearMap.isSymmetric_iff_sesqForm, ContinuousLinearMap.IsPositive.adjoint_conj, ContinuousLinearMap.star_eq_adjoint, continuousOn_cfcₙ_setProd, wInner_one_const_left, ProperCone.hyperplane_separation_of_notMem, norm_sq_re_add_conj, innerₛₗ_apply, innerSL_apply, InnerProductSpace.isIdempotentElem_rankOne_self_iff, InnerProductSpaceable.innerProp, conj_inv, LinearIsometryEquiv.symm_units_smul, IsSelfAdjoint.adjoint_conj, OrthonormalBasis.sum_rankOne_eq_id, norm_apply_le_norm_cfc, MeasureTheory.BoundedContinuousFunction.inner_toLp, ContinuousLinearMap.adjoint_inner_right, integrable_cfc, LinearIsometryEquiv.symm_smul_apply, enorm_conj, conjAe_coe, norm_cfcHom, signedDist_apply, EuclideanSpace.inner_toLp_toLp, HasFDerivAt.hasGradientAt, Matrix.instCStarRing, LinearMap.IsSymmetric.conj_inner_sym, ContinuousLinearMap.isAdjointPair_inner, ContinuousMap.ker_evalStarAlgHom_inter_adjoin_id, cfc_setIntegral', OrthonormalBasis.toMatrix_orthonormalBasis_self_mul_conjTranspose, cfcₙ_setIntegral', cfcₙ_apply_mem_elemental, wInner_cWeight_const_right, inv_eq_conj, ContinuousMap.elemental_id_eq_top, LinearMap.eq_adjoint_iff_basis_right, IsSelfAdjoint.commute_cfcₙ, norm_apply_le_norm_cfcₙ, innerₛₗ_apply_coe, OrthonormalBasis.toMatrix_orthonormalBasis_conjTranspose_mul_self, range_cfcHom, AddChar.map_neg_eq_conj, EuclideanSpace.inner_single_right, nnnorm_cfcHom, integrableOn_cfc, continuousOn_cfc, Submodule.orthogonal_eq_inter, normSq_add, LinearMap.IsPositive.adjoint_eq, fderiv_norm_rpow, ContinuousLinearMap.norm_map_iff_adjoint_comp_self, ContinuousLinearMap.norm_adjoint_comp_self, LinearPMap.mem_adjoint_domain_iff, ContinuousMapZero.elemental_eq_top, ContinuousMapZero.adjoin_id_dense, Matrix.l2_opNNNorm_conjTranspose_mul_self, coe_innerₛₗ_apply, HasGradientAt.hasDerivAt, InnerProductSpace.continuousLinearMapOfBilin_apply, Matrix.cstar_norm_def, ContinuousMap.ker_evalStarAlgHom_eq_closure_adjoin_id, conj_eq_re_sub_im, inner_matrix_row_row, cfcₙL_integrable, conj_ofNat, Matrix.instStarOrderedRing, ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_right, innerSL_apply_coe, ContinuousWithinAt.cfc, MeasureTheory.ContinuousMap.inner_toLp, gradient_eq_deriv, LinearMap.toMatrix_adjoint, Matrix.IsStrictlyPositive.posDef, conj_smul, ContinuousLinearMap.isPositive_adjoint_comp_self, LinearMap.im_inner_adjoint_mul_self_eq_zero, nnnorm_cfcₙ_le, norm_innerSL_le, LinearMap.posSemidef_toMatrix_iff, HasGradientWithinAt.hasFDerivWithinAt, hasSum_conj', InnerProductSpace.conj_inner_symm, LinearMap.isAdjointPair_inner, LinearMap.IsPositive.adjoint_conj, range_cfc, LinearIsometryEquiv.toContinuousLinearEquiv_smul, HasGradientAtFilter.hasDerivAtFilter, MeasureTheory.eLpNorm_conj, inner_gradient_right, Real.fourierIntegral_iteratedFDeriv, norm_cfcₙ_le_iff, inner_conj_symm, AddChar.inv_apply_eq_conj, InnerProductSpace.symm_toEuclideanLin_rankOne, ContinuousLinearMap.adjoint_innerSL_apply, normSq_sub, Orthonormal.inner_sum, InnerProductSpaceable.inner_.conj_symm, Matrix.IsHermitian.instContinuousFunctionalCalculus, fderiv_norm_sq_apply, IsSelfAdjoint.commute_cfc, cfcHom_apply_mem_elemental, conj_neg_I, cfc_setIntegral, Matrix.posSemidef_iff_isHermitian_and_spectrum_nonneg, InnerProductSpace.Core.inner_conj_symm, fderiv_norm_sq, Orientation.inner_mul_inner_add_areaForm_mul_areaForm', norm_cfc_lt, ContinuousLinearMap.innerSL_apply_comp, ContinuousLinearMap.toSesqForm_apply_norm_le, LinearMap.adjoint_id, inner_smul_left, InnerProductSpace.nullSubmodule_le_ker_toDualMap_right, cfc_integral', ContinuousLinearMap.adjoint_adjoint, restrict_toContinuousMap_eq_toContinuousMapStar_restrict, inner_matrix_col_col, normSq_conj, ContinuousLinearMap.orthogonal_ker, InnerProductSpace.norm_rankOne, LinearMap.IsPositive.conj_adjoint, cfcₙ_integral', nnnorm_cfcₙ_lt
|
| Name | Category | Theorems |
|---|
instRCLike 📖 | CompOp | 2112 mathmath: Orientation.rightAngleRotationAux₁_rightAngleRotationAux₁, Affine.Simplex.isTangentAt_insphere_iff_eq_touchpoint, hasDerivAt_fourier, RCLike.map_from_real, norm_sub_sq_real, ProbabilityTheory.variance_eq_integral, TemperedDistribution.lineDerivOpCLM_eq, NumberField.mixedEmbedding.fundamentalDomain_integerLattice, Orientation.oangle_sign_smul_add_right, MeasureTheory.Lp.toTemperedDistributionCLM_apply, Orientation.oangle_eq_zero_or_eq_pi_iff_right_eq_smul, TemperedDistribution.fourierInv_toTemperedDistributionCLM_eq, MeasureTheory.Integrable.integral_norm_prod_right, inner_lt_one_iff_real_of_norm_eq_one, MeasureTheory.mulEquivHaarChar_smul_integral_map, EuclideanGeometry.dist_smul_vadd_sq, Bundle.ContMDiffRiemannianMetric.isVonNBounded, real_inner_div_norm_mul_norm_eq_neg_one_iff, Orientation.oangle_ne_zero_and_ne_pi_iff_linearIndependent, Polynomial.mahlerMeasure_def_of_ne_zero, EulerSine.integral_cos_mul_cos_pow, Bundle.ContMDiffRiemannianMetric.contMDiff, continuousOn_stereoToFun, SmoothBumpCovering.toSmoothPartitionOfUnity_eq_mul_prod, ContDiffBump.ae_convolution_tendsto_right_of_locallyIntegrable, MonotoneOn.intervalIntegral_slope_le, ProbabilityTheory.condIndepFun_iff_condExp_inter_preimage_eq_mul, ProbabilityTheory.isGaussian_iff_gaussian_charFun, ProperCone.innerDual_le_innerDual, exists_contMDiffMap_zero_one_of_isClosed, InformationTheory.integral_llr_add_mul_log_nonneg, NumberField.mixedEmbedding.normAtComplexPlaces_mixedSpaceOfRealSpace, MeasureTheory.eLpNorm_condExp_le, mellin_eq_fourier, integral_cos, RCLike.normSq_to_real, SchwartzMap.integral_sesq_fourier_fourier, ProbabilityTheory.condDistrib_ae_eq_condExp, MeasureTheory.charFun_eq_fourierIntegral', hasFDerivAt_fourierChar_neg_bilinear_left, instIsManifoldRealEuclideanSpaceFinModelWithCornersSelfTopWithTopENatElemHAddNatOfNatSphere, real_inner_div_norm_mul_norm_eq_neg_one_of_ne_zero_of_neg_mul, Function.hasTemperateGrowth_inner_right, Isometry.preimage_perpBisector, NumberField.Units.finrank_eq_rank, ValueDistribution.proximity_zero, Affine.Simplex.ExcenterExists.excenter_notMem_affineSpan_face, Affine.Simplex.smul_mongePoint_vsub_circumcenter_eq_sum_vsub, AddDissociated.randomisation, fourierCoeff_tsum_comp_add, Orientation.inner_rotation_pi_div_two_right_smul, tendsto_tsum_div_pow_atTop_integral, Orientation.oangle_add_left_smul_rotation_pi_div_two, fourierIntegral_comp_linearIsometry, fderiv_fourierIntegral, Affine.Simplex.sSameSide_excenter_singleton_point, Affine.Simplex.neg_mul_lt_inner_vsub_altitudeFoot, Manifold.pathELength_eq_lintegral_mfderiv_Ioo, LinearMap.IsSymmetric.restrictScalars, ZSpan.volume_real_fundamentalDomain, Complex.kahler, SchwartzMap.inner_fourier_toL2_eq, Complex.areaForm, SchwartzMap.toLp_fourierTransformInv_eq, finrank_real_complex_fact', hasDerivAt_sigmoid, UnitAddCircle.lintegral_preimage, EuclideanGeometry.Sphere.isDiameter_iff_right_mem_and_midpoint_eq_center, ProbabilityTheory.analyticOn_mgf, fourierIntegralInv_eq', MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul_of_measurable_of_sigmaFinite, Matrix.IsHermitian.det_abs, OpenPartialHomeomorph.contDiff_unitBallBall_symm, ProbabilityTheory.condIndep_iff, deriv_abs, integral_sin_mul_cos₂, Affine.Simplex.finiteDimensional_direction_altitude, ProbabilityTheory.covarianceBilinDual_apply', AffineSubspace.mem_perpBisector_iff_inner_eq_zero', MeasureTheory.charFunDual_apply, Affine.Simplex.circumcenter_map, ProbabilityTheory.hasGaussianLaw_iff_charFunDual_map_eq, norm_add_eq_iff_real, contDiffAt_norm_smul_iff, UnitAddCircle.intervalIntegral_preimage, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_completeFamily_of_ne, intervalIntegral.mul_integral_comp_mul_sub, AnalyticOn.im_ofReal, AbsolutelyContinuousOnInterval.integral_deriv_eq_sub, intervalIntegral.integral_hasFDerivAt_of_tendsto_ae, Polynomial.Chebyshev.integral_measureT_eq_integral_cos, Orientation.linearEquiv_det_rotation, EuclideanGeometry.Sphere.wbtw_secondInter, Orientation.tan_oangle_add_left_smul_rotation_pi_div_two, Affine.Simplex.inv_height_eq_sum_mul_inv_dist, Affine.Simplex.ExcenterExists.excenter_notMem_affineSpan_faceOpposite, EuclideanGeometry.Cospherical.affineIndependent_of_mem_of_ne, fourierIntegral_eq, PeriodPair.basis_one, ProperCone.innerDual_univ, Affine.Simplex.circumcenter_mem_affineSpan, Affine.Simplex.affineSpan_pair_altitudeFoot_eq_altitude, Orientation.kahler_comp_rightAngleRotation', integral_const_on_unit_interval, circleIntegral_def_Icc, integral_exp_mul_Iic, MeasureTheory.submartingale_iff_expected_stoppedValue_mono, Orientation.rotation_eq_self_iff, Affine.Simplex.excenter_singleton_mem_affineSpan_range, ZLattice.covolume_eq_det_inv, Orientation.two_zsmul_oangle_smul_left_of_ne_zero, circleIntegrable_iff, ProbabilityTheory.covarianceBilinDual_apply, InnerProductGeometry.angle_normalize_left, hasFDerivAt_stereoInvFunAux, SchwartzMap.integral_clm_comp_lineDerivOp_right_eq_neg_left, ProbabilityTheory.IsGaussian.map_eq_gaussianReal, MeasureTheory.integral_fintype_prod_volume_eq_pow, fderiv_fourierChar_neg_bilinear_right_apply, ConvexOn.map_set_average_le, real_inner_smul_self_left, intervalIntegral.fderiv_integral_of_tendsto_ae, flip_innerSL_real, LipschitzWith.memLp_lineDeriv, Orientation.volumeForm_robust_neg, AnalyticOnNhd.re_ofReal, SmoothPartitionOfUnity.contMDiffAt_finsum, Affine.Simplex.dist_point_faceOppositeCentroid, differentiableWithinAt_abs_pos, eventually_enorm_mfderivWithin_symm_extChartAt_lt, MeasureTheory.condExpL2_ae_eq_zero_of_ae_eq_zero, LipschitzWith.ae_lineDeriv_sum_eq, SchwartzMap.lineDerivOp_fourier_eq, Orientation.inner_mul_inner_add_areaForm_mul_areaForm, intervalIntegral.measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_right, Orientation.areaForm_le, DifferentiableWithinAt.norm, det_fderivPolarCoordSymm, SmoothPartitionOfUnity.locallyFinite, InnerProductGeometry.sin_angle, EuclideanGeometry.Sphere.mem_orthRadius_iff_inner_right, Affine.Simplex.incenter_map, SchwartzMap.integral_bilin_fourierInv_eq, exists_smooth_one_nhds_of_subset_interior, Orientation.neg_rotation, GaussianFourier.integral_cexp_neg_mul_sq_norm, ProbabilityTheory.covarianceBilin_apply_eq_cov, ProbabilityTheory.covarianceBilin_self, AffineSubspace.left_mem_perpBisector, NumberField.mixedEmbedding.fundamentalCone.abs_det_completeBasis_equivFunL_symm, EuclideanGeometry.preimage_inversion_perpBisector_inversion, Affine.Triangle.sSameSide_affineSpan_pair_point_incenter, SmoothPartitionOfUnity.nonneg, Orientation.eq_rotation_self_iff_angle_eq_zero, hasDerivAt_bernoulliFun, Orientation.volumeForm_neg_orientation, ProbabilityTheory.sum_prob_mem_Ioc_le, Complex.betaIntegral_scaled, MeasureTheory.pdf.integral_mul_eq_integral, GaussianFourier.integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace, ProbabilityTheory.uncenteredCovarianceBilin_apply, InnerProductGeometry.angle_smul_right_of_pos, TemperedDistribution.lineDerivOp_fourier_eq, MeasureTheory.charFun_neg, contMDiff_neg_sphere, not_differentiableAt_norm_zero, ProbabilityTheory.hasDerivAt_integral_pow_mul_exp, circleAverage_log_norm_sub_const₁, BoxIntegral.unitPartition.mem_smul_span_iff, exists_eq_const_mul_intervalIntegral_of_nonneg, ContDiffBump.integral_normed, MeasureTheory.integral_fintype_prod_eq_prod, NumberField.mixedEmbedding.fundamentalCone.completeBasis_apply_of_ne, SmoothBumpCovering.exists_immersion_euclidean, IsOpen.exists_msmooth_support_eq, Affine.Triangle.sbtw_touchpoint_singleton, Affine.Triangle.dist_point_faceOppositeCentroid, IsOpen.exists_smooth_support_eq, SmoothPartitionOfUnity.locallyFinite', rpow_eq_const_mul_integral, interval_average_eq_div, Bundle.RiemannianMetric.isVonNBounded, Orientation.tan_oangle_add_right_smul_rotation_pi_div_two, Affine.Simplex.mem_circumsphere, ProbabilityTheory.setIntegral_condCDF, integral_pow, fourierIntegral_gaussian_innerProductSpace', MeasureTheory.charFun_toDual_symm_eq_charFunDual, EuclideanGeometry.Sphere.mem_commonExtTangents_iff, InnerProductSpace.canonicalCovariantTensor_eq_sum, fourier_gaussian_pi', MeasureTheory.charFun_eq_fourierIntegral, Matrix.PosSemidef.sqrt_eq_zero_iff, ProbabilityTheory.integral_continuousLinearMap_gaussianReal, integral_log_sin_zero_pi_div_two, lintegral_fderiv_lineMap_eq_edist, EuclideanGeometry.oangle_sign_eq_zero_iff_collinear, exists_eq_interval_average_of_noAtoms, MeasureTheory.Measure.addHaarScalarFactor_eq_integral_div, ConvexOn.set_average_mem_epigraph, OrthonormalBasis.det_eq_neg_det_of_opposite_orientation, StrictConcaveOn.ae_eq_const_or_lt_map_average, norm_add_pow_two_real, intervalIntegral.integral_ofReal, ProbabilityTheory.hasGaussianLaw_iff_charFun_map_eq, MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul, OrthonormalBasis.det_to_matrix_orthonormalBasis_of_opposite_orientation, GaussianFourier.integral_cexp_neg_mul_sq_norm_add, ContDiffOn.inner, integral_exp, integral_inv_of_pos, Affine.Simplex.sign_signedInfDist_lineMap_incenter_touchpoint, Module.Basis.parallelepiped_basisFun, SchwartzMap.laplacianCLM_eq, MeasureTheory.hasFiniteIntegral_prod_iff', Affine.Simplex.ExcenterExists.affineCombination_eq_excenter_iff, vector_fourierIntegral_eq_integral_exp_smul, UnitAddTorus.mFourierSubalgebra_closure_eq_top, fourier_real_eq_integral_exp_smul, EuclideanGeometry.Sphere.mem_tangentsFrom_iff, ProbabilityTheory.covarianceOperator_apply, InnerProductGeometry.angle_smul_left_of_neg, ProbabilityTheory.cdf_paretoMeasure_eq_integral, InnerProductGeometry.angle_normalize_right, differentiableWithinAt_abs, inner_lt_norm_mul_iff_real, LocallyBoundedVariationOn.ae_differentiableWithinAt, integral_sin_pow_three, hasFPowerSeriesOnBall_ofScalars_mul_add_zero, instIsManifoldRealEuclideanSpaceFinOfNatNatEuclideanHalfSpaceModelWithCornersEuclideanHalfSpaceElemIcc, circleAverage_log_norm_sub_const_of_mem_closedBall, hasStrictDerivAt_abs_pos, hasDerivWithinAt_abs_pos, EuclideanGeometry.Sphere.mem_commonTangents_iff, ProbabilityTheory.IsRatCondKernelCDF.setIntegral, analyticOnNhd_circleMap, tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support, antideriv_bernoulliFun, NumberField.mixedEmbedding.commMap_apply_of_isComplex, differentiableAt_sigmoid, Affine.Simplex.excenterWeightsUnnorm_reindex, ProbabilityTheory.IsCondKernelCDF.integral, intervalIntegral.integral_mono_on, Orientation.oangle_smul_left_of_neg, abs_setIntegral_mulExpNegMulSq_comp_sub_le_mul_measure, MeasureTheory.L2.inner_def, Orientation.volumeForm_map, Icc_isBoundaryPoint_bot, OrthonormalBasis.sum_sq_inner_right, Polynomial.Chebyshev.integral_T_real_mul_self_measureT_of_ne_zero, deriv_abs_neg, ProbabilityTheory.moment_one, integral_exp_neg_mul_rpow, MeasureTheory.BorelCantelli.martingalePart_process_ae_eq, Complex.toBasis_orthonormalBasisOneI, Homeomorph.contDiff_unitBall, OrthonormalBasis.toBasis_adjustToOrientation, Polynomial.Chebyshev.integral_measureT, intervalIntegral.integral_div, integral_sin_pow_pos, Affine.Triangle.orthocenter_eq_smul_vsub_vadd_circumcenter, EuclideanGeometry.inversion_mem_perpBisector_inversion_iff', Affine.Simplex.ExcenterExists.touchpoint_map, Orientation.inner_rightAngleRotation_swap', EuclideanGeometry.angle_eq_iff_oangle_eq_or_wbtw, Complex.integral_rpow_mul_exp_neg_rpow, OrthonormalBasis.measurePreserving_repr, InformationTheory.leftDeriv_klFun_one, integral_Ioi_rpow_of_lt, SchwartzMap.integral_fourierInv_smul_eq, exists_smooth_tsupport_subset, MeasureTheory.withDensityᵥ_eq_withDensity_pos_part_sub_withDensity_neg_part, signedDist_triangle, SchwartzMap.inner_toL2_toL2_eq, tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_integrableOn, EuclideanGeometry.dist_eq_iff_eq_smul_rotation_pi_div_two_vadd_midpoint, ProbabilityTheory.gammaCDFReal_eq_integral, integral_bernoulliFun, Complex.coe_orthonormalBasisOneI, LocallyBoundedVariationOn.ae_differentiableAt, MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_det_fderiv_mul, MonotoneOn.intervalIntegrable_deriv, MeasureTheory.AEStronglyMeasurable.ae_integrable_condKernel_iff, Icc_mem_vitaliFamily_at_left, Orientation.abs_volumeForm_apply_of_orthonormal, ContDiffBump.normed_def, signedDist_linear_apply_apply, Affine.Simplex.sSameSide_incenter_point, EuclideanGeometry.collinear_iff_of_two_zsmul_oangle_eq, setIntegral_Ioi_zero_rpow, SchwartzMap.integral_bilin_fourierIntegral_eq, fourier_gaussian_innerProductSpace, EuclideanGeometry.oangle_midpoint_right, Affine.Simplex.ExcenterExists.excenter_map, integral_rpow_mul_exp_neg_rpow, SchwartzMap.toLp_fourierInv_eq, NumberField.mixedEmbedding.negAt_apply_snd, MeasureTheory.measure_lt_one_eq_integral_div_gamma, MeasureTheory.setIntegral_prod_mul, Orientation.neg_rotation_neg_pi_div_two, one_add_rpow_hasFPowerSeriesOnBall_zero, Polynomial.Chebyshev.integral_measureT_eq_integral_cos_of_continuous, VectorFourier.fourierPowSMulRight_eq_comp, MeasureTheory.charFunDual_eq_charFun_map_one, MeasureTheory.integral_fintype_prod_eq_pow, MeasureTheory.charFun_apply, mfderivWithin_projIcc_one, intervalIntegral.integral_pos_iff_support_of_nonneg_ae', integral_cos_pow, Orientation.oangle_sign_sub_smul_left, AnalyticAt.harmonicAt_im, ProbabilityTheory.integral_stieltjesOfMeasurableRat, Affine.Simplex.ExcenterExists.touchpoint_notMem_affineSpan_of_ne, norm_sub_pow_two_real, EuclideanGeometry.Sphere.isTangentAt_of_dist_sq_eq_power, Affine.Simplex.abs_inner_vsub_altitudeFoot_div_lt_one, MeasureTheory.Measure.integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport, Orientation.rightAngleRotation_def, EuclideanGeometry.angle_eq_zero_iff_eq_and_ne_or_sbtw, ProbabilityTheory.IndepFun.integral_comp_mul_comp, Function.HasTemperateGrowth.toTemperedDistribution_apply, Euclidean.closedBall_eq_image, Affine.Simplex.touchpoint_singleton_mem_interior_faceOpposite, MeasureTheory.Measure.integral_isMulLeftInvariant_isMulRightInvariant_combo, NumberField.mixedEmbedding.negAt_preimage, InformationTheory.not_differentiableWithinAt_klFun_Iio_zero, Complex.hasDerivAt_GammaIntegral, Affine.Simplex.excenterExists_reindex, SchwartzMap.integral_sesq_fourier_eq, EuclideanGeometry.Sphere.secondInter_collinear, fderiv_fourier, intervalIntegral.integral_mono_ae_restrict, NumberField.mixedEmbedding.iUnion_negAt_plusPart_ae, BoxIntegral.unitPartition.integralSum_eq_tsum_div, InformationTheory.toReal_klDiv_eq_integral_klFun, Quaternion.linearIsometryEquivTuple_symm_apply, Affine.Simplex.ninePointCircle_eq_circumsphere_medial, Probability.integral_cauchyPDFReal, intervalIntegral.hasFDerivAt_integral_of_dominated_loc_of_lip, MeasureTheory.SignedMeasure.singularPart_smul, ProbabilityTheory.covarianceBilin_apply_basisFun_self, MeasureTheory.charFun_apply_real, Orientation.areaForm_to_volumeForm, stereoInvFunAux_apply, Icc_isInteriorPoint_interior, fourierCoeff_bernoulli_eq, circleAverage_log_norm_sub_const_eq_log_radius_add_posLog, GaussianFourier.integrable_cexp_neg_mul_sq_norm_add_of_euclideanSpace, signedDist_le_dist, EuclideanGeometry.Sphere.IsTangentAt.mem_space, Affine.Simplex.circumcenter_reindex, OpenPartialHomeomorph.contDiff_univUnitBall, EulerSine.integral_cos_mul_cos_pow_aux, SchwartzMap.fourier_lineDerivOp_eq, EuclideanGeometry.affineSpan_of_orthocentricSystem, TemperedDistribution.instLineDerivLeftSMulReal, AffineSubspace.mem_perpBisector_iff_inner_eq_zero, Orientation.areaForm_neg_orientation, EuclideanGeometry.inversion_vsub_center, Orientation.rightAngleRotation_trans_rightAngleRotation, Function.Periodic.sInf_add_zsmul_le_integral_of_pos, NumberField.mixedEmbedding.stdBasis_apply_isComplex_snd, Monotone.ae_differentiableAt, ProbabilityTheory.iCondIndep_iff, ProbabilityTheory.centralMoment_one', MeasureTheory.integral_fin_nat_prod_volume_eq_prod, TemperedDistribution.fourierInv_lineDerivOp_eq, MeasureTheory.condExpL2_indicator_ae_eq_smul, Affine.Simplex.excenter_eq_affineCombination, mfderivWithin_comp_projIcc_one, ProbabilityTheory.iCondIndepFun_iff_condExp_inter_preimage_eq_mul, Affine.Triangle.dist_div_sin_angle_eq_two_mul_circumradius, SimpleGraph.lapMatrix_toLinearMap₂'_apply'_eq_zero_iff_forall_reachable, NumberField.mixedEmbedding.negAt_signSet_apply_isComplex, SmoothPartitionOfUnity.sum_finsupport', ProbabilityTheory.variance_le_sub_mul_sub, abs_real_inner_le_norm, EuclideanGeometry.Sphere.commonIntTangents_union_commonExtTangents, ContDiffBump.measure_closedBall_div_le_integral, Orientation.kahler_eq_zero_iff, Orientation.oangle_sign_sub_smul_right, ProperCone.innerDual_sUnion, AffineSubspace.perpBisector_nonempty, signedDist_apply_apply, integral_sin_sq, SchwartzMap.integral_norm_sq_fourier, norm_add_eq_sqrt_iff_real_inner_eq_zero, Orientation.oangle_smul_left_self_of_nonneg, Affine.Simplex.altitudeFoot_mem_affineSpan_image_compl, UnitAddTorus.mFourierCoeff_toLp, ProbabilityTheory.gaussianReal_map_continuousLinearMap, Manifold.pathELength_def, EuclideanSpace.volume_closedBall_fin_three, IccLeftChart_extend_interior_pos, Orientation.areaForm_swap, NumberField.mixedEmbedding.euclidean.stdOrthonormalBasis_map_eq, real_inner_mul_inner_self_le, ProbabilityTheory.covarianceOperator_zero, Bundle.ContinuousRiemannianMetric.symm, integral_exp_mul_complex_Ioi, LinearIsometryEquiv.measurePreserving, MeasureTheory.SignedMeasure.withDensityᵥ_rnDeriv_eq, setIntegral_Ioi_zero_cpow, Affine.Simplex.finrank_direction_altitude, InformationTheory.tendsto_rightDeriv_klFun_atTop, TemperedDistribution.instFourierAdd, intervalIntegral.integral_mono, Complex.sameRay_of_arg_eq, MeasureTheory.Integrable.integral_norm_condDistrib_map, NumberField.mixedEmbedding.normAtComplexPlaces_polarSpaceCoord_symm, MeasureTheory.ComplexMeasure.singularPart_add_withDensity_rnDeriv_eq, hasDerivAt_abs_neg, Affine.Simplex.mongePoint_mem_mongePlane, Orientation.kahler_swap, Orientation.det_rotation, Orientation.rotation_pi_apply, intervalIntegral.integral_mono_interval, norm_sub_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero, Affine.Simplex.isTangentAt_insphere_touchpoint, Orientation.rotation_rotation, MeasureTheory.condExp_smul_of_aestronglyMeasurable_right, Affine.Simplex.excenterWeightsUnnorm_map, EuclideanGeometry.Sphere.IsExtTangentAt.wbtw, Matrix.PosSemidef.det_sqrt, TemperedDistribution.instFourierSMul, instIsContinuousRiemannianBundleTrivial, DifferentiableWithinAt.dist, hasDerivWithinAt_abs, contDiff_circleMap, Affine.Simplex.ExcenterExists.affineSpan_faceOpposite_eq_orthRadius, intervalIntegral.integral_mono_on_of_le_Ioo, eventually_norm_mfderivWithin_symm_extChartAt_lt, ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_integral_of_antitone, NumberField.mixedEmbedding.fundamentalCone.logMap_expMapBasis, Affine.Simplex.inner_mongePoint_vsub_face_centroid_vsub, BoundedVariationOn.intervalIntegrable_deriv, Orientation.volumeForm_def, ProbabilityTheory.Kernel.setIntegral_densityProcess_of_mem, VectorFourier.hasFDerivAt_fourierIntegral, MeasureTheory.Integrable.tendsto_eLpNorm_condExp, MeasureTheory.convolution_precompR_apply, ProbabilityTheory.condIndepSets_singleton_iff, VectorFourier.fourierIntegral_iteratedFDeriv, MonotoneOn.sum_le_integral, InformationTheory.hasDerivAt_klFun, MeasureTheory.setIntegral_condExpL2_indicator, contMDiff_coe_sphere, integral_cos_pow_aux, ProbabilityTheory.isPosSemidef_covarianceBilin, stereographic_apply_neg, intervalIntegral.abs_intervalIntegral_eq, Orientation.kahler_comp_rightAngleRotation, InformationTheory.toReal_klDiv, TemperedDistribution.instFourierPairInv, EuclideanGeometry.oangle_eq_pi_iff_sbtw, TemperedDistribution.instFourierPair, ae_differentiableAt_norm, IsOpen.exists_contMDiff_support_eq_aux, TemperedDistribution.delta_apply, NumberField.Units.instZLattice_unitLattice, Manifold.pathELength_eq_lintegral_mfderivWithin_Icc, Affine.Simplex.circumcenter_eq_affineCombination_of_pointsWithCircumcenter, MeasureTheory.BorelCantelli.predictablePart_process_ae_eq, ProbabilityTheory.iIndepSet.condExp_indicator_filtrationOfSet_ae_eq, ProbabilityTheory.tendsto_integral_truncation, Orientation.volumeForm_zero_pos, ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_mgf', fourierIntegral_gaussian_pi, ProbabilityTheory.uncenteredCovarianceBilinDual_of_not_memLp, Bundle.ContinuousRiemannianMetric.continuous, ProbabilityTheory.complexMGF_mul_I, Affine.Simplex.affineSpan_faceOpposite_eq_orthRadius_insphere, SchwartzMap.laplacianCLM_eq', MeasureTheory.condExp_mul_of_aestronglyMeasurable_right, integral_exp_mul_complex, EuclideanGeometry.Sphere.orthRadius_center, NumberField.Units.span_basisOfIsMaxRank, instIsManifoldRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle, SmoothBumpCovering.toSmoothPartitionOfUnity_apply, VectorFourier.norm_iteratedFDeriv_fourierPowSMulRight, ProbabilityTheory.Kernel.martingale_densityProcess, range_stereographic_symm, Complex.GammaIntegral_ofReal, TemperedDistribution.instContinuousFourier, mellinInv_eq_fourierIntegralInv, MonotoneOn.integral_le_sum_Ico, PiLp.volume_preserving_toLp, InnerProductGeometry.norm_toLp_symm_crossProduct, SmoothPartitionOfUnity.contDiffAt_finsum, intervalIntegral.intervalIntegral_pos_of_pos, isOpenEmbedding_stereographic_symm, Chebyshev.integral_one_div_log_sq_isBigO, MeasureTheory.charFun_eq_prod_iff, NumberField.Units.basisOfIsMaxRank_apply, EuclideanGeometry.Sphere.coe_secondInter, Orientation.measure_eq_volume, Complex.integral_exp_neg_rpow, MeasureTheory.SignedMeasure.absolutelyContinuous_iff_withDensityᵥ_rnDeriv_eq, PeriodPair.basis_zero, ProbabilityTheory.analyticAt_mgf, NumberField.mixedEmbedding.negAt_signSet_apply_isReal, Matrix.PosSemidef.posSemidef_sqrt, orthonormalBasis_one_dim, Seminorm.gaugeSeminorm_ball, integral_le_sum_mul_Ico_of_antitone_monotone, LipschitzWith.ae_lineDifferentiableAt, EuclideanGeometry.oangle_midpoint_rev_left, InformationTheory.leftDeriv_klFun, integral_bernoulliFun_eq_zero, Affine.Triangle.touchpoint_singleton_sbtw, MeasureTheory.Integrable.tendsto_ae_condExp, Orientation.rotation_symm, EuclideanGeometry.Sphere.isTangent_iff_isTangentAt_orthogonalProjection, NumberField.mixedEmbedding.fundamentalDomain_idealLattice, Affine.Simplex.exradius_map, MeasureTheory.Integrable.integral_norm_comp, ProbabilityTheory.differentiableAt_mgf, Orientation.oangle_eq_zero_iff_sameRay, Complex.orthonormalBasisOneI_repr_apply, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_completeFamily_of_eq, analyticOn_log, Affine.Triangle.dist_circumcenter_reflection_orthocenter, analyticOnNhd_log, Orientation.angle_eq_iff_oangle_eq_or_sameRay, fourierIntegralInv_comp_linearIsometry, Affine.Simplex.ExcenterExists.sign_signedInfDist_touchpoint, ProbabilityTheory.iteratedDeriv_mgf, SchwartzMap.delta_apply, InnerProductGeometry.angle_eq_zero_iff, Affine.Simplex.abs_inner_vsub_altitudeFoot_lt_mul, ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_mgf, SchwartzMap.norm_fourier_toL2_eq, norm_cauchyPowerSeries_le, Orientation.rotation_map, ProbabilityTheory.Kernel.setIntegral_densityProcess_of_le, Orientation.oangle_rotation_left, one_div_one_sub_sq_hasFPowerSeriesOnBall_zero, SchwartzMap.instFourierPair, hasFDerivAt_norm_rpow, mellinInv_eq_fourierInv, ProperCone.innerDual_zero, Affine.Simplex.excenterWeights_reindex, EuclideanGeometry.collinear_of_angle_eq_zero, Metric.exists_smooth_forall_closedBall_subset, EuclideanGeometry.Sphere.tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center, instLieGroupRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle, fourier_gaussian_innerProductSpace', InnerProductGeometry.cos_angle, ContDiffBump.convolution_tendsto_right, RCLike.im_to_real, fourier_real_eq, Affine.Simplex.ExcenterExists.isTangentAt_touchpoint, intervalIntegral.integral_lt_integral_of_continuousOn_of_le_of_exists_lt, Affine.Simplex.inradius_reindex, hasDerivAt_abs_rpow, EuclideanGeometry.preimage_inversion_perpBisector, NumberField.mixedEmbedding.mem_span_fractionalIdealLatticeBasis, integral_cpow, ZSpan.volume_fundamentalDomain, ProbabilityTheory.iteratedDeriv_complexMGF, ProbabilityTheory.covarianceBilin_zero, tendsto_integral_gaussian_smul', contDiffOn_stereoToFun, hasFDerivAt_fourier, VectorFourier.differentiable_fourierIntegral, Affine.Simplex.incenter_mem_interior, Affine.Simplex.mongePoint_eq_affineCombination_of_pointsWithCircumcenter, MeasureTheory.condExp_mul_of_stronglyMeasurable_right, Affine.Simplex.altitudeFoot_map, analyticOnNhd_sigmoid, Matrix.PosSemidef.sqrt_eq_one_iff, ProbabilityTheory.integral_truncation_eq_intervalIntegral, ProbabilityTheory.condExpKernel_ae_eq_condExp', deriv_Gamma_nat, real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two, LogDeriv_exp, stereoInvFun_apply, Isometry.mapsTo_perpBisector, EuclideanGeometry.Cospherical.affineIndependent_of_ne, Affine.Simplex.circumcenter_eq_point, fourierIntegral_convergent_iff', Matrix.PosSemidef.sqrt_sq, InnerProductGeometry.cos_angle_mul_norm_mul_norm, Bundle.ContMDiffRiemannianMetric.symm, fourier_comp_linearIsometry, MeasureTheory.integral_comap_eq_addEquivAddHaarChar_smul, LSeries_eq_mul_integral_of_nonneg, ProbabilityTheory.analyticOnNhd_cgf, real_inner_div_norm_mul_norm_eq_one_iff, MeasureTheory.lintegral_nnnorm_condExpL2_le, SmoothPartitionOfUnity.le_one, EuclideanGeometry.oangle_eq_zero_iff_wbtw, Monotone.ae_hasDerivAt, ProbabilityTheory.IsCondKernelCDF.setIntegral, SchwartzMap.norm_fourierTransformCLM_toL2_eq, EuclideanSpace.volume_closedBall_fin_two, LinearIsometryEquiv.coe_toMeasurableEquiv, Affine.Simplex.signedInfDist_apply_self, VectorFourier.iteratedFDeriv_fourierIntegral, exists_contMDiffMap_zero_one_nhds_of_isClosed, ProbabilityTheory.HasCondSubgaussianMGF.ae_condExp_le, one_div_one_sub_hasFPowerSeriesOnBall_zero, ContDiffBump.normed_convolution_eq_right, ProbabilityTheory.gaussianReal_map_linearMap, norm_sub_eq_sqrt_iff_real_inner_eq_zero, HasDerivWithinAt.inner, AbsolutelyContinuousOnInterval.integral_deriv_mul_eq_sub, BoxIntegral.integral_nonneg, DifferentiableAt.inner, differentiable_fourierIntegral, IntervalIntegrable.absolutelyContinuousOnInterval_intervalIntegral, NumberField.mixedEmbedding.fundamentalCone.prod_deriv_expMap_single, fourierInv_comp_linearIsometry, MeasureTheory.hasFDerivAt_convolution_right_with_param, ProbabilityTheory.IsGaussian.charFun_eq', ProbabilityTheory.covarianceBilinDual_eq_covariance, Matrix.PosSemidef.eq_sqrt_iff_sq_eq, signedDist_zero, LinearIsometryEquiv.reflections_generate, AffineSubspace.signedInfDist_eq_signedDist_orthogonalProjection, EulerSine.sin_pi_mul_eq, integral_exp_Iic, Chebyshev.primeCounting_eq_theta_div_log_add_integral, UnitAddCircle.measure_univ, integral_mul_cexp_neg_mul_sq, MeasureTheory.integrable_comp, NumberField.mixedEmbedding.span_idealLatticeBasis, NumberField.mixedEmbedding.fundamentalCone.norm_expMapBasis, InformationTheory.integral_llr_add_sub_measure_univ_nonneg, MeasureTheory.Integrable.integral_norm_prod_left, HasCompactSupport.hasFDerivAt_convolution_right, frontier_range_modelWithCornersEuclideanHalfSpace, SchwartzMap.integral_bilinear_deriv_right_eq_neg_left, MeasureTheory.condExp_stronglyMeasurable_simpleFunc_mul, ProbabilityTheory.covarianceBilinDual_zero, Affine.Simplex.ExcenterExists.sOppSide_excenter_point_iff, contDiff_bernoulliFun, Affine.Simplex.incenter_notMem_affineSpan_face, HasFDerivWithinAt.inner, EuclideanSpace.instIsManifoldSphere, Affine.Triangle.affineSpan_pair_eq_orthRadius, MeasureTheory.tendsto_sum_indicator_atTop_iff, circleAverage_log_norm_sub_const₀, Orientation.oangle_rotation_oangle_right, ProbabilityTheory.condIndepSet_iff, MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul_of_measurable, ProbabilityTheory.differentiableOn_mgf, contDiffOn_abs, MeasureTheory.Integrable.integral_norm_condExpKernel, EuclideanGeometry.image_inversion_perpBisector, innerₗ_apply, SmoothBumpFunction.contMDiffAt, Orientation.rightAngleRotation_symm, Affine.Simplex.mongePlane_def, Affine.Triangle.acuteAngled_iff_angle_lt, ProbabilityTheory.complexMGF_id_mul_I, one_div_sub_hasFPowerSeriesOnBall_zero, ContDiff.euclidean_dist, MeasureTheory.lpMeasToLpTrimLie_symm_indicator, MeasureTheory.condExp_mul_of_aestronglyMeasurable_left, MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_det_fderiv_mul, Bundle.ContMDiffRiemannianMetric.pos, ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_cgf', signedDist_triangle_left, TemperedDistribution.fourier_toTemperedDistributionCLM_eq, IsContMDiffRiemannianBundle.exists_contMDiff, sum_Ico_le_integral_of_le, Affine.Simplex.excenterExists_map, integral_sin_pow_mul_cos_pow_odd, integral_rpow_mul_exp_neg_mul_rpow, SmoothBumpCovering.sum_toSmoothPartitionOfUnity_eq, ProbabilityTheory.integral_gaussianPDFReal_eq_one, Affine.Simplex.vectorSpan_isOrtho_altitude_direction, integral_exp_mul_I_eq_sinc, contMDiff_subtype_coe_Icc, Orientation.inner_rotation_pi_div_two_right, Affine.Simplex.exsphere_reindex, ProperCone.innerDual_singleton, NumberField.mixedEmbedding.fundamentalCone.completeBasis_apply_of_eq, InformationTheory.integral_klFun_rnDeriv, differentiable_inner, intervalIntegral.abs_integral_mono_interval, OrthonormalBasis.volume_parallelepiped, hasFDerivAt_integral_of_dominated_loc_of_lip', integral_id, Affine.Simplex.altitudeFoot_mem_affineSpan, Orientation.oangle_rotation, ExistsContDiffBumpBase.u_int_pos, SchwartzMap.integral_mul_laplacian_right_eq_left, MeasureTheory.charFun_pi, stereoToFun_apply, SchwartzMap.convolution_apply, differentiableAt_Gamma, orthogonalBilin_innerₗ, NumberField.mixedEmbedding.mem_span_latticeBasis, ProbabilityTheory.evariance_eq_lintegral_ofReal, TemperedDistribution.fourierTransformInv_toTemperedDistributionCLM_eq, ProbabilityTheory.integral_condVar_add_variance_condExp, ContDiffWithinAt.norm_sq, Function.hasTemperateGrowth_norm_sq, BoundedContinuousFunction.innerProbChar_apply, ProbabilityTheory.analyticOn_cgf, zero_at_infty_fourierIntegral, ProbabilityTheory.covarianceBilin_comm, intervalIntegral.integral_congr_codiscreteWithin, ProbabilityTheory.Kernel.tendsto_integral_density_of_monotone, Orientation.inner_rotation_pi_div_two_left, SchwartzMap.integral_bilin_fourier_eq, InformationTheory.klDiv_of_ac_of_integrable, gradient_eq_deriv', Orientation.oangle_rotation_self_left, Orientation.kahler_neg_orientation, EuclideanGeometry.inner_pos_or_eq_of_dist_le_radius, MeasureTheory.L2.integral_inner_eq_sq_eLpNorm, MonotoneOn.intervalIntegrable_slope, real_inner_self_nonneg, Affine.Triangle.circumsphere_eq_of_dist_of_oangle, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed, SchwartzMap.fourierInv_apply_eq, SchwartzMap.smulRightCLM_apply_apply, differentiableOn_Gamma_Ioi, ProbabilityTheory.analyticAt_cgf, InformationTheory.klDiv_def, MeasureTheory.L2.inner_indicatorConstLp_one, RCLike.abs_wInner_le, EuclideanGeometry.image_inversion_sphere_dist_center, InnerProductSpace.volume_ball, NumberField.mixedEmbedding.negAt_apply_isReal_and_notMem, fderiv_norm_smul_neg, SchwartzMap.toTemperedDistributionCLM_apply_apply, integrableOn_Ioi_deriv_ofReal_cpow, ExistsContDiffBumpBase.u_exists, EuclideanGeometry.Sphere.sbtw_secondInter, fourierIntegral_real_eq_integral_exp_smul, deriv_fourierIntegral, integral_exp_mul_I_eq_sin, InnerProductGeometry.inner_eq_neg_mul_norm_of_angle_eq_pi, Orientation.oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero, NumberField.Units.dirichletUnitTheorem.unitLattice_span_eq_top, Affine.Triangle.sOppSide_affineSpan_pair_excenter_singleton_point, intervalIntegral.integral_eq_zero_iff_of_le_of_nonneg_ae, dense_differentiableAt_norm, Orientation.inner_eq_norm_mul_norm_mul_cos_oangle, AntitoneOn.sum_le_integral_Ico, NumberField.mixedEmbedding.fundamentalCone.expMap_basis_of_eq, intervalIntegral.integral_hasStrictFDerivAt_of_tendsto_ae, ContDiff.norm_sq, MonotoneOn.intervalIntegral_deriv_mem_uIcc, NumberField.mixedEmbedding.volume_preserving_negAt, Affine.Simplex.ExcenterExists.sign_signedInfDist_lineMap_excenter_touchpoint, SmoothPartitionOfUnity.sum_eq_one', OrthonormalBasis.sum_sq_inner_left, RCLike.sqrt_real, integral_sin_mul_cos₁, MeasureTheory.Measure.withDensityᵥ_absolutelyContinuous, Orientation.rightAngleRotation_map', EuclideanGeometry.oangle_midpoint_left, ProbabilityTheory.iCondIndepSets_singleton_iff, NumberField.mixedEmbedding.negAt_apply_isComplex, integral_rpowIntegrand₀₁_one_pos, ProbabilityTheory.hasFiniteIntegral_compProd_iff', ProbabilityTheory.isGaussian_iff_charFun_eq, Orientation.inner_rotation_pi_div_two_left_smul, InnerProductGeometry.inner_eq_neg_mul_norm_iff_angle_eq_pi, ProbabilityTheory.integral_truncation_eq_intervalIntegral_of_nonneg, fourierIntegral_eq_half_sub_half_period_translate, RCLike.re_to_real, Affine.Simplex.circumsphere_unique_dist_eq, integral_sin_pow_aux, integral_comp_abs, ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat, integral_div_sq_add_sq, Polynomial.rootSet_derivative_subset_convexHull_rootSet, LineDeriv.laplacianCLM_eq_sum, SmoothPartitionOfUnity.mem_finsupport, Continuous.inner_bundle, Wallis.W_eq_integral_sin_pow_div_integral_sin_pow, EuclideanGeometry.preimage_inversion_sphere_dist_center, has_antideriv_at_fourier_neg, IsOpen.exists_contMDiff_support_eq, UnitAddTorus.mFourier_norm, Orientation.rotation_neg_orientation_eq_neg, ProbabilityTheory.IndepFun.integral_fun_mul_eq_mul_integral, Matrix.instNonnegSpectrumClass, Orientation.eq_rotation_self_iff, NumberField.mixedEmbedding.normAtComplexPlaces_normAtAllPlaces, DifferentiableAt.norm_sq, ProbabilityTheory.sum_variance_truncation_le, Orientation.areaForm'_apply, inner_eq_norm_sq_left_iff, MeasureTheory.condExp_stronglyMeasurable_mul_of_bound, Affine.Triangle.dist_orthocenter_reflection_circumcenter, hasSum_one_div_nat_pow_mul_cos, signedDist_smul_of_pos, IsContinuousRiemannianBundle.exists_continuous, contDiff_fourierIntegral, Affine.Simplex.exradius_reindex, MonotoneOn.sum_le_integral_Ico, Affine.Simplex.ninePointCircle_reindex, ProbabilityTheory.condExp_set_generateFrom_singleton, Orientation.inner_comp_rightAngleRotation, intervalIntegral.integral_hasStrictFDerivAt, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_apply, signedDist_lineMap_lineMap, mfderiv_coe_sphere_injective, ProbabilityTheory.variance_eq_sub, Affine.Triangle.dist_div_sin_oangle_eq_two_mul_circumradius, NumberField.mixedEmbedding.mem_negAt_plusPart_of_mem, NumberField.Units.regOfFamily_of_isMaxRank, intervalIntegral.inv_mul_integral_comp_add_div, inner_map_complex, analyticAt_sigmoid, contDiffAt_norm, tendsto_integral_mul_one_add_inv_smul_sq_pow, MeasureTheory.charFun_conv, AnalyticOnNhd.circleAverage_log_norm_of_ne_zero, PiLp.volume_preserving_ofLp, integral_sin_pow_even_mul_cos_pow_even, ProbabilityTheory.Kernel.setIntegral_density_of_measurableSet, signedDist_vadd_left_swap, OpenPartialHomeomorph.contDiffOn_univUnitBall_symm, MeasureTheory.integrable_prod_iff, Polynomial.eq_centerMass_of_eval_derivative_eq_zero, sum_mul_Ico_le_integral_of_monotone_antitone, Complex.restrictScalars_one_smulRight, ProbabilityTheory.meas_ge_le_variance_div_sq, differentiableAt_abs_neg, real_inner_self_abs, Orientation.oangle_eq_iff_eq_pos_smul_rotation_or_eq_zero, hasDerivAt_fourier_neg, Orientation.rotation_zero, ProbabilityTheory.isGaussian_gaussianReal, integral_inner, deriv_abs_zero, VectorFourier.fderiv_fourierIntegral, AnalyticAt.harmonicAt_conj, InnerProductGeometry.norm_ofLp_crossProduct, hasStrictDerivAt_abs, EuclideanGeometry.OrthocentricSystem.affineIndependent, SchwartzMap.fourierInv_lineDerivOp_eq, Affine.Simplex.touchpointWeights_reindex, EuclideanGeometry.Sphere.secondInter_smul, Bundle.RiemannianMetric.symm, MeasureTheory.integral_charFun_Icc, real_inner_add_sub_eq_zero_iff, strongConcaveOn_iff_convex, Affine.Simplex.height_map, ProbabilityTheory.Kernel.tendsto_integral_density_of_antitone, ContDiffWithinAt.dist, ProbabilityTheory.moment_truncation_eq_intervalIntegral_of_nonneg, Affine.Simplex.orthogonalProjection_circumcenter, MeasureTheory.mul_le_integral_rnDeriv_of_ac, intervalIntegral.inv_mul_integral_comp_sub_div, EulerSine.integral_sin_mul_sin_mul_cos_pow_eq, Function.Periodic.tendsto_atBot_intervalIntegral_of_pos', NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, DifferentiableOn.norm_sq, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_mem_fundamentalCone_iff, Orientation.oangle_rotation_oangle_left, ProbabilityTheory.hasDerivAt_complexMGF, intervalIntegral.integral_mono_ae, ProbabilityTheory.IsGaussian.charFunDual_eq, ProbabilityTheory.variance_continuousLinearMap_gaussianReal, ProbabilityTheory.covarianceBilin_eq_covarianceBilinDual, ProbabilityTheory.covariance_eq_sub, MeasureTheory.integrable_conv_iff, signedDist_vadd_right, InnerProductSpace.instIsContPerfPairRealInnerₗOfCompleteSpace, hasSum_sq_fourierCoeffOn, circleAverage_mono_on_of_le_circle, ProbabilityTheory.strong_law_aux6, MeasureTheory.tendsto_sum_indicator_atTop_iff', MeasureTheory.integral_prod_mul, contDiff_norm_sq, tendsto_integral_mulExpNegMulSq_comp, SmoothBumpCovering.embeddingPiTangent_injective_mfderiv, intervalAverage_congr_codiscreteWithin, Polynomial.logMahlerMeasure_def, Orientation.oangle_sign_smul_left, deriv_abs_pos, ProbabilityTheory.hasFPowerSeriesAt_mgf, Complex.integral_exp_neg_mul_rpow, NumberField.mixedEmbedding.fundamentalCone.hasFDerivAt_expMap, MeasureTheory.Measure.integrable_compProd_iff, ContDiff.inner, Affine.Simplex.touchpoint_mem_affineSpan, EuclideanGeometry.Sphere.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center, intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae, EuclideanGeometry.oangle_eq_zero_or_eq_pi_iff_collinear, ProbabilityTheory.covarianceBilin_self_nonneg, Orientation.rightAngleRotation_rightAngleRotation, ProbabilityTheory.integral_linearMap_gaussianReal, MeasureTheory.Measure.exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport, exists_msmooth_support_eq_eq_one_iff, fourier_eq, Polynomial.Chebyshev.integral_eval_T_real_measureT_zero, MeasureTheory.integral_le_liminf_integral_of_forall_isOpen_measure_le_liminf_measure, MeasureTheory.L2.real_inner_indicatorConstLp_one_indicatorConstLp_one, ProbabilityTheory.condIndepSets_iff, inner_vsub_vsub_right_eq_dist_sq_left_iff, Orientation.oangle_sign_smul_add_smul_smul_add_smul, Affine.Simplex.direction_mongePlane, integral_inv_of_neg, ProbabilityTheory.covarianceBilinDual_self_eq_variance, ProperCone.innerDual_union, ProbabilityTheory.iCondIndepSet_iff, Affine.Simplex.dist_point_centroid, MeasureTheory.integral_condExpL2_eq_of_fin_meas_real, hasStrictFDerivAt_norm_sq, Affine.Simplex.altitudeFoot_reindex, SmoothPartitionOfUnity.coe_finsupport, SchwartzMap.fourier_evalCLM_eq, ConcaveOn.le_map_integral, Affine.Simplex.affineCombination_eq_touchpoint_iff, Emetric.exists_contMDiffMap_forall_closedBall_subset, norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero, Orientation.oangle_sign_smul_sub_left, Submodule.reflection_sub, TemperedDistribution.instLineDerivSMulReal, MeasureTheory.MemLp.condExp, ProbabilityTheory.differentiableAt_iteratedDeriv_mgf, Affine.Simplex.altitudeFoot_mem_altitude, Orientation.rotation_eq_self_iff_angle_eq_zero, InnerProductGeometry.angle_smul_right_of_neg, Affine.Triangle.inv_tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_circumcenter, ProbabilityTheory.condVar_ae_le_condExp_sq, MDifferentiableOn.inner_bundle, MeasureTheory.Measure.toTemperedDistribution_apply, tendsto_integral_exp_smul_cocompact_of_inner_product, ProbabilityTheory.Kernel.setIntegral_densityProcess, SchwartzMap.instContinuousFourierInv, EuclideanGeometry.oangle_ne_zero_and_ne_pi_iff_affineIndependent, Orientation.oangle_rotation_right, real_inner_le_norm, Affine.Triangle.affineSpan_orthocenter_point_le_altitude, differentiableAt_norm_smul, AntitoneOn.integral_le_sum_Ico, MeasureTheory.setIntegral_abs_condExp_le, Metric.exists_contMDiffMap_forall_closedBall_subset, ProbabilityTheory.IndepFun.integral_fun_comp_mul_comp, EuclideanGeometry.Cospherical.affineIndependent, Differentiable.norm_sq, exists_msmooth_zero_iff_one_iff_of_isClosed, ConcaveOn.set_average_mem_hypograph, RCLike.norm_wInner_le, MeasureTheory.SignedMeasure.haveLebesgueDecomposition_smul_real, ProbabilityTheory.covarianceBilinDual_self_nonneg, IccLeftChart_extend_bot, NumberField.mixedEmbedding.stdBasis_apply_isComplex_fst, ContDiffBump.measure_closedBall_le_integral, TemperedDistribution.fourier_lineDerivOp_eq, ProbabilityTheory.Kernel.integral_densityProcess, MeasureTheory.Integrable.integral_eq_integral_meas_le, EuclideanGeometry.Sphere.IsTangentAt_of_angle_eq_pi_div_two, SmoothPartitionOfUnity.finsum_smul_mem_convex, TemperedDistribution.fourier_delta_zero, intervalIntegral.mul_integral_comp_add_mul, Orientation.inner_eq_zero_of_oangle_eq_neg_pi_div_two, Orientation.rotation_trans, inner_lt_one_iff_real_of_norm_one, signedDist_lineMap_left, ProbabilityTheory.covarianceBilin_real_self, MeasureTheory.BoundedContinuousFunction.integral_eq_integral_meas_le, integral_univ_inv_one_add_sq, MeasureTheory.Integrable.integral_norm_compProd, NumberField.mixedEmbedding.fundamentalDomain_stdBasis, SmoothPartitionOfUnity.sum_le_one', real_inner_le_one_of_norm_eq_one, ValueDistribution.characteristic_sub_characteristic_inv, NumberField.mixedEmbedding.span_latticeBasis, ProbabilityTheory.indepFun_iff_charFun_prod, SchwartzMap.integral_pow_mul_iteratedFDeriv_le, integral_exp_neg_rpow, real_inner_smul_right, AnalyticWithinAt.re_ofReal, Orientation.nonneg_inner_and_areaForm_eq_zero_iff_sameRay, InformationTheory.klDiv_eq_integral_klFun, Orientation.oangle_sub_right_smul_rotation_pi_div_two, abs_real_inner_div_norm_mul_norm_le_one, VectorFourier.fourierSMulRight_apply, MeasureTheory.Integrable.integral_eq_integral_meas_lt, stereographic_neg_apply, integral_cexp_quadratic, TemperedDistribution.lineDerivOp_toTemperedDistributionCLM_eq, MeasureTheory.tendsto_ae_condExp, Affine.Simplex.sOppSide_excenter_singleton_point, ProbabilityTheory.evariance_def', MeasureTheory.condExpL2_indicator_eq_toSpanSingleton_comp, instIsRiemannianManifoldModelWithCornersSelfReal, eventually_norm_symmL_trivializationAt_self_comp_lt, OrthonormalBasis.det_adjustToOrientation, integral_inv, SmoothBumpCovering.embeddingPiTangent_ker_mfderiv, ContMDiffOn.inner_bundle, Complex.orthonormalBasisOneI_repr_symm_apply, SmoothPartitionOfUnity.sum_nonneg, intervalIntegral.abs_integral_le_integral_abs, Manifold.riemannianEDist_def, MeasureTheory.norm_charFun_le_one, hasDerivAt_circleMap, one_div_one_sub_rpow_hasFPowerSeriesOnBall_zero, EuclideanGeometry.oangle_homothety, Affine.Simplex.ExcenterExists.sOppSide_point_excenter_iff, intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae', signedDist_anticomm, real_inner_self_eq_norm_sq, TemperedDistribution.laplacian_eq_sum, Affine.Simplex.dist_circumcenter_eq_circumradius, NumberField.mixedEmbedding.stdBasis_repr_eq_matrixToStdBasis_mul, Orientation.areaForm_comp_rightAngleRotation, modelWithCornersEuclideanHalfSpace_zero, Matrix.PosSemidef.isUnit_sqrt_iff, MeasureTheory.lintegral_nnnorm_condExpL2_indicator_le_real, ProbabilityTheory.exponentialCDFReal_eq_integral, differentiableWithinAt_abs_neg, ContDiffAt.norm_sq, MeasureTheory.integral_comp, TemperedDistribution.instContinuousLineDeriv, ProbabilityTheory.iteratedDeriv_mgf_zero, ProbabilityTheory.moment_truncation_eq_intervalIntegral, VectorFourier.pow_mul_norm_iteratedFDeriv_fourierIntegral_le, hasDerivAt_fourier, ProbabilityTheory.cdf_expMeasure_eq_integral, ProbabilityTheory.condExp_zero_or_one_of_measurableSet_limsup, MeasureTheory.rnDeriv_ae_eq_condExp, OpenPartialHomeomorph.contDiff_univBall, EuclideanGeometry.Sphere.direction_orthRadius_le_iff, NumberField.mixedEmbedding.fundamentalCone.norm_normAtAllPlaces, MeasureTheory.Measure.haarScalarFactor_eq_integral_div, EuclideanGeometry.Sphere.IsTangentAt.mem_and_mem_iff_eq, ProbabilityTheory.isGaussian_iff_gaussian_charFunDual, EuclideanGeometry.collinear_iff_eq_or_eq_or_sin_eq_zero, ProbabilityTheory.hasFiniteIntegral_comp_iff', ProbabilityTheory.covarianceOperator_inner, real_inner_self_nonpos, mellin_eq_fourierIntegral, hasStrictDerivAt_abs_neg, MDifferentiableWithinAt.inner_bundle, Orientation.inner_rightAngleRotation_left, AffineSubspace.mem_perpBisector_iff_inner_eq_inner, InnerProductGeometry.angle_eq_angle_add_angle_iff, ProbabilityTheory.norm_uncenteredCovarianceBilinDual_le, integral_cos_pow_three, EuclideanGeometry.Sphere.IsTangent.infDist_eq_radius, SchwartzMap.integral_sesq_fourierIntegral_eq, LSeries_eq_mul_integral, fourierIntegral_eq', HasFDerivAt.inner, ProbabilityTheory.paretoCDFReal_eq_integral, MeasureTheory.condExpL1CLM_lpMeas, SmoothBumpCovering.exists_finset_toSmoothPartitionOfUnity_eventuallyEq, integral_one_div_of_pos, EuclideanGeometry.inversion_def, deriv_circleMap, Affine.Simplex.inner_vsub_altitudeFoot_vsub_altitudeFoot_eq_zero, ProbabilityTheory.covarianceBilin_apply_pi, ProbabilityTheory.deriv_mgf, SchwartzMap.integral_bilinear_laplacian_right_eq_left, ExistsContDiffBumpBase.u_smooth, intervalIntegral.intervalIntegral_pos_of_pos_on, VectorFourier.hasFTaylorSeriesUpTo_fourierIntegral', contDiff_fourier, ProbabilityTheory.condExpKernel_ae_eq_condExp, Orientation.kahler_apply_self, Affine.Simplex.dist_circumcenter_eq_circumradius', EuclideanGeometry.Sphere.IsTangent.notMem_of_dist_lt, signedDist_triangle_right, Orientation.inner_smul_rotation_pi_div_two_right, ProbabilityTheory.hasFiniteIntegral_comp_iff, EuclideanGeometry.Sphere.IsIntTangentAt.wbtw, Orientation.inner_eq_zero_of_oangle_eq_pi_div_two, contMDiffWithinAt_comp_projIcc_iff, Orientation.inner_mul_areaForm_sub', hasFDerivAt_polarCoord_symm, fourierIntegral_gaussian_innerProductSpace, MeasureTheory.dist_convolution_le', EuclideanGeometry.Sphere.IsTangentAt.le_orthRadius, EuclideanGeometry.Sphere.isDiameter_of_angle_eq_pi_div_two, AnalyticWithinAt.im_ofReal, RCLike.I_to_real, ProbabilityTheory.hasDerivAt_neg_exp_mul_exp, abs_signedDist_eq_dist_iff_vsub_mem_span, iteratedDeriv_fourier, Affine.Simplex.ExcenterExists.isTangentAt_exsphere_iff_eq_touchpoint, Orientation.kahler_rotation_left', ProbabilityTheory.Kernel.integral_density, Affine.Simplex.ExcenterExists.excenter_notMem_affineSpan_pair, Affine.Simplex.pointsWithCircumcenter_point, Orientation.oangle_eq_zero_or_eq_pi_iff_not_linearIndependent, eventually_norm_symmL_trivializationAt_comp_self_lt, eulerMascheroniConstant_eq_neg_deriv, EuclideanSpace.volume_ball_fin_three, ProbabilityTheory.IsGaussian.integral_dual, Affine.Simplex.mongePoint_reindex, Affine.Triangle.affineSpan_pair_eq_orthRadius_insphere, Orientation.abs_areaForm_le, EuclideanGeometry.cospherical_or_collinear_of_two_zsmul_oangle_eq, IsOpen.exists_msmooth_support_eq_aux, Affine.Simplex.mongePoint_eq_smul_vsub_vadd_circumcenter, EuclideanGeometry.angle_homothety, logDeriv_exp, InnerProductGeometry.angle_smul_smul, integral_log_sin_zero_pi, Polynomial.Chebyshev.integral_eval_T_real_mul_eval_T_real_measureT, NumberField.mixedEmbedding.fundamentalCone.hasFDerivAt_expMapBasis, intervalIntegral.integral_pos_iff_support_of_nonneg_ae, OpenPartialHomeomorph.contDiff_unitBallBall, Affine.Simplex.altitude_reindex, MeasureTheory.L2.inner_indicatorConstLp_eq_setIntegral_inner, MeasureTheory.Integrable.integral_norm_condDistrib, NumberField.mixedEmbedding.euclidean.instIsZLatticeRealMixedSpaceIntegerLattice, signedDist_neg, ProbabilityTheory.covarianceBilin_apply_basisFun, exists_contMDiff_zero_iff_one_iff_of_isClosed, Complex.restrictScalars_toSpanSingleton, Orientation.oangle_sign_smul_right, Orientation.normSq_kahler, ProbabilityTheory.condExpKernel_ae_eq_trim_condExp, integral_inv_sq_add_sq, NumberField.mixedEmbedding.fundamentalCone.hasDerivAt_expMap_single, ProbabilityTheory.setIntegral_preCDF_fst, NumberField.mixedEmbedding.negAt_symm, neg_one_le_real_inner_of_norm_eq_one, VectorFourier.contDiff_fourierIntegral, ConcaveOn.le_map_average, ProbabilityTheory.integrable_compProd_iff, intervalIntegral.measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_left, Complex.inner, Polynomial.sum_sq_norm_coeff_eq_circleAverage, ContDiffBump.contDiff_normed, integral_rpow, AnalyticAt.harmonicAt_re, Orientation.oangle_sign_add_smul_left, ProbabilityTheory.iCondIndepSets_iff, Diffeology.isPlot_iff_contDiff, Matrix.PosSemidef.sq_sqrt, signedDist_vsub_self_rev, InformationTheory.toReal_klDiv_of_measure_eq, intervalIntegral.measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae, EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangent, Orientation.neg_rotation_pi_div_two, ProperCone.relative_hyperplane_separation, contDiffAt_inner, NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis, OrthonormalBasis.measurePreserving_repr_symm, NumberField.mixedEmbedding.instIsZLatticeRealMixedSpaceIntegerLattice, MeasureTheory.measureReal_abs_gt_le_integral_charFun, DifferentiableOn.inner, eventually_enorm_mfderiv_extChartAt_lt, enorm_tangentSpace_vectorSpace, integral_exp_neg_Ioi, Differentiable.inner, signedDist_linear_apply, UnitAddCircle.measurePreserving_mk, NumberField.mixedEmbedding.negAt_apply_isReal_and_mem, Orientation.rotation_eq_matrix_toLin, oneTangentSpaceIcc_def, Orientation.inner_rightAngleRotation_swap, abs_circleAverage_le_circleAverage_abs, IccRightChart_extend_top_mem_frontier, NumberField.mixedEmbedding.volume_negAt_plusPart, Orientation.oangle_sub_left_smul_rotation_pi_div_two, ProperCone.innerDual_insert, ProbabilityTheory.integral_truncation_le_integral_of_nonneg, ZLattice.covolume.tendsto_card_div_pow', SmoothPartitionOfUnity.sum_eq_one, SchwartzMap.hasDerivAt, MeasureTheory.tendsto_eLpNorm_condExp, Orientation.oangle_eq_iff_eq_norm_div_norm_smul_rotation_or_eq_zero, MeasureTheory.eLpNorm_one_condExp_le_eLpNorm, Affine.Simplex.incenter_eq_affineCombination, integral_log, signedDist_self, integral_sqrt_one_sub_sq, tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_measure_nhdsWithin_pos, circleAverage_log_norm_add_const_eq_posLog, Gamma_eq_integral, signedDist_vsub_self, EuclideanGeometry.inversion_mul, stereographic_target, MeasureTheory.SignedMeasure.rnDeriv_smul, signedDist_smul, TemperedDistribution.fourierTransform_apply, Orientation.oangle_add_right_smul_rotation_pi_div_two, MeromorphicOn.circleAverage_log_norm, Orientation.inner_smul_rotation_pi_div_two_left, ZLattice.volume_image_eq_volume_div_covolume, MeasureTheory.SignedMeasure.haveLebesgueDecomposition_smul, ContDiffOn.norm_sq, map_linearMap_volume_pi_eq_smul_volume_pi, intervalIntegral.inv_mul_integral_comp_div_sub, Affine.Simplex.sOppSide_point_excenter_singleton, Euclidean.closedBall_eq_preimage, NumberField.mixedEmbedding.iUnion_negAt_plusPart_union, AffineSubspace.mem_perpBisector_iff_dist_eq', Matrix.PosSemidef.inv_sqrt, intervalIntegral.differentiable_integral_of_continuous, integral_log_from_zero_of_pos, LipschitzWith.locallyIntegrable_lineDeriv, InnerProductSpace.laplacian_eq_iteratedFDeriv_stdOrthonormalBasis, Affine.Simplex.ninePointCircle_center_mem_affineSpan, SmoothBumpCovering.embeddingPiTangent_injOn, EulerSine.integral_cos_pow_eq, MeasureTheory.measureReal_abs_dual_gt_le_integral_charFunDual, Orientation.kahler_rightAngleRotation_left, intervalIntegral.hasFDerivAt_integral_of_dominated_of_fderiv_le, ConvexOn.average_mem_epigraph, MeasureTheory.Measure.map_linearMap_addHaar_pi_eq_smul_addHaar, MeasureTheory.integral_condExp_indicator, eventually_norm_symmL_trivializationAt_lt, Function.locallyFinsuppWithin.logCounting_divisor_eq_circleAverage_sub_const, AffineSubspace.perpBisector_eq_top, Orientation.oangle_smul_right_of_neg, fourierIntegral_convergent_iff, ProbabilityTheory.Kernel.tendsto_setIntegral_densityProcess, LipschitzOnWith.ae_differentiableWithinAt_real, MeasureTheory.AEStronglyMeasurable.ae_integrable_condDistrib_map_iff, integral_sin, innerₗ_apply_apply, Function.hasTemperateGrowth_inner_left, exists_eq_const_mul_intervalIntegral_of_ae_nonneg, AffineSubspace.midpoint_mem_perpBisector, inner_sum_smul_sum_smul_of_sum_eq_zero, ProbabilityTheory.hasDerivAt_iteratedDeriv_mgf, Affine.Simplex.touchpoint_reindex, hasDerivAt_fourierChar, le_integral_rpowIntegrand₀₁_one, bilinFormOfRealInner_orthogonal, ContinuousLinearMap.intervalIntegral_apply, MeasureTheory.norm_one_sub_charFun_le_two, analyticWithinAt_sigmoid, EuclideanGeometry.inner_weightedVSub, Orientation.kahler_rotation_left, LindemannWeierstrass.integral_exp_mul_eval, ProbabilityTheory.variance_le_expectation_sq, MeasureTheory.Integrable.withDensityᵥ_trim_eq_integral, analyticOn_sigmoid, EuclideanGeometry.Sphere.center_mem_orthRadius_iff, EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp, MeasureTheory.integral_fin_nat_prod_eq_prod, EuclideanGeometry.collinear_of_sin_eq_zero, OrthonormalBasis.orthonormal_adjustToOrientation, MeasureTheory.Measure.integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport, Affine.Simplex.ExcenterExists.excenter_mem_affineSpan_range, ContDiffBump.integral_le_measure_closedBall, SchwartzMap.inner_fourierTransformCLM_toL2_eq, mdifferentiableWithinAt_comp_projIcc_iff, zero_at_infty_fourier, Orientation.inner_sq_add_areaForm_sq, intervalIntegral.integral_nonneg_of_ae_restrict, signedDist_smul_of_neg, iteratedFDeriv_fourier, norm_add_sq_real, hasFPowerSeriesOnBall_linear_zero, differentiableAt_abs_pos, SchwartzMap.convolution_continuous_left, Affine.Triangle.orthocenter_mem_altitude, Polynomial.Chebyshev.integral_eval_T_real_measureT_of_ne_zero, hasDerivAt_Gamma_one_half, ProbabilityTheory.isPosSemidef_covarianceBilinDual, EuclideanGeometry.angle_left_midpoint_eq_pi_div_two_of_dist_eq, fderiv_norm_smul, Diffeology.IsContDiffCompatible.isPlot_iff, MeasureTheory.Measure.integrable_integral_norm_of_integrable_comp, InnerProductSpace.laplacian_eq_iteratedFDeriv_complexPlane, NumberField.mixedEmbedding.injective_mixedSpaceOfRealSpace, SchwartzMap.integral_fourier_mul_eq, range_mfderiv_coe_sphere, ProbabilityTheory.strong_law_aux7, EuclideanGeometry.Sphere.isDiameter_iff_mem_and_mem_and_dist, Affine.Triangle.eulerPoint_eq_midpoint, MeasureTheory.integrable_prod_iff', stereographic_source, hahnEmbedding_isOrderedModule_rat, Affine.Simplex.sign_signedInfDist_touchpoint_empty, MeasureTheory.SignedMeasure.singularPart_add_withDensity_rnDeriv_eq, one_add_rpow_hasFPowerSeriesAt_zero, integral_sin_pow_odd_mul_cos_pow, signedDist_vadd_right_swap, ProbabilityTheory.integral_condCDF, ValueDistribution.proximity_zero_of_complexValued, hasFDerivAt_fourierIntegral, SchwartzMap.integralCLM_apply, EulerSine.tendsto_integral_cos_pow_mul_div, Affine.Simplex.midpoint_faceOppositeCentroid_eulerPoint, MeasureTheory.withDensityᵥ_toReal, ProbabilityTheory.Kernel.condExp_densityProcess, EuclideanSpace.volume_ball_fin_two, EuclideanSpace.inner_basisFun_real, iccLeftChart_extend_zero, SmoothBumpCovering.comp_embeddingPiTangent_mfderiv, EuclideanGeometry.Sphere.IsTangentAt.eq_orthogonalProjection, MeasureTheory.SignedMeasure.singularPart_smul_nnreal, ProbabilityTheory.covarianceBilin_real, bernoulliFun_eq_integral, EuclideanGeometry.Sphere.IsDiameter.midpoint_eq_center, ProbabilityTheory.moment_def, SchwartzMap.fourier_coe, Affine.Triangle.dist_circumcenter_reflection_orthocenter_finset, ProbabilityTheory.iIndepFun.integral_prod_eq_prod_integral, Euclidean.ball_eq_preimage, SchwartzMap.lineDerivOp_fourierInv_eq, InformationTheory.rightDeriv_klFun_one, hasDerivAt_abs, NumberField.mixedEmbedding.stdBasis_apply_isReal, Function.RCLike.hasTemperateGrowth_ofReal, EuclideanGeometry.Sphere.secondInter_vsub_mem_affineSpan, EuclideanSpace.volume_ball, ContDiffAt.norm, EuclideanGeometry.inner_nonneg_of_dist_le_radius, intervalIntegral.integral_hasFDerivWithinAt_of_tendsto_ae, Orientation.inner_eq_zero_iff_eq_zero_or_eq_smul_rotation_pi_div_two, ProbabilityTheory.covarianceBilin_of_not_memLp, InformationTheory.rightDeriv_klFun, interior_range_modelWithCornersEuclideanHalfSpace, ExistsContDiffBumpBase.y_smooth, contDiff_inner, ProbabilityTheory.condVar_bot', Affine.Simplex.point_eq_affineCombination_of_pointsWithCircumcenter, hasDerivAt_Gamma_one, AffineSubspace.perpBisector_self, fourier_bilin_convolution_eq_integral, IntervalIntegrable.intervalIntegrable_slope, SchwartzMap.fourierInv_coe, ProperCone.innerDual_empty, inner_vsub_vsub_left_eq_dist_sq_right_iff, ConvexOn.map_integral_le, Differentiable.dist, GaussianFourier.integral_cexp_neg_mul_sq_add_real_mul_I, Orientation.oangle_map, EulerSine.antideriv_cos_comp_const_mul, ProbabilityTheory.condVar_of_sigmaFinite, EuclideanGeometry.Sphere.isDiameter_iff_mem_and_mem_and_wbtw, ContDiffAt.dist, EuclideanGeometry.oangle_midpoint_rev_right, Orientation.kahler_mul, innerSL_real_flip, GaussianFourier.integral_cexp_neg_mul_sum_add, tsum_sq_fourierCoeffOn, ProbabilityTheory.covarianceBilinDual_comm, ProbabilityTheory.isGaussian_iff_charFunDual_eq, ProbabilityTheory.iteratedDeriv_two_cgf, SchwartzMap.integral_smul_lineDerivOp_right_eq_neg_left, integral_exp_mul_Ioi, integral_sin_mul_cos_sq, SmoothPartitionOfUnity.exists_pos_of_mem, ProbabilityTheory.deriv_mgf_zero, MeasureTheory.charFun_eq_charFunDual_toDualMap, Affine.Simplex.incenter_mem_affineSpan_range, real_inner_sub_sub_self, Orientation.oangle_smul_smul_self_of_nonneg, fourierIntegral_gaussian, deriv_sigmoid, ZLattice.volume_image_eq_volume_div_covolume', flip_innerₗ, Affine.Simplex.eulerPoint_reindex, one_add_rpow_hasFPowerSeriesAt_zero, ProbabilityTheory.iCondIndepFun_iff, circleAverage_log_norm_sub_const_eq_posLog, Orientation.rightAngleRotation_trans_neg_orientation, Orientation.volumeForm_robust', exists_smooth_zero_one_of_isClosed, NumberField.mixedEmbedding.instIsZLatticeRealMixedSpaceIdealLattice, ContMDiff.inner_bundle, real_inner_self_eq_norm_mul_norm, Affine.Simplex.excenterWeights_map, EulerSine.antideriv_sin_comp_const_mul, Affine.Simplex.sum_inv_height_sq_smul_vsub_eq_zero, analyticAt_log, MeasureTheory.ae_mem_limsup_atTop_iff, signedDist_vadd_left, Diffeology.IsPlot.contDiff, MeasureTheory.charFun_zero_measure, ContDiffBump.convolution_eq_right, TemperedDistribution.instFourierInvSMul, ExistsContDiffBumpBase.w_def, ProbabilityTheory.deriv_cgf, isBoundedBilinearMap_inner, integral_gaussian_sq_complex, contDiff_stereoInvFunAux, Affine.Simplex.incenter_notMem_affineSpan_pair, intervalIntegral.integral_hasFDerivWithinAt, circleAverage_log_norm_factorizedRational, SmoothBumpCovering.embeddingPiTangent_injective, LinearIsometryEquiv.toMeasurableEquiv_symm, instIsContMDiffRiemannianBundleTrivial, SchwartzMap.toLp_fourierTransform_eq, ContDiff.dist, ProbabilityTheory.covarianceBilin_apply, exists_contMDiff_support_eq_eq_one_iff, fourierIntegral_half_period_translate, MeasureTheory.stronglyMeasurable_charFun, AffineSubspace.mem_perpBisector_iff_inner_pointReflection_vsub_eq_zero, Orientation.eq_zero_or_oangle_eq_iff_inner_eq_zero, Affine.Simplex.touchpoint_eq_point_rev, EuclideanGeometry.hasFDerivAt_inversion, Orientation.kahler_map, TemperedDistribution.instFourierInvAdd, dist_div_norm_sq_smul, MeasureTheory.Lp.fourierInv_toTemperedDistribution_eq, volume_regionBetween_eq_integral', MeasureTheory.ae_bdd_condExp_of_ae_bdd, hasDerivAt_norm_rpow, Affine.Simplex.signedInfDist_reindex, UnitAddTorus.hasSum_prod_mFourierCoeff, ContMDiffAt.inner_bundle, NumberField.mixedEmbedding.latticeBasis_apply, SmoothPartitionOfUnity.sum_finsupport_smul_eq_finsum, ProbabilityTheory.uncenteredCovarianceBilin_of_not_memLp, signedDist_apply_linear_apply, SchwartzMap.integral_mul_deriv_eq_neg_deriv_mul, TemperedDistribution.fourierInv_apply, AnalyticAt.harmonicAt_log_norm, EuclideanGeometry.inversion_mem_perpBisector_inversion_iff, ProbabilityTheory.HasGaussianLaw.charFunDual_map_eq_fun, Affine.Simplex.neg_one_lt_inner_vsub_altitudeFoot_div, Affine.Simplex.ExcenterExists.touchpointWeights_map, MonotoneOn.exists_tendsto_deriv_liminf_lintegral_enorm_le, EuclideanGeometry.collinear_of_angle_eq_pi, ProbabilityTheory.covarianceBilin_map, Affine.Simplex.mongePoint_map, Affine.Simplex.eulerPoint_map, SchwartzMap.instFourierSMul, MeasureTheory.measureReal_abs_inner_gt_le_integral_charFun, Orientation.two_zsmul_oangle_smul_right_self, Affine.Triangle.sOppSide_affineSpan_pair_point_excenter_singleton, SchwartzMap.fourierTransformCLM_apply, AffineSubspace.signedInfDist_singleton, EuclideanGeometry.angle_midpoint_eq_pi, hasSum_one_div_nat_pow_mul_sin, Orientation.coe_basisRightAngleRotation, TemperedDistribution.fourierTransform_toTemperedDistributionCLM_eq, intervalIntegral.mul_integral_comp_mul_add, SchwartzMap.fderivCLM_fourier_eq, ProbabilityTheory.iIndepFun_iff_charFun_pi, Bundle.ContinuousRiemannianMetric.pos, ProbabilityTheory.strong_law_aux4, TemperedDistribution.instLineDerivAdd, SchwartzMap.derivCLM_apply, ProbabilityTheory.condExp_zero_or_one_of_measurableSet_limsup_atTop, Affine.Simplex.affineCombination_touchpointWeights, intervalIntegral.integral_nonneg_of_ae, Orientation.volumeForm_zero_neg, SmoothPartitionOfUnity.contMDiff_finsum_smul, ContDiffBump.dist_normed_convolution_le, Orientation.oangle_eq_iff_eq_norm_div_norm_smul_rotation_of_ne_zero, SmoothPartitionOfUnity.sum_finsupport, Orientation.areaForm_map, Affine.Triangle.orthocenter_mem_affineSpan, EuclideanGeometry.oangle_ne_zero_and_ne_pi_iff_not_collinear, Complex.GammaSeq_eq_approx_Gamma_integral, deriv_bernoulliFun, OrthonormalBasis.adjustToOrientation_apply_eq_or_eq_neg, det_fderivPiPolarCoordSymm, isConformalMap_iff, ProbabilityTheory.condVar_bot_ae_eq, Affine.Simplex.faceOppositeCentroid_mem_ninePointCircle, Affine.Simplex.mongePoint_mem_affineSpan, real_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two, SchwartzMap.integral_clm_comp_deriv_right_eq_neg_left, NumberField.mixedEmbedding.commMap_apply_of_isReal, Fourier.norm_fourierIntegral_le_integral_norm, RCLike.ofReal_real_eq_id, EuclideanGeometry.Sphere.IsTangent.isTangentAt, ZSpan.fundamentalDomain_pi_basisFun, LipschitzWith.ae_differentiableAt_of_real, ProperCone.mem_innerDual, EuclideanGeometry.Sphere.orthRadius_le_orthRadius_iff, MeasureTheory.Measure.integrable_comp_iff, Bundle.RiemannianMetric.pos, IsOpen.exists_contDiff_support_eq, integral_zpow, TemperedDistribution.instLineDerivSMulComplex, exists_eq_interval_average_of_measure, NumberField.mixedEmbedding.hasFDerivAt_polarCoordReal_symm, Function.Complex.hasTemperateGrowth_ofReal, InnerProductGeometry.inner_eq_mul_norm_of_angle_eq_zero, ConvexOn.map_average_le, ProbabilityTheory.analyticOnNhd_mgf, GaussianFourier.integrable_cexp_neg_mul_sq_norm_add, integral_one_div_one_add_sq, EuclideanGeometry.collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi, Complex.log_eq_integral, MeasureTheory.BoundedContinuousFunction.integral_le_of_levyProkhorovEDist_lt, Affine.Simplex.incenter_reindex, integral_one, circleAverage_log_norm_sub_const₂, Manifold.pathELength_eq_lintegral_mfderiv_Icc, AffineSubspace.mem_perpBisector_iff_dist_eq, MeasureTheory.hasFiniteIntegral_prod_iff, MeasureTheory.charFun_map_mul, Orientation.inner_rightAngleRotationAux₁_right, hasFDerivAt_pi_polarCoord_symm, ContDiffWithinAt.inner, NumberField.mixedEmbedding.latticeBasis_repr_apply, norm_tangentSpace_vectorSpace, Affine.Simplex.mongePoint_vsub_face_centroid_eq_weightedVSub_of_pointsWithCircumcenter, InformationTheory.not_differentiableWithinAt_klFun_Ioi_zero, DifferentiableWithinAt.norm_sq, SchwartzMap.integral_fourierInv_mul_eq, fourierIntegral_continuousLinearMap_apply', TemperedDistribution.laplacian_toTemperedDistributionCLM_eq, integral_sin_pow_succ_le, ProbabilityTheory.iteratedDeriv_two_cgf_eq_integral, signedDist_right_lineMap, ProbabilityTheory.uncenteredCovarianceBilin_zero, differentiable_fourierChar, hasFDerivAt_integral_of_dominated_of_fderiv_le, EuclideanGeometry.Sphere.mem_tangentSet_iff, logDeriv_sin, VectorFourier.fourierPowSMulRight_apply, inner_eq_norm_mul_iff_real, Affine.Simplex.altitude_map, ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_cgf, SmoothBumpCovering.support_toSmoothPartitionOfUnity_subset, DifferentiableOn.dist, NumberField.mixedEmbedding.normAtPlace_negAt, Chebyshev.integral_theta_div_log_sq_isBigO, SchwartzMap.convolution_flip, Matrix.l2_opNorm_le_one_of_mem_doublyStochastic, AlternatingMap.measure_def, LinearIsometryEquiv.reflections_generate_dim, Complex.isometryOfOrthonormal_apply, SchwartzMap.laplacian_eq_sum, tendsto_Icc_vitaliFamily_left, Complex.sameRay_iff, integral_le_sum_Ico_of_le, EuclideanGeometry.Sphere.isTangentAt_center_iff, integral_gaussian, intervalIntegral.integral_smul_const, ProbabilityTheory.hasDerivAt_iteratedDeriv_complexMGF, intervalIntegral.mul_integral_comp_sub_mul, contMDiffOn_comp_projIcc_iff, intervalIntegral.abs_integral_eq_abs_integral_uIoc, NumberField.mixedEmbedding.finrank, Orientation.two_zsmul_oangle_smul_right_of_ne_zero, integral_one_div, ProbabilityTheory.integral_id_gaussianReal, SchwartzMap.integral_fourier_smul_eq, ProbabilityTheory.meas_ge_le_evariance_div_sq, SmoothBumpFunction.contMDiff, AnalyticAt.re_ofReal, Orientation.inner_rightAngleRotation_right, GaussianFourier.integral_cexp_neg_sum_mul_add, volume_euclideanSpace_eq_dirac, NumberField.mixedEmbedding.fractionalIdealLatticeBasis_apply, eventually_norm_mfderivWithin_symm_extChartAt_comp_lt, MeasureTheory.Measure.exists_integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport, ConcaveOn.average_mem_hypograph, integral_sin_sq_mul_cos, ProbabilityTheory.IsRatCondKernelCDFAux.setIntegral_iInf_rat_gt, intervalIntegral.norm_integral_le_integral_norm, Complex.sameRay_iff_arg_div_eq_zero, Affine.Simplex.ExcenterExists.signedInfDist_excenter, Orientation.volumeForm_apply_le, BoxIntegral.Box.volume_apply, SmoothPartitionOfUnity.finite_tsupport, VectorFourier.hasFTaylorSeriesUpTo_fourierIntegral, Complex.integral_rpow_mul_exp_neg_mul_rpow, NumberField.mixedEmbedding.negAt_apply_norm_isReal, Chebyshev.integral_theta_div_log_sq_isLittleO, InnerProductSpace.laplacian_eq_iteratedFDeriv_orthonormalBasis, SchwartzMap.instFourierInvAdd, abs_real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul, EulerSine.integral_cos_pow_pos, MonotoneOn.integral_le_sum, MeasureTheory.pdf.IsUniform.integral_eq, ContDiff.norm, OpenPartialHomeomorph.contDiffOn_univBall_symm, AntitoneOn.sum_le_integral, stereographic_apply, Affine.Triangle.sbtw_touchpoint_empty, Orientation.rotation_apply, integral_pow_mul_le_of_le_of_pow_mul_le, deriv_fourierChar, TemperedDistribution.derivCLM_toTemperedDistributionCLM_eq, iteratedFDeriv_fourierIntegral, hasDerivWithinAt_abs_neg, StieltjesFunction.ae_hasDerivAt, contDiffWithinAt_abs, hasSum_sq_fourierCoeff, ProbabilityTheory.strong_law_aux1, ProbabilityTheory.condExp_zero_or_one_of_measurableSet_limsup_atBot, Affine.Simplex.touchpoint_empty_notMem_affineSpan_of_ne, EuclideanGeometry.Sphere.IsTangentAt_iff_angle_eq_pi_div_two, Orientation.kahler_apply_apply, Orientation.inner_rightAngleRotationAux₁_left, exists_embedding_euclidean_of_compact, HasDerivAt.inner, LineDeriv.tensorLineDerivTwo_canonicalCovariantTensor_eq_sum, Orientation.areaForm_apply_self, Orientation.oangle_smul_add_right_eq_zero_or_eq_pi_iff, ProbabilityTheory.hasFiniteIntegral_compProd_iff, differentiable_fourierChar_neg_bilinear_right, MeasureTheory.Lp.ker_toTemperedDistributionCLM_eq_bot, Affine.Simplex.sSameSide_point_excenter_singleton, ProbabilityTheory.variance_linearMap_gaussianReal, MeasureTheory.Lp.toTemperedDistribution_toLp_eq, MeasureTheory.condExp_stronglyMeasurable_mul_of_bound₀, AffineSubspace.signedInfDist_def, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply, ValueDistribution.logCounting_zero_sub_logCounting_top_eq_circleAverage_sub_const, Affine.Simplex.acuteAngled_reindex_iff, MeasureTheory.BoundedContinuousFunction.inner_toLp, Submodule.angle_coe, tendsto_integral_gaussian_smul, MeasureTheory.integral_fintype_prod_volume_eq_prod, Affine.Simplex.mem_altitude, Affine.Simplex.isDiameter_ninePointCircle, ProbabilityTheory.IsGaussian.integral_dual_conv_map_neg_eq_zero, UnitAddTorus.span_mFourier_closure_eq_top, signedDist_lineMap_right, TemperedDistribution.laplacian_apply_apply, MeasureTheory.Integrable.uniformIntegrable_condExp_filtration, Affine.Triangle.sSameSide_affineSpan_pair_point_excenter_singleton, Affine.Triangle.dist_div_sin_angle_div_two_eq_circumradius, integral_rpow_mul_exp_neg_mul_Ioi, SchwartzMap.tsupport_derivCLM_subset, Affine.Simplex.orthogonalProjectionSpan_eulerPoint_mem_ninePointCircle, tendsto_integral_exp_inner_smul_cocompact, Affine.Simplex.mongePlane_reindex, Manifold.lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc, SchwartzMap.integral_smul_laplacian_right_eq_left, SchwartzMap.le_seminorm', differentiable_norm_rpow, VectorFourier.fourierIntegral_probChar, SchwartzMap.instFourierInvPair, Affine.Simplex.sign_signedInfDist_incenter, Affine.Simplex.ExcenterExists.sign_signedInfDist_excenter, Orientation.rightAngleRotation_map, ProbabilityTheory.evariance_eq_zero_iff, integral_inv_one_add_sq, VectorFourier.norm_fourierSMulRight_le, AlternatingMap.measure_parallelepiped, EuclideanGeometry.Sphere.isTangentAt_iff_dist_sq_eq_power, Orientation.two_zsmul_oangle_smul_left_self, Orientation.kahler_rotation_right, integral_Ioi_cpow_of_lt, MeasureTheory.charFun_dirac, ProbabilityTheory.Kernel.setIntegral_density, Affine.Simplex.signedInfDist_affineCombination, NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis, TemperedDistribution.lineDerivOp_apply_apply, ProbabilityTheory.strong_law_aux2, intervalIntegral.mul_integral_comp_mul_right, one_div_sub_pow_hasFPowerSeriesOnBall_zero, signedDist_apply, Polynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv, ProbabilityTheory.iIndepFun.integral_fun_prod_eq_prod_integral, intervalIntegral.norm_integral_le_abs_integral_norm, UnitAddTorus.hasSum_sq_mFourierCoeff, TemperedDistribution.lineDerivOp_fourierInv_eq, Polynomial.Chebyshev.integral_eval_T_real_mul_eval_T_real_measureT_of_ne, sphere_ext_iff, integral_sin_pow_odd, EuclideanGeometry.dist_affineCombination, ProbabilityTheory.hasDerivAt_integral_pow_mul_exp_real, Orientation.oangle_sign_smul_add_smul_right, signedDist_eq_dist_iff_vsub_mem_span, EuclideanGeometry.Sphere.mem_commonIntTangents_iff, AffineSubspace.direction_perpBisector, volume_regionBetween_eq_integral, AffineSubspace.angle_coe, OrthonormalBasis.same_orientation_iff_det_eq_det, ProbabilityTheory.IsGaussian.charFun_eq, Affine.Simplex.ninePointCircle_map, ContinuousAt.inner_bundle, VectorFourier.norm_fourierPowSMulRight_le, EuclideanGeometry.dist_smul_vadd_eq_dist, integral_gaussian_complex, SmoothPartitionOfUnity.mem_fintsupport_iff, Emetric.exists_smooth_forall_closedBall_subset, ProbabilityTheory.norm_uncenteredCovarianceBilin_le, hasFDerivAt_fourierChar_neg_bilinear_right, ContinuousWithinAt.inner_bundle, intervalIntegral.inv_mul_integral_comp_div, AffineSubspace.mem_perpBisector_iff_inner_eq, ProbabilityTheory.strong_law_aux3, MeasureTheory.BoundedContinuousFunction.integral_eq_integral_meas_le_of_hasFiniteIntegral, SchwartzMap.integral_inner_fourier_fourier, VectorFourier.norm_fourierSMulRight, InnerProductSpace.volume_closedBall, Function.Periodic.integral_le_sSup_add_zsmul_of_pos, differentiableOn_abs, ProbabilityTheory.hasDerivAt_mgf, integral_exp_mul_complex_Iic, InnerProductSpace.laplacian_eq_iteratedDeriv_real, MeasureTheory.Lp.toTemperedDistribution_apply, TemperedDistribution.smulLeftCLM_const, strongConvexOn_iff_convex, EuclideanGeometry.angle_right_midpoint_eq_pi_div_two_of_dist_eq, Orientation.oangle_eq_pi_iff_sameRay_neg, SchwartzMap.fourier_fderivCLM_eq, SchwartzMap.fourier_convolution_apply, intervalIntegral.integral_eq_zero_iff_of_nonneg_ae, ProbabilityTheory.strong_law_ae_real, iteratedDeriv_fourierIntegral, SchwartzMap.instContinuousFourier, ContDiffAt.inner, real_inner_smul_left, norm_add_mul_self_real, ExistsContDiffBumpBase.w_integral, NumberField.mixedEmbedding.fundamentalCone.abs_det_fderiv_expMapBasis, ProbabilityTheory.deriv_cgf_zero, Orientation.oangle_rotation_self_right, LipschitzWith.integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul, NumberField.mixedEmbedding.euclidean.finrank, DifferentiableAt.norm, differentiable_fourierChar_neg_bilinear_left, MeasureTheory.lpNorm_expect_le, ProbabilityTheory.IsGaussian.ext_iff, fderiv_norm_smul_pos, EuclideanGeometry.concyclic_or_collinear_of_two_zsmul_oangle_eq, integral_Ioi_inv_one_add_sq, circleAverage_mono, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_expMap_symm, Affine.Simplex.ExcenterExists.signedInfDist_excenter_eq_mul_sum_inv, MeasureTheory.Measure.integral_isAddLeftInvariant_isAddRightInvariant_combo, TemperedDistribution.instContinuousFourierInv, Polynomial.Chebyshev.integral_eval_T_real_mul_self_measureT_zero, NumberField.mixedEmbedding.measurableSet_negAt_plusPart, range_modelWithCornersEuclideanHalfSpace, VectorFourier.fourierPowSMulRight_iteratedFDeriv_fourierIntegral, NumberField.mixedEmbedding.euclidean.volumePreserving_toMixed_symm, ProbabilityTheory.iIndepFun.integral_fun_prod_comp, integral_exp_neg_Ioi_zero, nnnorm_tangentSpace_vectorSpace, OrthonormalBasis.toMatrix_orthonormalBasis_mem_orthogonal, real_inner_add_add_self, TemperedDistribution.fourier_apply, Matrix.PosSemidef.sqrt_mul_self, Orientation.areaForm_rightAngleRotation_right, OrthonormalBasis.orientation_adjustToOrientation, MDifferentiableAt.inner_bundle, contDiff_norm_rpow, exists_contDiff_tsupport_subset, ProbabilityTheory.indepFun_iff_integral_comp_mul, tsum_sq_fourierCoeff, intervalIntegral.integral_pos, Affine.Simplex.touchpoint_mem_affineSpan_simplex, Orientation.inner_smul_rotation_pi_div_two_smul_left, integral_sin_pow, ProbabilityTheory.iIndepFun.integral_prod_comp, SchwartzMap.coe_apply, real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul, integral_mul_cpow_one_add_sq, EuclideanGeometry.angle_eq_zero_iff_ne_and_wbtw, AntitoneOn.integral_le_sum, integral_gaussian_Ioi, Orientation.oangle_smul_right_of_pos, abs_real_inner_div_norm_mul_norm_eq_one_iff, fderiv_norm_rpow, Affine.Simplex.circumsphere_reindex, Orientation.inner_smul_rotation_pi_div_two_smul_right, CircleIntegrable.out, RCLike.intervalIntegral_ofReal, Icc_mem_vitaliFamily_at_right, ConcaveOn.le_map_set_average, EuclideanGeometry.Sphere.direction_orthRadius, hasDerivAt_fourierIntegral, Complex.rightAngleRotation, EuclideanGeometry.dist_sq_add_dist_sq_eq_two_mul_dist_midpoint_sq_add_half_dist_sq, EuclideanGeometry.inner_pos_of_dist_lt_radius, Affine.Simplex.circumradius_reindex, AnalyticOn.re_ofReal, AffineSubspace.signedInfDist_apply_self, integral_sin_sq_mul_cos_sq, ProbabilityTheory.covarianceBilinDual_of_not_memLp, integral_mul_rpow_one_add_sq, InnerProductGeometry.angle_eq_pi_iff, deriv_circleMap_eq_zero_iff, MeasureTheory.charFun_map_eq_charFunDual_smul, inner_vsub_vsub_left_eq_dist_sq_left_iff, NumberField.mixedEmbedding.normAtAllPlaces_mixedSpaceOfRealSpace, ProbabilityTheory.condVar_ae_eq_condExp_sq_sub_sq_condExp, NumberField.mixedEmbedding.det_fderivPolarCoordRealSymm, abs_integral_sub_setIntegral_mulExpNegMulSq_comp_lt, PeriodPair.indep, fourierInv_eq, ProperCone.innerDual_iUnion, SchwartzMap.tsum_eq_tsum_fourierIntegral, ProbabilityTheory.uncenteredCovarianceBilinDual_apply, Orientation.kahler_rightAngleRotation_right, MeasureTheory.condExpIndSMul_ae_eq_smul, Quaternion.linearIsometryEquivTuple_apply, EuclideanGeometry.Sphere.orthRadius_parallel_orthRadius_iff, MeasureTheory.intervalIntegrable_charFun, InnerProductGeometry.inner_eq_cos_angle_of_norm_eq_one, integral_Iic_inv_one_add_sq, SmoothPartitionOfUnity.toPartitionOfUnity_toFun, ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_integral_of_monotone, EuclideanGeometry.inner_vsub_vsub_of_mem_sphere_of_mem_sphere, SmoothPartitionOfUnity.contMDiff_smul, ProbabilityTheory.condIndepFun_iff, compact_inner_le_weight_mul_Lp_of_nonneg, Affine.Triangle.sSameSide_affineSpan_pair_excenter_singleton_point, MeasureTheory.charFun_eq_integral_innerProbChar, instNonemptySeedRatReal, SchwartzMap.instFourierInvSMul, TemperedDistribution.derivCLM_apply_apply, integral_cos_sq, abs_signedDist_le_dist, Orientation.norm_kahler, NumberField.mixedEmbedding.disjoint_span_commMap_ker, mfderiv_subtype_coe_Icc_one, Complex.isometryOfOrthonormal_symm_apply, integral_rpowIntegrand₀₁_eq_rpow_mul_const, intervalIntegral.integral_hasFDerivAt, ProperCone.innerDual_toSubmodule, Orientation.inner_rightAngleRotation_self, ValueDistribution.proximity_coe, Affine.Triangle.dist_div_sin_oangle_div_two_eq_circumradius, MeasureTheory.tendsto_iff_forall_lipschitz_integral_tendsto, intervalIntegral.fderiv_integral, ProbabilityTheory.gaussianReal_apply_eq_integral, EuclideanGeometry.affineIndependent_iff_of_two_zsmul_oangle_eq, eventually_norm_trivializationAt_lt, ProbabilityTheory.IsGaussian.charFunDual_eq', OrthonormalBasis.addHaar_eq_volume, OrthonormalBasis.det_to_matrix_orthonormalBasis_real, MeasureTheory.integral_prod_smul, ProbabilityTheory.condExp_eq_zero_or_one_of_condIndepSet_self, ProbabilityTheory.IsRatCondKernelCDFAux.setIntegral, hasDerivAt_Gamma_nat, Orientation.oangle_smul_right_self_of_nonneg, HasStrictFDerivAt.inner, MeasureTheory.ContinuousMap.inner_toLp, differentiableAt_abs, ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat_rat, LipschitzWith.integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul', intervalIntegral.norm_integral_le_abs_of_norm_le, ProbabilityTheory.analyticAt_iteratedDeriv_mgf, ProbabilityTheory.isPositive_covarianceOperator, Affine.Simplex.reflection_circumcenter_eq_affineCombination_of_pointsWithCircumcenter, logDeriv_cos, Orientation.inner_rev_eq_zero_of_oangle_eq_pi_div_two, Affine.Simplex.height_reindex, ProbabilityTheory.charFun_gaussianReal, exists_eq_interval_average, exists_smooth_zero_one_nhds_of_isClosed, DifferentiableOn.norm, Affine.Simplex.inradius_map, Complex.map_isometryOfOrthonormal, integral_exp_Iic_zero, TemperedDistribution.fourierTransformInv_apply, Orientation.oangle_neg_orientation_eq_neg, Orientation.oangle_sign_smul_add_smul_left, ContDiffOn.norm, logDeriv_cosh, EuclideanGeometry.Sphere.secondInter_eq_lineMap, SchwartzMap.integral_clm_comp_laplacian_right_eq_left, ProbabilityTheory.IndepFun.charFun_map_add_eq_mul, fourierInv_eq', signedDist_apply_linear, EuclideanGeometry.Sphere.secondInter_map, Bundle.RiemannianMetric.continuousAt, MeasureTheory.charFun_zero, continuous_stereoInvFun, parallelepiped_orthonormalBasis_one_dim, EuclideanGeometry.Sphere.isDiameter_iff_left_mem_and_midpoint_eq_center, norm_sub_mul_self_real, integral_log_from_zero, MeasureTheory.integrable_mconv_iff, VectorFourier.norm_fourierIntegral_le_integral_norm, EuclideanGeometry.Sphere.angle_eq_pi_div_two_iff_mem_sphere_ofDiameter, Orientation.inner_rev_eq_zero_of_oangle_eq_neg_pi_div_two, deriv_log_comp_eq_logDeriv, real_inner_smul_self_right, Manifold.exists_lt_of_riemannianEDist_lt, MeasureTheory.integral_abs_condExp_le, InnerProductGeometry.sin_angle_add, StrictConvexOn.ae_eq_const_or_map_average_lt, MeasureTheory.norm_charFun_le, VectorFourier.hasFDerivAt_fourierChar_smul, OrthonormalBasis.measurePreserving_measurableEquiv, Orientation.rotation_pi, fourierIntegral_real_eq, InformationTheory.not_differentiableAt_klFun_zero, PeriodPair.lattice_eq_span_range_basis, MeasureTheory.measurable_charFun, MeasureTheory.measure_unitBall_eq_integral_div_gamma, integral_cos_sq_sub_sin_sq, ProbabilityTheory.variance_tilted_mul, MeasureTheory.le_integral_rnDeriv_of_ac, ContinuousOn.inner_bundle, AffineSubspace.mem_perpBisector_pointReflection_iff_inner_eq_zero, SmoothBumpCovering.embeddingPiTangent_coe, real_inner_comm, SchwartzMap.integral_smul_deriv_right_eq_neg_left, SmoothPartitionOfUnity.nonneg', ProbabilityTheory.covarianceBilinDual_of_not_memLp', Affine.Triangle.orthocenter_vsub_circumcenter_eq_sum_vsub, Function.hasTemperateGrowth_one_add_norm_sq_rpow, Orientation.two_zsmul_oangle_smul_smul_self, SchwartzMap.fourier_convolution, tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn, ContDiffWithinAt.norm, Complex.log_inv_eq_integral, SmoothPartitionOfUnity.IsSubordinate.contMDiff_finsum_smul, Orientation.rotation_symm_apply, AbsolutelyContinuousOnInterval.integral_mul_deriv_eq_deriv_mul, ProbabilityTheory.analyticOn_iteratedDeriv_mgf, MeasureTheory.Integrable.integral_norm_condKernel, Affine.Simplex.altitudeFoot_mem_affineSpan_faceOpposite, InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two, intervalIntegral.inv_mul_integral_comp_div_add, OrthonormalBasis.abs_det_adjustToOrientation, EuclideanGeometry.inversion_eq_lineMap, Complex.integral_cpow_mul_exp_neg_mul_Ioi, inner_eq_norm_sq_right_iff, norm_fderiv_norm_id_rpow, NumberField.Units.basisOfIsMaxRank_fundSystem, NumberField.mixedEmbedding.fundamentalCone.linearIndependent_completeFamily, intervalIntegral.norm_integral_le_integral_norm_uIoc, MeasureTheory.charFun_map_const_add, Affine.Triangle.dist_orthocenter_reflection_circumcenter_finset, Affine.Simplex.affineSpan_pair_eq_altitude_iff, MeasureTheory.charFun_eq_pi_iff, AffineIsometry.angle_map, NumberField.mixedEmbedding.commMap_canonical_eq_mixed, Orientation.rotation_oangle_eq_iff_norm_eq, Affine.Simplex.signedInfDist_apply_of_ne, integral_cos_mul_complex, exists_contMDiffMap_one_nhds_of_subset_interior, signedDist_left_lineMap, Affine.Simplex.direction_altitude, DifferentiableWithinAt.inner, NumberField.mixedEmbedding.norm_negAt, Orientation.oangle_sign_smul_sub_right, SmoothPartitionOfUnity.sum_le_one, VectorFourier.fourierIntegral_fderiv, ProbabilityTheory.HasCondSubgaussianMGF.ae_trim_condExp_le, IccRightChart_extend_top, ModularFormClass.qExpansion_coeff_eq_intervalIntegral, UnitAddCircle.integral_preimage, integral_one_div_of_neg, Affine.Simplex.circumcenter_eq_centroid, fourierIntegralInv_eq, ContDiffBump.convolution_tendsto_right_of_continuous, Affine.Simplex.excenter_reindex, Complex.approx_Gamma_integral_tendsto_Gamma_integral, MeasureTheory.Lp.fourier_toTemperedDistribution_eq, fderivInnerCLM_apply, intervalIntegral.integral_lt_integral_of_ae_le_of_measure_setOf_lt_ne_zero, eventually_norm_mfderiv_extChartAt_lt, ContMDiffWithinAt.inner_bundle, ProbabilityTheory.HasGaussianLaw.charFunDual_map_eq, MeasureTheory.Integrable.integral_eq_integral_Ioc_meas_le, Affine.Simplex.ninePointCircle_center, EuclideanGeometry.dist_orthogonalProjection_line_eq_of_two_zsmul_oangle_eq, boundary_Icc, MeasureTheory.charFun_prod, EuclideanGeometry.inner_vsub_vsub_of_dist_eq_of_dist_eq, SchwartzMap.toLp_fourier_eq, MeasureTheory.tendsto_integral_meas_thickening_le, VectorFourier.norm_fourierPowSMulRight_iteratedFDeriv_fourierIntegral_le, fderiv_fourierChar_neg_bilinear_left_apply, hasContDiffBump_of_innerProductSpace, exists_measure_rpow_eq_integral, fourierIntegral_continuousMultilinearMap_apply', InnerProductGeometry.sin_angle_mul_norm_mul_norm, ValueDistribution.proximity_top, Affine.Triangle.sSameSide_affineSpan_pair_incenter_point, fourier_eq', differentiable_fourier, ProbabilityTheory.integrable_comp_iff, MeasureTheory.lpMeasToLpTrimLie_symm_toLp, MeasureTheory.lintegral_comp_eq_lintegral_meas_lt_mul, integral_sin_pow_antitone, Matrix.PosDef.posDef_sqrt, integral_pow_abs_sub_uIoc, circleAverage_nonneg_of_nonneg, EuclideanSpace.volume_closedBall, Orientation.rightAngleRotation_neg_orientation, Orientation.rotationAux_apply, intervalIntegral.integral_nonneg_of_forall, Affine.Simplex.centroid_eq_affineCombination_of_pointsWithCircumcenter, InformationTheory.deriv_klFun, one_add_rpow_hasFPowerSeriesOnBall_zero, AnalyticOnNhd.im_ofReal, boundary_product, Manifold.exists_lt_locally_constant_of_riemannianEDist_lt, differentiable_sigmoid, Orientation.cos_oangle_eq_inner_div_norm_mul_norm, NumberField.mixedEmbedding.normAtPlace_mixedSpaceOfRealSpace, Affine.Simplex.incenter_notMem_affineSpan_faceOpposite, Affine.Simplex.touchpoint_empty_mem_interior_faceOpposite, LindemannWeierstrass.hasDerivAt_cexp_mul_sumIDeriv, SchwartzMap.laplacian_apply, MeasureTheory.charFun_map_smul, ProbabilityTheory.IsGaussian.eq_gaussianReal, one_div_sub_sq_hasFPowerSeriesOnBall_zero, real_inner_self_pos, ProbabilityTheory.uncenteredCovarianceBilinDual_zero, ProbabilityTheory.integral_tilted_mul_self, LSeries_eq_mul_integral', integrableOn_Ioi_deriv_norm_ofReal_cpow, AffineSubspace.right_mem_perpBisector, EuclideanGeometry.Sphere.dist_orthogonalProjection_eq_radius_iff_isTangentAt, intervalIntegral.integral_mul_const, AbsolutelyContinuousOnInterval.intervalIntegrable_deriv, ProbabilityTheory.cdf_gammaMeasure_eq_integral, MeasureTheory.integral_comap_eq_mulEquivHaarChar_smul, fourier_gaussian_pi, Function.Periodic.tendsto_atTop_intervalIntegral_of_pos', EuclideanGeometry.Sphere.mem_orthRadius_iff_inner_left, not_differentiableAt_abs_zero, MonotoneOn.ae_differentiableWithinAt, TemperedDistribution.laplacianCLM_apply, EuclideanGeometry.Sphere.secondInter_eq_self_iff, SchwartzMap.instFourierAdd, ValueDistribution.proximity_sub_proximity_inv_eq_circleAverage, continuousAt_gaussian_integral, ProperCone.innerDual_innerDual, NumberField.mixedEmbedding.fundamentalCone.expMap_basis_of_ne, Orientation.areaForm_rightAngleRotation_left, Differentiable.norm, deriv_fourier, contDiff_sigmoid, LinearIsometry.angle_map, NumberField.mixedEmbedding.disjoint_negAt_plusPart, DifferentiableAt.dist, IccLeftChart_extend_bot_mem_frontier, fderiv_norm_sq_apply, LipschitzWith.ae_differentiableAt_real, EuclideanGeometry.Sphere.finrank_orthRadius, NumberField.mixedEmbedding.volume_fundamentalDomain_stdBasis, EulerSine.integral_cos_mul_cos_pow_even, InnerProductGeometry.inner_eq_mul_norm_iff_angle_eq_zero, Icc_isBoundaryPoint_top, integral_sin_pow_even, Affine.Simplex.points_vsub_eulerPoint, MeasureTheory.condExp_mul_of_stronglyMeasurable_left, InnerProductGeometry.angle_smul_left_of_pos, Orientation.measure_orthonormalBasis, Affine.Simplex.ExcenterExists.sSameSide_excenter_point_iff, fderiv_norm_sq, MeasureTheory.addEquivAddHaarChar_smul_integral_map, Complex.ofReal_choose, inner_vsub_vsub_right_eq_dist_sq_right_iff, real_inner_mem_Icc_of_norm_eq_one, MeasureTheory.charFun_eq_integral_probChar, Orientation.inner_mul_inner_add_areaForm_mul_areaForm', ContDiffOn.dist, EuclideanGeometry.angle_eq_pi_iff_sbtw, MDifferentiable.inner_bundle, conformalAt_iff', surjective_stereographic, fourierIntegral_gaussian_pi', hasDerivAt_abs_pos, Orientation.oangle_smul_left_of_pos, hasFDerivAt_stereoInvFunAux_comp_coe, LipschitzWith.integral_lineDeriv_mul_eq, Affine.Triangle.dist_point_centroid, integral_gaussian_complex_Ioi, MeasureTheory.condExpL2_indicator_nonneg, Affine.Triangle.orthocenter_reindex, HasCompactSupport.hasFDerivAt_convolution_left, Affine.Simplex.circumradius_map, MeasureTheory.charFun_map_add_const, instIsManifoldIcc, Bundle.ContinuousRiemannianMetric.isVonNBounded, Matrix.PosSemidef.sqrt_eq_iff_eq_sq, TemperedDistribution.smulLeftCLM_apply_apply, NumberField.mixedEmbedding.mem_rat_span_latticeBasis, RCLike.restrict_toContinuousMap_eq_toContinuousMapStar_restrict, ProbabilityTheory.hasSubgaussianMGF_of_mem_Icc, Orientation.inner_mul_areaForm_sub, ProbabilityTheory.integral_preCDF_fst, fderiv_inner_apply, SmoothBumpCovering.toSmoothPartitionOfUnity_zero_of_zero, contDiffAt_abs, ProbabilityTheory.covarianceOperator_of_not_memLp, MeasureTheory.Integrable.uniformIntegrable_condExp, SmoothPartitionOfUnity.contMDiff_sum, EuclideanGeometry.Sphere.infDist_eq_radius_iff_isTangent, Affine.Simplex.altitude_def, contMDiffOn_projIcc, NumberField.mixedEmbedding.fundamentalCone.logMap_normAtAllPlaces, ContDiffBump.integral_pos, NumberField.mixedEmbedding.fundamentalCone.normAtAllPlaces_normLeOne, Complex.rotation, Metric.exists_contMDiffMap_forall_closedEBall_subset, BoxIntegral.unitPartition.tag_mem_smul_span, signedDist_vadd_vadd, parallelepiped_single, contMDiff_circleExp, SchwartzMap.tsum_eq_tsum_fourier, NumberField.mixedEmbedding.normAtAllPlaces_normAtAllPlaces, ProbabilityTheory.IndepFun.integral_mul_eq_mul_integral, hasFDerivAt_integral_of_dominated_loc_of_lip, EuclideanGeometry.Sphere.self_mem_orthRadius, intervalIntegral.norm_integral_le_of_norm_le, Affine.Simplex.insphere_reindex, PeriodPair.instIsZLatticeRealComplexLattice, GaussianFourier.integral_rexp_neg_mul_sq_norm, tendsto_Icc_vitaliFamily_right, RCLike.map_to_real, intervalIntegral.differentiableOn_integral_of_continuous, differentiable_circleMap, norm_eq_sqrt_real_inner, Affine.Simplex.sSameSide_point_incenter, AnalyticAt.im_ofReal, intervalIntegral.integral_nonneg, NumberField.mixedEmbedding.mixedSpaceOfRealSpace_apply, LinearIsometryEquiv.coe_symm_toMeasurableEquiv, ProbabilityTheory.analyticOnNhd_iteratedDeriv_mgf, Orientation.abs_volumeForm_apply_le, Affine.Simplex.ExcenterExists.sSameSide_point_excenter_iff, intervalIntegral.mul_integral_comp_mul_left, Affine.Simplex.signedInfDist_incenter, Affine.Simplex.inner_vsub_vsub_altitudeFoot_eq_height_sq
|