Convex

2 Example

Here you can use LaTex.

Definition 2.1 ✓
#

Lean declarations

No documentation.

Theorem 2.2 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.3 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.4 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.5 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Definition 2.6 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Definition 2.8 ✓
#

Uses

Lean declarations

No documentation.

Theorem 2.9 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Definition 2.10 ✓
#

Lean declarations

No documentation.

Lemma 2.11 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.12 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Lemma 2.13 ✓
#

Lean declarations

No documentation.

Proof ▼
Lemma 2.14 ✓
#

Lean declarations

No documentation.

Proof ▼
Lemma 2.15 ✓
#

Lean declarations

No documentation.

Proof ▼
Lemma 2.16 ✓
#

Lean declarations

No documentation.

Proof ▼
Lemma 2.17 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.18 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Lemma 2.19 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Lemma 2.20 ✓
#

Lean declarations

No documentation.

Proof ▼
Lemma 2.21 ✓
#

Lean declarations

No documentation.

Proof ▼
Proof ▼
Lemma 2.23 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.25 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.26 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.27 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.28 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Definition 2.29 ✓
#

Uses

Lean declarations

No documentation.

Theorem 2.30 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.31 ✓
#

Uses

Lean declarations

convergence with fixed step size -

Proof ▼
Theorem 2.32 ✓
#

Uses

Lean declarations

convergence with fixed \(‖x^{i+1}-x^{i}‖\) -

Proof ▼
Theorem 2.33 ✓
#

Uses

Lean declarations

convergence with diminishing step size -

Proof ▼
Definition 2.34 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Definition 2.36 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Definition 2.38 ✓
#

Uses

Lean declarations

No documentation.

Theorem 2.39 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.40 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Lemma 2.41 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Lemma 2.42 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Lemma 2.43 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Lemma 2.44 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Lemma 2.45 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Definition 2.46 ✓
#

Lean declarations

No documentation.

Definition 2.47 ✓
#

Uses

Lean declarations

No documentation.

Lemma 2.48 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Lemma 2.49 ✓
#

Lean declarations

No documentation.

Proof ▼
Lemma 2.50 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Lemma 2.51 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Definition 2.52 ✓
#

Uses

Lean declarations

Subgradient of functions -

Definition 2.53 ✓
#

Uses

Lean declarations

No documentation.

Definition 2.54 ✓
#

Uses

Lean declarations

Subderiv of functions -

Definition 2.55 ✓
#

Uses

Lean declarations

No documentation.

Definition 2.56 ✓
#

Lean declarations

No documentation.

Lemma 2.57 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Lemma 2.58 ✓
#

Lean declarations

No documentation.

Proof ▼
Theorem 2.59 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.60 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Definition 2.61 ✓
#

Lean declarations

Subgradient of functions -

Definition 2.62 ✓
#

Lean declarations

No documentation.

Definition 2.63 ✓
#

Uses

Lean declarations

Subderiv of functions -

Definition 2.64 ✓
#

Uses

Lean declarations

No documentation.

Theorem 2.65 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.66 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.67 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.68 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.69 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.70 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Proof ▼
Proof ▼
Theorem 2.73 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.74 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.75 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.76 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.77 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.78 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.79 ✓
#

Uses

Lean declarations

The subderiv of ‘f‘ at ‘x‘ is a closed set. -

Proof ▼
Theorem 2.80 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.81 ✓
#

Uses

Lean declarations

The subderiv of ‘f‘ at ‘x‘ is a convex set. -

Proof ▼
Theorem 2.82 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.83 ✓
#

Uses

Lean declarations

Monotonicity of subderiv-

Proof ▼
Theorem 2.84 ✓
#

Uses

Lean declarations

Subderiv of differentiable convex functions -

Proof ▼
Theorem 2.85 ✓
#

Uses

Lean declarations

Alternarive version for FDeriv -

Proof ▼
Theorem 2.86 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.87 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.88 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.89 ✓
#

Uses

Lean declarations

‘x’‘ minimize ‘f‘ if and only if ‘0‘ is a subgradient of ‘f‘ at ‘x’‘ -

Proof ▼
Theorem 2.90 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.91 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.92 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.93 ✓
#

Uses

Lean declarations

Multiplication by a Positive Scalar-

Proof ▼
Theorem 2.94 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.95 ✓
#

Uses

Lean declarations

Subderivatives of the sum of two functions is a subset of the sum of the subderivatives of the two functions -

Proof ▼
Theorem 2.96 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.97 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.98 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Definition 2.99 ✓
#

Lean declarations

No documentation.

Definition 2.100 ✓
#

Uses

Lean declarations

No documentation.

Definition 2.101 ✓
#

Uses

Lean declarations

No documentation.

