StrongDual 📖 | CompOp | 266 mathmath: geometric_hahn_banach_open, HasStrictFDerivAt.log, NormedSpace.isBounded_polar_of_mem_nhds_zero, HasFDerivWithinAt.ccosh, RCLike.geometric_hahn_banach_point_open, HasFDerivWithinAt.ccos, InnerProductSpace.toLinearIsometry_toDual, geometric_hahn_banach_point_point, hasFDerivAt_iff_hasGradientAt, RCLike.reCLM_apply, RCLike.separate_convex_open_set, HasStrictFDerivAt.csin, NormedSpace.Dual.isClosed_image_polar_of_mem_nhds, ProbabilityTheory.covarianceBilinDual_apply', MeasureTheory.charFunDual_apply, ProbabilityTheory.hasGaussianLaw_iff_charFunDual_map_eq, IsLocalMaxOn.hasFDerivWithinAt_nonpos, ProbabilityTheory.IsGaussian.integrable_dual, geometric_hahn_banach_open_point, StrongDual.polarSubmodule_eq_setOf, ContinuousLinearMapWOT.withSeminorms, ProbabilityTheory.covarianceBilinDual_apply, ProbabilityTheory.IsGaussian.map_eq_gaussianReal, ContinuousLinearEquiv.coe_toSpanNonzeroSingleton_symm, ProbabilityTheory.uncenteredCovarianceBilin_apply, LipschitzWith.ae_exists_fderiv_of_countable, InnerProductSpace.toDual_symm_apply, MeasureTheory.charFun_toDual_symm_eq_charFunDual, exposed_point_def, ContinuousLinearMap.norm_extendTo𝕜, geometric_hahn_banach_compact_closed, HasFDerivWithinAt.csin, NormedSpace.Dual.toWeakDual_continuous, RCLike.reCLM_norm, RCLike.geometric_hahn_banach_closed_point, SeparatingDual.exists_eq_one, NormedSpace.isClosed_polar, MeasureTheory.charFunDual_eq_charFun_map_one, ContinuousLinearMapWOT.le_nhds_iff_forall_dual_apply_le_nhds, HasFDerivAt.arctan, HasStrictFDerivAt.abs, HasStrictFDerivAt.arsinh, HasFDerivWithinAt.exp, ContinuousLinearMapWOT.inducingFn_apply, InnerProductSpace.toDualMap_apply_apply, HasStrictFDerivAt.hasStrictDerivAt_norm_smul_neg, WeakDual.toStrongDual_inj, StrongDual.toWeakDual_inj, WeakDual.coe_toStrongDual, NormedSpace.eq_zero_iff_forall_dual_eq_zero, ProbabilityTheory.uncenteredCovarianceBilinDual_of_not_memLp, hasGradientWithinAt_iff_hasFDerivWithinAt, NormedSpace.inclusionInDoubleDual_norm_eq, tendsto_integral_exp_smul_cocompact, HasFDerivWithinAt.abs_of_neg, LinearMap.toLinearMap_toContPerfPair, ContinuousLinearMap.norm_smulRightL, NormedSpace.eq_iff_forall_dual_eq, HasFDerivWithinAt.hasGradientWithinAt, HasFDerivWithinAt.cpow, StrongDual.toLp_of_not_memLp, HasStrictFDerivAt.const_cpow, HasFDerivWithinAt.csinh, NormedSpace.inclusionInDoubleDual_norm_le, HasFDerivAt.abs, WeakDual.isCompact_closedBall, HasStrictFDerivAt.abs_of_neg, HasFDerivWithinAt.abs, InnerProductSpace.toDual_apply, ProbabilityTheory.covarianceBilinDual_eq_covariance, ProbabilityTheory.covarianceBilinDual_zero, NormedSpace.polar_ball_subset_closedBall_div, InnerProductSpace.toDualMap_apply, geometric_hahn_banach_point_closed, HasStrictFDerivAt.clog, HasStrictFDerivAt.sqrt, HasStrictFDerivAt.rpow, InnerProductSpace.toDual_apply_apply, ContinuousLinearMap.adjointAux_apply, IsLocalMinOn.hasFDerivWithinAt_nonneg, ContinuousLinearMap.norm_smulRight_apply, HasStrictFDerivAt.ccos, ContinuousLinearMapWOT.isInducing_inducingFn, StrongDual.polarSubmodule_eq_polar, RCLike.geometric_hahn_banach_point_point, ContinuousLinearMapWOT.hasBasis_seminorms, IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt, IsLocalMinOn.hasFDerivWithinAt_eq_zero, ProperCone.hyperplane_separation_point, IsLocalMax.hasFDerivAt_eq_zero, WeakDual.isSeqCompact_closedBall, HasFDerivAt.ccos, HasFDerivWithinAt.log, HasFDerivAt.clog, BoundedContinuousFunction.probCharDual_zero, HasGradientAt.hasFDerivAt, ContinuousLinearMapWOT.isEmbedding_inducingFn, ProperCone.dual_singleton, HasFDerivAt.ccosh, exists_dual_vector, HasFDerivAt.abs_of_neg, ProbabilityTheory.IsGaussian.charFunDual_eq, ProbabilityTheory.covarianceBilin_eq_covarianceBilinDual, HasStrictFDerivAt.arctan, LinearPMap.adjointDomainMkCLM_apply, iInter_halfSpaces_eq, geometric_hahn_banach_closed_compact, ProbabilityTheory.covarianceBilinDual_self_eq_variance, geometric_hahn_banach_open_open, tendsto_integral_exp_smul_cocompact_of_inner_product, InnerProductSpace.nullSubmodule_le_ker_toDualMap_left, HasFDerivWithinAt.sinh, exists_dual_vector'', ProbabilityTheory.IsGaussian.memLp_dual, ProbabilityTheory.covarianceBilinDual_self_nonneg, HasFDerivAt.log, MeasureTheory.charFunDual_map_const_add, MeasureTheory.charFunDual_map_add_const, HasFDerivAt.exp, ContinuousLinearMap.norm_extendTo𝕜'_bound, IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt_1d, WeakDual.isClosed_closedBall, ContinuousLinearEquiv.coord_toSpanNonzeroSingleton, IsLocalExtrOn.exists_linear_map_of_hasStrictFDerivAt, ProbabilityTheory.isGaussian_iff_gaussian_charFunDual, ProbabilityTheory.norm_uncenteredCovarianceBilinDual_le, StrongDual.toLpₗ_apply, HasFDerivWithinAt.rpow_const, IsLocalExtrOn.linear_dependent_of_hasStrictFDerivAt, ContinuousLinearEquiv.toSpanNonzeroSingleton_coord, ContinuousLinearMap.extendTo𝕜_apply, HasFDerivAt.sinh, ProbabilityTheory.IsGaussian.integral_dual, ContinuousLinearMap.norm_extendTo𝕜', StrongDual.polar_univ, HasFDerivWithinAt.clog, hasGradientAt_iff_hasFDerivAt, ProbabilityTheory.IndepFun.charFunDual_map_add_eq_mul, HasFDerivAt.rpow_const, coord_norm', ContinuousLinearMapWOT.ext_dual_iff, HasStrictFDerivAt.const_rpow, StrongDual.norm_toLpₗ_le, HasStrictFDerivAt.cos, HasFDerivWithinAt.arsinh, geometric_hahn_banach_point_open, StrongDual.toLpₗ_of_not_memLp, StrongDual.mem_polarSubmodule, exists_dual_vector', MeasureTheory.measureReal_abs_dual_gt_le_integral_charFunDual, separate_convex_open_set, RCLike.geometric_hahn_banach_open, HasFDerivAt.sin, HasFDerivAt.csin, WStarAlgebra.exists_predual, IsExposed.eq_inter_halfSpace, ProbabilityTheory.isPosSemidef_covarianceBilinDual, HasFDerivAt.hasFDerivAt_norm_smul, AlgHom.coe_toContinuousLinearMap, HasFDerivWithinAt.sqrt, SeparatingDual.exists_eq_one_ne_zero_of_ne_zero_pair, NormedSpace.polar_ball, InnerProductSpace.toContinuousLinearMap_toDualMap, HasFDerivWithinAt.const_cpow, WeakDual.CharacterSpace.norm_le_norm_one, InnerProductSpace.toDual_apply_eq_toDualMap_apply, ProbabilityTheory.variance_dual_prod', HasFDerivWithinAt.arctan, ProbabilityTheory.covarianceBilinDual_comm, ProbabilityTheory.isGaussian_iff_charFunDual_eq, HasFDerivWithinAt.rpow, MeasureTheory.charFun_eq_charFunDual_toDualMap, NormedSpace.Dual.dual_norm_topology_le_weak_dual_topology, NormedSpace.sInter_polar_eq_closedBall, HasFDerivAt.cos, ProbabilityTheory.uncenteredCovarianceBilin_of_not_memLp, ProbabilityTheory.HasGaussianLaw.charFunDual_map_eq_fun, HasFDerivAt.const_rpow, ContinuousLinearMap.nnnorm_smulRight_apply, HasFDerivAt.arsinh, StrongDual.zero_mem_polar, ContinuousLinearMapWOT.continuous_inducingFn, LinearPMap.adjointDomainMkCLMExtend_apply, HasStrictFDerivAt.cpow, hasFDerivWithinAt_iff_hasGradientWithinAt, ProbabilityTheory.uncenteredCovarianceBilin_zero, LinearMap.toContPerfPair_apply, MeasureTheory.charFunDual_dirac, AlgHom.toContinuousLinearMap_norm, HasFDerivAt.hasFDerivAt_norm_smul_neg, StrongDual.toLp_apply, StrongDual.polar_empty, IsLocalMin.hasFDerivAt_eq_zero, exists_extension_norm_eq, NormedSpace.closedBall_inv_subset_polar_closedBall, ProbabilityTheory.IsGaussian.integral_dual_conv_map_neg_eq_zero, ContinuousLinearMap.norm_smulRightL_le, ProbabilityTheory.IsGaussian.charFunDual_eq_of_integral_eq_zero, ProbabilityTheory.variance_dual_prod, HasFDerivAt.hasGradientAt, HasStrictFDerivAt.sin, HasFDerivWithinAt.const_rpow, ContinuousLinearMap.extendTo𝕜'_apply, HasStrictFDerivAt.hasStrictFDerivAt_norm_smul, ProbabilityTheory.norm_uncenteredCovarianceBilin_le, ContinuousLinearEquiv.coord_norm', IsLocalMaxOn.hasFDerivWithinAt_eq_zero, StrongDual.coe_toWeakDual, WeakDual.toStrongDual_apply, geometric_hahn_banach_closed_point, HasFDerivAt.sqrt, HasFDerivAt.csinh, RCLike.iInter_halfSpaces_eq, StrongDual.polar_zero, ProperCone.hyperplane_separation, StrongDual.mem_polar_iff, ContinuousLinearEquiv.coord_self, RCLike.geometric_hahn_banach_compact_closed, HasStrictFDerivAt.ccosh, ContinuousLinearEquiv.coord_norm, HasStrictFDerivAt.cosh, RCLike.geometric_hahn_banach_point_closed, NormedSpace.polar_closedBall, IsExposed.eq_inter_halfSpace', ProbabilityTheory.covarianceBilinDual_of_not_memLp, MeasureTheory.charFun_map_eq_charFunDual_smul, NormedSpace.double_dual_bound, Real.zero_at_infty_vector_fourierIntegral, ProbabilityTheory.uncenteredCovarianceBilinDual_apply, HasStrictFDerivAt.sinh, HasFDerivAt.cpow, ProbabilityTheory.IsGaussian.charFunDual_eq', StrongDual.polar_singleton, HasFDerivAt.cosh, ContinuousLinearMap.isOpenMap_of_ne_zero, ContinuousLinearMapWOT.continuous_dual_apply, StrongDual.mem_polar_singleton, HasStrictFDerivAt.csinh, HasFDerivWithinAt.cos, Real.exists_extension_norm_eq, ProbabilityTheory.covarianceBilinDual_of_not_memLp', HasGradientWithinAt.hasFDerivWithinAt, NormedSpace.Dual.coe_toWeakDual, ContinuousLinearMap.smulRightL_apply_apply, ProbabilityTheory.HasGaussianLaw.charFunDual_map_eq, IsLocalExtr.hasFDerivAt_eq_zero, RCLike.geometric_hahn_banach_closed_compact, ContinuousLinearMapWOT.tendsto_iff_forall_dual_apply_tendsto, NormedSpace.Dual.toWeakDual_inj, RCLike.re_extendTo𝕜'ₗ, ProbabilityTheory.uncenteredCovarianceBilinDual_zero, HasFDerivAt.rpow, ContinuousLinearMap.norm_smulRightL_apply, HasFDerivWithinAt.sin, HasStrictFDerivAt.exp, RCLike.imCLM_apply, domain_mvt, StrongDual.polar_nonempty, NormedSpace.dual_def, RCLike.geometric_hahn_banach_open_open, InnerProductSpace.nullSubmodule_le_ker_toDualMap_right, BoundedContinuousFunction.probCharDual_apply, HasFDerivAt.const_cpow, HasFDerivWithinAt.cosh, HasStrictFDerivAt.rpow_const, RCLike.geometric_hahn_banach_open_point
|