Lemma 2.102 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Lemma 2.103 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.104 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Proof ▼
Theorem 2.106 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.107 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.108 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Definition 2.109 ✓
#

Uses

Lean declarations

No documentation.

Definition 2.110 ✓
#

Uses

Lean declarations

No documentation.

Lemma 2.111 ✓
#

Lean declarations

No documentation.

Proof ▼
Lemma 2.112 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Proof ▼
Theorem 2.114 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Proof ▼
Theorem 2.116 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.117 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.118 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.119 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.120 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.121 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.122 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.123 ✓
#

Lean declarations

No documentation.

Proof ▼
Theorem 2.124 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.125 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.126 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.127 ✓
#

Lean declarations

No documentation.

Proof ▼
Theorem 2.128 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.129 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.130 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.131 ✓
#

Lean declarations

No documentation.

Proof ▼
Theorem 2.132 ✓
#

Lean declarations

No documentation.

Proof ▼
Theorem 2.133 ✓
#

Lean declarations

No documentation.

Proof ▼
Theorem 2.134 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.135 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.136 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.137 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.138 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.139 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.140 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.141 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.142 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.143 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.144 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.145 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.146 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.147 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.148 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.149 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.150 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.151 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.152 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.153 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.154 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Definition 2.155 ✓
#

Lean declarations

No documentation.

Theorem 2.156 ✓
#

Lean declarations

No documentation.

Proof ▼
Theorem 2.157 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.158 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.159 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Lemma 2.160 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.161 ✓
#

Lean declarations

No documentation.

Proof ▼
Theorem 2.162 ✓
#

Lean declarations

No documentation.

Proof ▼
Theorem 2.163 ✓
#

Lean declarations

No documentation.

Proof ▼
Theorem 2.164 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.165 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.166 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.167 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.168 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.169 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Lemma 2.170 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Lemma 2.171 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Lemma 2.172 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Lemma 2.173 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Lemma 2.174 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Lemma 2.175 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Lemma 2.176 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Lemma 2.177 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.178 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Lemma 2.179 ✓
#

Lean declarations

No documentation.

Proof ▼
Lemma 2.180 ✓
#

Lean declarations

No documentation.

Proof ▼
Lemma 2.181 ✓
#

Lean declarations

No documentation.

Proof ▼
Lemma 2.182 ✓
#

Lean declarations

No documentation.

Proof ▼
Lemma 2.183 ✓
#

Lean declarations

No documentation.

Proof ▼
Theorem 2.184 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.185 ✓
#

Lean declarations

No documentation.

Proof ▼
Theorem 2.186 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.187 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.188 ✓
#

Lean declarations

No documentation.

Proof ▼
Theorem 2.189 ✓
#

Uses

Lean declarations

The chain rule.

Proof ▼
Theorem 2.190 ✓
#

Lean declarations

No documentation.

Proof ▼
Theorem 2.191 ✓
#

Lean declarations

No documentation.

Proof ▼
Theorem 2.192 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.193 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.194 ✓
#

Lean declarations

No documentation.

Proof ▼
Theorem 2.195 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.196 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.197 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.198 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.199 ✓
#

Lean declarations

No documentation.

Proof ▼
Theorem 2.200 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.201 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.202 ✓
#

Lean declarations

No documentation.

Proof ▼
Theorem 2.203 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.204 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.205 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.206 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.207 ✓
#

Lean declarations

No documentation.

Proof ▼
Theorem 2.208 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.209 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.210 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.211 ✓
#

Lean declarations

No documentation.

Proof ▼
Theorem 2.212 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.213 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.214 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.215 ✓
#

Lean declarations

No documentation.

Proof ▼
Theorem 2.216 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.217 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.218 ✓
#

Lean declarations

No documentation.

Proof ▼
Theorem 2.219 ✓
#

Lean declarations

No documentation.

Proof ▼
Theorem 2.220 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.221 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.222 ✓
#

Lean declarations

No documentation.

Proof ▼
Theorem 2.223 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.224 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.225 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.226 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.227 ✓
#

Lean declarations

No documentation.

Proof ▼
Theorem 2.228 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.229 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.230 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Lemma 2.231 ✓
#

Lean declarations

No documentation.

Proof ▼
Theorem 2.232 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.233 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.234 ✓
#

Lean declarations

No documentation.

Proof ▼
Theorem 2.235 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.236 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.237 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Lemma 2.238 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.239 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.240 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.241 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Lemma 2.242 ✓
#

Lean declarations

No documentation.

Proof ▼
Theorem 2.243 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.244 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.245 ✓
#

Lean declarations

No documentation.

Proof ▼
Theorem 2.246 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.247 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.248 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.249 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.250 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼
Theorem 2.251 ✓
#

Uses

Lean declarations

No documentation.

Proof ▼