Documentation

LeanMlir.Proofs.Certificates.LipschitzCertScorecardSDPUncon

Per-pair LipSDP scorecard — unconstrained /128 net (`mlpT`) #

REDUCED CERTIFICATE MODEL — this file's concrete net is the 4×4-pooled 49-dim MNIST family (width-8 hidden, /128–/256 rational weights), NOT the canonical 784→512→512→10 mlpVerified; chosen so every margin/norm/SOS check is exact rational arithmetic in-kernel. Canonical surface: Proofs/MlpCanonical.lean.

The tighter-Lipschitz-constant pass over the SAME first-100 MNIST test subset and SAME ε = 1/10 as LipschitzCertScorecard.lean: replacing the global √2·∏‖Wᵢ‖ criterion by per-pair LipSDP certificates lifts the count from 1/100 to 63/100 — no retraining, no new data, just a less lossy constant on each pairwise logit gap. Each class pair carries a PSD witness checked by linarith from the 8 LDLᵀ column squares (hS* — the exact sum-of-squares certificate, d ≥ 0 weights found by linarith itself), turned into the squared gap bound by pair_sq_bound; each image evaluates its logits once (logit*_eval) and then needs only 9 rational margin checks against Lp·ε (certifiedSU<i>). PGD bracket: 69/100 — the cert ≤ TRUE ≤ PGD sandwich is nearly closed.

Theorem vs. measurement — read this before quoting a number. Soundness lives in the ENGINE (LipschitzCertPairSDP.lean), proved once — kernel- checking the 57th image buys nothing the 56th didn't. The count above is an exact-rational MEASUREMENT over the first 100 images; the first 8 certifying images (test-set order — an unbiased, reproducible rule) each carry a CertifiedAt THEOREM, and scorecard_sdp_uncon below states only those. Capping the images also caps the class pairs that need an LDLᵀ witness, which is what this tier costs on every proof push.

Generated by scripts/lipschitz_cert_pair_sdp.py; weights/images/ certificates are DATA (SDP solved off-line, verified exactly here).

noncomputable def Proofs.LipschitzCertDemo.vP01U :

Fin 8 → ℝ

Pair (0,1): ρ = 1389.652, Lp = 37.2781 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP01U = ![151 / 128, -621 / 128, 491 / 128, -71 / 32, 285 / 64, -135 / 64, 95 / 128, 73 / 128]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP01U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP01U = ![9533 / 512, 72075 / 1024, 38, 4365 / 64, 11941 / 128, 65257 / 1024, 13283 / 512, 7325 / 256]

Instances For

theorem Proofs.LipschitzCertDemo.vP01U_eq (t : Fin 8) :

vP01U t = W2t 0 t - W2t 1 t

theorem Proofs.LipschitzCertDemo.tP01U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS01U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP01U k * z k) ^ 2 + 1 / (1389652491 / 1000000) * ∑ a : Fin 8, ∑ b : Fin 8, tP01U a * z a * (G1t a b * (tP01U b * z b)) ≤ 2 * ∑ k : Fin 8, tP01U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_0_1 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 0 - (mlpT u).ofLp 1 - ((mlpT u').ofLp 0 - (mlpT u').ofLp 1)) ^ 2 ≤ 1389652491 / 1000000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP02U :

Fin 8 → ℝ

Pair (0,2): ρ = 726.897, Lp = 26.9611 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP02U = ![51 / 32, -111 / 32, 209 / 128, 93 / 128, 7 / 64, 289 / 128, -87 / 64, -205 / 128]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP02U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP02U = ![5887 / 512, 8575 / 256, 18583 / 1024, 507 / 32, 1943 / 512, 42687 / 1024, 5611 / 256, 19791 / 512]

Instances For

theorem Proofs.LipschitzCertDemo.vP02U_eq (t : Fin 8) :

vP02U t = W2t 0 t - W2t 2 t

theorem Proofs.LipschitzCertDemo.tP02U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS02U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP02U k * z k) ^ 2 + 1 / (363448733 / 500000) * ∑ a : Fin 8, ∑ b : Fin 8, tP02U a * z a * (G1t a b * (tP02U b * z b)) ≤ 2 * ∑ k : Fin 8, tP02U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_0_2 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 0 - (mlpT u).ofLp 2 - ((mlpT u').ofLp 0 - (mlpT u').ofLp 2)) ^ 2 ≤ 363448733 / 500000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP03U :

Fin 8 → ℝ

Pair (0,3): ρ = 494.336, Lp = 22.2337 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP03U = ![-1 / 32, -435 / 128, -13 / 128, 13 / 32, 161 / 64, 3 / 64, -173 / 64, 49 / 128]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP03U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP03U = ![1949 / 1024, 6287 / 256, 2427 / 512, 18451 / 1024, 21779 / 1024, 741 / 512, 9035 / 256, 3051 / 256]

Instances For

theorem Proofs.LipschitzCertDemo.vP03U_eq (t : Fin 8) :

vP03U t = W2t 0 t - W2t 3 t

theorem Proofs.LipschitzCertDemo.tP03U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS03U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP03U k * z k) ^ 2 + 1 / (123584079 / 250000) * ∑ a : Fin 8, ∑ b : Fin 8, tP03U a * z a * (G1t a b * (tP03U b * z b)) ≤ 2 * ∑ k : Fin 8, tP03U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_0_3 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 0 - (mlpT u).ofLp 3 - ((mlpT u').ofLp 0 - (mlpT u').ofLp 3)) ^ 2 ≤ 123584079 / 250000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP04U :

Fin 8 → ℝ

Pair (0,4): ρ = 1785.039, Lp = 42.2498 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP04U = ![-401 / 128, -213 / 128, 383 / 64, -31 / 64, 161 / 128, -57 / 128, -105 / 64, 243 / 128]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP04U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP04U = ![85999 / 1024, 87045 / 1024, 49189 / 1024, 75161 / 1024, 51403 / 1024, 4743 / 256, 35335 / 1024, 71579 / 1024]

Instances For

theorem Proofs.LipschitzCertDemo.vP04U_eq (t : Fin 8) :

vP04U t = W2t 0 t - W2t 4 t

theorem Proofs.LipschitzCertDemo.tP04U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS04U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP04U k * z k) ^ 2 + 1 / (892519569 / 500000) * ∑ a : Fin 8, ∑ b : Fin 8, tP04U a * z a * (G1t a b * (tP04U b * z b)) ≤ 2 * ∑ k : Fin 8, tP04U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_0_4 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 0 - (mlpT u).ofLp 4 - ((mlpT u').ofLp 0 - (mlpT u').ofLp 4)) ^ 2 ≤ 892519569 / 500000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP05U :

Fin 8 → ℝ

Pair (0,5): ρ = 446.615, Lp = 21.1333 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP05U = ![-15 / 16, -63 / 128, 9 / 16, -311 / 128, 401 / 128, -47 / 16, -45 / 128, 59 / 128]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP05U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP05U = ![5417 / 512, 6053 / 256, 95 / 16, 14307 / 512, 24359 / 1024, 23545 / 1024, 12461 / 1024, 25583 / 1024]

Instances For

theorem Proofs.LipschitzCertDemo.vP05U_eq (t : Fin 8) :

vP05U t = W2t 0 t - W2t 5 t

theorem Proofs.LipschitzCertDemo.tP05U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS05U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP05U k * z k) ^ 2 + 1 / (89323009 / 200000) * ∑ a : Fin 8, ∑ b : Fin 8, tP05U a * z a * (G1t a b * (tP05U b * z b)) ≤ 2 * ∑ k : Fin 8, tP05U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_0_5 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 0 - (mlpT u).ofLp 5 - ((mlpT u').ofLp 0 - (mlpT u').ofLp 5)) ^ 2 ≤ 89323009 / 200000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP06U :

Fin 8 → ℝ

Pair (0,6): ρ = 1360.015, Lp = 36.8784 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP06U = ![143 / 128, -167 / 128, 237 / 64, -231 / 64, -47 / 64, -5 / 4, -171 / 128, 131 / 64]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP06U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP06U = ![8417 / 512, 29057 / 256, 28035 / 1024, 12341 / 256, 13395 / 1024, 7743 / 128, 5319 / 256, 86769 / 1024]

Instances For

theorem Proofs.LipschitzCertDemo.vP06U_eq (t : Fin 8) :

vP06U t = W2t 0 t - W2t 6 t

theorem Proofs.LipschitzCertDemo.tP06U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS06U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP06U k * z k) ^ 2 + 1 / (680007581 / 500000) * ∑ a : Fin 8, ∑ b : Fin 8, tP06U a * z a * (G1t a b * (tP06U b * z b)) ≤ 2 * ∑ k : Fin 8, tP06U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_0_6 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 0 - (mlpT u).ofLp 6 - ((mlpT u').ofLp 0 - (mlpT u').ofLp 6)) ^ 2 ≤ 680007581 / 500000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP07U :

Fin 8 → ℝ

Pair (0,7): ρ = 1215.933, Lp = 34.8703 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP07U = ![-157 / 64, -519 / 128, 175 / 128, 87 / 64, 15 / 32, -183 / 128, 149 / 128, 497 / 128]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP07U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP07U = ![7437 / 256, 14867 / 256, 30711 / 1024, 25521 / 1024, 14247 / 1024, 2369 / 32, 25853 / 1024, 10541 / 256]

Instances For

theorem Proofs.LipschitzCertDemo.vP07U_eq (t : Fin 8) :

vP07U t = W2t 0 t - W2t 7 t

theorem Proofs.LipschitzCertDemo.tP07U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS07U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP07U k * z k) ^ 2 + 1 / (1215933471 / 1000000) * ∑ a : Fin 8, ∑ b : Fin 8, tP07U a * z a * (G1t a b * (tP07U b * z b)) ≤ 2 * ∑ k : Fin 8, tP07U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_0_7 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 0 - (mlpT u).ofLp 7 - ((mlpT u').ofLp 0 - (mlpT u').ofLp 7)) ^ 2 ≤ 1215933471 / 1000000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP08U :

Fin 8 → ℝ

Pair (0,8): ρ = 550.526, Lp = 23.4633 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP08U = ![-233 / 128, -315 / 128, 89 / 32, -9 / 8, 77 / 32, 67 / 64, 45 / 32, -87 / 64]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP08U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP08U = ![16097 / 1024, 6999 / 256, 5191 / 256, 25431 / 1024, 21031 / 1024, 15857 / 1024, 18953 / 1024, 28339 / 1024]

Instances For

theorem Proofs.LipschitzCertDemo.vP08U_eq (t : Fin 8) :

vP08U t = W2t 0 t - W2t 8 t

theorem Proofs.LipschitzCertDemo.tP08U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS08U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP08U k * z k) ^ 2 + 1 / (275263221 / 500000) * ∑ a : Fin 8, ∑ b : Fin 8, tP08U a * z a * (G1t a b * (tP08U b * z b)) ≤ 2 * ∑ k : Fin 8, tP08U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_0_8 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 0 - (mlpT u).ofLp 8 - ((mlpT u').ofLp 0 - (mlpT u').ofLp 8)) ^ 2 ≤ 275263221 / 500000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP09U :

Fin 8 → ℝ

Pair (0,9): ρ = 1367.420, Lp = 36.9787 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP09U = ![-279 / 64, -189 / 64, 479 / 128, 135 / 128, 127 / 64, 7 / 4, 135 / 128, 181 / 128]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP09U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP09U = ![4573 / 128, 74995 / 1024, 57839 / 1024, 15387 / 512, 16533 / 512, 3071 / 64, 6431 / 256, 24995 / 1024]

Instances For

theorem Proofs.LipschitzCertDemo.vP09U_eq (t : Fin 8) :

vP09U t = W2t 0 t - W2t 9 t

theorem Proofs.LipschitzCertDemo.tP09U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS09U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP09U k * z k) ^ 2 + 1 / (68370991 / 50000) * ∑ a : Fin 8, ∑ b : Fin 8, tP09U a * z a * (G1t a b * (tP09U b * z b)) ≤ 2 * ∑ k : Fin 8, tP09U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_0_9 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 0 - (mlpT u).ofLp 9 - ((mlpT u').ofLp 0 - (mlpT u').ofLp 9)) ^ 2 ≤ 68370991 / 50000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP12U :

Fin 8 → ℝ

Pair (1,2): ρ = 1012.861, Lp = 31.8255 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP12U = ![53 / 128, 177 / 128, -141 / 64, 377 / 128, -139 / 32, 559 / 128, -269 / 128, -139 / 64]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP12U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP12U = ![7815 / 1024, 24655 / 512, 2071 / 64, 3519 / 64, 49857 / 1024, 51433 / 1024, 10773 / 256, 24121 / 512]

Instances For

theorem Proofs.LipschitzCertDemo.vP12U_eq (t : Fin 8) :

vP12U t = W2t 1 t - W2t 2 t

theorem Proofs.LipschitzCertDemo.tP12U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS12U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP12U k * z k) ^ 2 + 1 / (1012860851 / 1000000) * ∑ a : Fin 8, ∑ b : Fin 8, tP12U a * z a * (G1t a b * (tP12U b * z b)) ≤ 2 * ∑ k : Fin 8, tP12U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_1_2 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 1 - (mlpT u).ofLp 2 - ((mlpT u').ofLp 1 - (mlpT u').ofLp 2)) ^ 2 ≤ 1012860851 / 1000000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP13U :

Fin 8 → ℝ

Pair (1,3): ρ = 1085.594, Lp = 32.9484 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP13U = ![-155 / 128, 93 / 64, -63 / 16, 21 / 8, -31 / 16, 69 / 32, -441 / 128, -3 / 16]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP13U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP13U = ![1913 / 128, 43643 / 512, 12763 / 512, 5917 / 128, 8893 / 256, 44873 / 1024, 8595 / 128, 6413 / 1024]

Instances For

theorem Proofs.LipschitzCertDemo.vP13U_eq (t : Fin 8) :

vP13U t = W2t 1 t - W2t 3 t

theorem Proofs.LipschitzCertDemo.tP13U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS13U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP13U k * z k) ^ 2 + 1 / (1085593567 / 1000000) * ∑ a : Fin 8, ∑ b : Fin 8, tP13U a * z a * (G1t a b * (tP13U b * z b)) ≤ 2 * ∑ k : Fin 8, tP13U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_1_3 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 1 - (mlpT u).ofLp 3 - ((mlpT u').ofLp 1 - (mlpT u').ofLp 3)) ^ 2 ≤ 1085593567 / 1000000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP14U :

Fin 8 → ℝ

Pair (1,4): ρ = 1653.706, Lp = 40.6658 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP14U = ![-69 / 16, 51 / 16, 275 / 128, 111 / 64, -409 / 128, 213 / 128, -305 / 128, 85 / 64]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP14U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP14U = ![53417 / 1024, 54847 / 1024, 16009 / 512, 30083 / 512, 4751 / 64, 63635 / 1024, 68179 / 1024, 28079 / 512]

Instances For

theorem Proofs.LipschitzCertDemo.vP14U_eq (t : Fin 8) :

vP14U t = W2t 1 t - W2t 4 t

theorem Proofs.LipschitzCertDemo.tP14U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS14U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP14U k * z k) ^ 2 + 1 / (206713291 / 125000) * ∑ a : Fin 8, ∑ b : Fin 8, tP14U a * z a * (G1t a b * (tP14U b * z b)) ≤ 2 * ∑ k : Fin 8, tP14U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_1_4 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 1 - (mlpT u).ofLp 4 - ((mlpT u').ofLp 1 - (mlpT u').ofLp 4)) ^ 2 ≤ 206713291 / 125000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP15U :

Fin 8 → ℝ

Pair (1,5): ρ = 1071.084, Lp = 32.7275 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP15U = ![-271 / 128, 279 / 64, -419 / 128, -27 / 128, -169 / 128, -53 / 64, -35 / 32, -7 / 64]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP15U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP15U = ![19393 / 1024, 25819 / 512, 14193 / 512, 21121 / 1024, 35043 / 1024, 78769 / 1024, 17271 / 512, 12863 / 1024]

Instances For

theorem Proofs.LipschitzCertDemo.vP15U_eq (t : Fin 8) :

vP15U t = W2t 1 t - W2t 5 t

theorem Proofs.LipschitzCertDemo.tP15U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS15U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP15U k * z k) ^ 2 + 1 / (107108431 / 100000) * ∑ a : Fin 8, ∑ b : Fin 8, tP15U a * z a * (G1t a b * (tP15U b * z b)) ≤ 2 * ∑ k : Fin 8, tP15U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_1_5 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 1 - (mlpT u).ofLp 5 - ((mlpT u').ofLp 1 - (mlpT u').ofLp 5)) ^ 2 ≤ 107108431 / 100000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP16U :

Fin 8 → ℝ

Pair (1,6): ρ = 1184.729, Lp = 34.4199 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP16U = ![-1 / 16, 227 / 64, -17 / 128, -89 / 64, -83 / 16, 55 / 64, -133 / 64, 189 / 128]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP16U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP16U = ![2803 / 1024, 1575 / 32, 907 / 512, 28235 / 1024, 49055 / 1024, 65017 / 1024, 19649 / 512, 37083 / 512]

Instances For

theorem Proofs.LipschitzCertDemo.vP16U_eq (t : Fin 8) :

vP16U t = W2t 1 t - W2t 6 t

theorem Proofs.LipschitzCertDemo.tP16U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS16U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP16U k * z k) ^ 2 + 1 / (592364409 / 500000) * ∑ a : Fin 8, ∑ b : Fin 8, tP16U a * z a * (G1t a b * (tP16U b * z b)) ≤ 2 * ∑ k : Fin 8, tP16U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_1_6 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 1 - (mlpT u).ofLp 6 - ((mlpT u').ofLp 1 - (mlpT u').ofLp 6)) ^ 2 ≤ 592364409 / 500000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP17U :

Fin 8 → ℝ

Pair (1,7): ρ = 1869.057, Lp = 43.2326 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP17U = ![-465 / 128, 51 / 64, -79 / 32, 229 / 64, -255 / 64, 87 / 128, 27 / 64, 53 / 16]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP17U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP17U = ![37845 / 1024, 22361 / 256, 8681 / 256, 895 / 16, 117999 / 1024, 28747 / 512, 11959 / 1024, 55197 / 1024]

Instances For

theorem Proofs.LipschitzCertDemo.vP17U_eq (t : Fin 8) :

vP17U t = W2t 1 t - W2t 7 t

theorem Proofs.LipschitzCertDemo.tP17U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS17U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP17U k * z k) ^ 2 + 1 / (373811483 / 200000) * ∑ a : Fin 8, ∑ b : Fin 8, tP17U a * z a * (G1t a b * (tP17U b * z b)) ≤ 2 * ∑ k : Fin 8, tP17U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_1_7 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 1 - (mlpT u).ofLp 7 - ((mlpT u').ofLp 1 - (mlpT u').ofLp 7)) ^ 2 ≤ 373811483 / 200000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP18U :

Fin 8 → ℝ

Pair (1,8): ρ = 850.370, Lp = 29.1612 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP18U = ![-3, 153 / 64, -135 / 128, 35 / 32, -131 / 64, 101 / 32, 85 / 128, -247 / 128]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP18U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP18U = ![20573 / 1024, 39613 / 1024, 5325 / 512, 24695 / 512, 5435 / 128, 41827 / 1024, 985 / 64, 40557 / 1024]

Instances For

theorem Proofs.LipschitzCertDemo.vP18U_eq (t : Fin 8) :

vP18U t = W2t 1 t - W2t 8 t

theorem Proofs.LipschitzCertDemo.tP18U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS18U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP18U k * z k) ^ 2 + 1 / (425185151 / 500000) * ∑ a : Fin 8, ∑ b : Fin 8, tP18U a * z a * (G1t a b * (tP18U b * z b)) ≤ 2 * ∑ k : Fin 8, tP18U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_1_8 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 1 - (mlpT u).ofLp 8 - ((mlpT u').ofLp 1 - (mlpT u').ofLp 8)) ^ 2 ≤ 425185151 / 500000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP19U :

Fin 8 → ℝ

Pair (1,9): ρ = 1914.202, Lp = 43.7516 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP19U = ![-709 / 128, 243 / 128, -3 / 32, 419 / 128, -79 / 32, 247 / 64, 5 / 16, 27 / 32]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP19U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP19U = ![24831 / 512, 35303 / 512, 2439 / 1024, 76471 / 1024, 22317 / 256, 61313 / 512, 479 / 32, 19689 / 1024]

Instances For

theorem Proofs.LipschitzCertDemo.vP19U_eq (t : Fin 8) :

vP19U t = W2t 1 t - W2t 9 t

theorem Proofs.LipschitzCertDemo.tP19U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS19U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP19U k * z k) ^ 2 + 1 / (95710089 / 50000) * ∑ a : Fin 8, ∑ b : Fin 8, tP19U a * z a * (G1t a b * (tP19U b * z b)) ≤ 2 * ∑ k : Fin 8, tP19U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_1_9 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 1 - (mlpT u).ofLp 9 - ((mlpT u').ofLp 1 - (mlpT u').ofLp 9)) ^ 2 ≤ 95710089 / 50000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP24U :

Fin 8 → ℝ

Pair (2,4): ρ = 2054.235, Lp = 45.3237 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP24U = ![-605 / 128, 231 / 128, 557 / 128, -155 / 128, 147 / 128, -173 / 64, -9 / 32, 7 / 2]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP24U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP24U = ![30949 / 512, 25517 / 512, 30293 / 512, 55733 / 1024, 107301 / 1024, 71693 / 1024, 16937 / 1024, 23081 / 256]

Instances For

theorem Proofs.LipschitzCertDemo.vP24U_eq (t : Fin 8) :

vP24U t = W2t 2 t - W2t 4 t

theorem Proofs.LipschitzCertDemo.tP24U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS24U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP24U k * z k) ^ 2 + 1 / (1027117507 / 500000) * ∑ a : Fin 8, ∑ b : Fin 8, tP24U a * z a * (G1t a b * (tP24U b * z b)) ≤ 2 * ∑ k : Fin 8, tP24U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_2_4 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 2 - (mlpT u).ofLp 4 - ((mlpT u').ofLp 2 - (mlpT u').ofLp 4)) ^ 2 ≤ 1027117507 / 500000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP26U :

Fin 8 → ℝ

Pair (2,6): ρ = 1126.622, Lp = 33.5652 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP26U = ![-61 / 128, 277 / 128, 265 / 128, -555 / 128, -27 / 32, -449 / 128, 3 / 128, 467 / 128]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP26U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP26U = ![8251 / 256, 41799 / 1024, 5273 / 256, 53151 / 1024, 17425 / 1024, 65959 / 1024, 271 / 1024, 18117 / 256]

Instances For

theorem Proofs.LipschitzCertDemo.vP26U_eq (t : Fin 8) :

vP26U t = W2t 2 t - W2t 6 t

theorem Proofs.LipschitzCertDemo.tP26U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS26U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP26U k * z k) ^ 2 + 1 / (225324373 / 200000) * ∑ a : Fin 8, ∑ b : Fin 8, tP26U a * z a * (G1t a b * (tP26U b * z b)) ≤ 2 * ∑ k : Fin 8, tP26U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_2_6 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 2 - (mlpT u).ofLp 6 - ((mlpT u').ofLp 2 - (mlpT u').ofLp 6)) ^ 2 ≤ 225324373 / 200000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP27U :

Fin 8 → ℝ

Pair (2,7): ρ = 1988.401, Lp = 44.5915 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP27U = ![-259 / 64, -75 / 128, -17 / 64, 81 / 128, 23 / 64, -59 / 16, 323 / 128, 351 / 64]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP27U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP27U = ![21273 / 512, 29063 / 256, 607 / 64, 7207 / 512, 19355 / 1024, 33937 / 256, 62, 43037 / 512]

Instances For

theorem Proofs.LipschitzCertDemo.vP27U_eq (t : Fin 8) :

vP27U t = W2t 2 t - W2t 7 t

theorem Proofs.LipschitzCertDemo.tP27U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS27U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP27U k * z k) ^ 2 + 1 / (1988400511 / 1000000) * ∑ a : Fin 8, ∑ b : Fin 8, tP27U a * z a * (G1t a b * (tP27U b * z b)) ≤ 2 * ∑ k : Fin 8, tP27U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_2_7 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 2 - (mlpT u).ofLp 7 - ((mlpT u').ofLp 2 - (mlpT u').ofLp 7)) ^ 2 ≤ 1988400511 / 1000000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP34U :

Fin 8 → ℝ

Pair (3,4): ρ = 1892.635, Lp = 43.5045 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP34U = ![-397 / 128, 111 / 64, 779 / 128, -57 / 64, -161 / 128, -63 / 128, 17 / 16, 97 / 64]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP34U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP34U = ![21875 / 256, 1511 / 32, 51811 / 1024, 110521 / 1024, 32165 / 1024, 19147 / 1024, 8219 / 256, 83413 / 1024]

Instances For

theorem Proofs.LipschitzCertDemo.vP34U_eq (t : Fin 8) :

vP34U t = W2t 3 t - W2t 4 t

theorem Proofs.LipschitzCertDemo.tP34U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS34U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP34U k * z k) ^ 2 + 1 / (473158719 / 250000) * ∑ a : Fin 8, ∑ b : Fin 8, tP34U a * z a * (G1t a b * (tP34U b * z b)) ≤ 2 * ∑ k : Fin 8, tP34U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_3_4 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 3 - (mlpT u).ofLp 4 - ((mlpT u').ofLp 3 - (mlpT u').ofLp 4)) ^ 2 ≤ 473158719 / 250000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP36U :

Fin 8 → ℝ

Pair (3,6): ρ = 1972.116, Lp = 44.4086 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP36U = ![147 / 128, 67 / 32, 487 / 128, -257 / 64, -13 / 4, -83 / 64, 175 / 128, 213 / 128]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP36U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP36U = ![24497 / 1024, 71637 / 1024, 37335 / 1024, 35023 / 512, 24201 / 512, 66295 / 1024, 37807 / 1024, 82085 / 1024]

Instances For

theorem Proofs.LipschitzCertDemo.vP36U_eq (t : Fin 8) :

vP36U t = W2t 3 t - W2t 6 t

theorem Proofs.LipschitzCertDemo.tP36U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS36U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP36U k * z k) ^ 2 + 1 / (1972115633 / 1000000) * ∑ a : Fin 8, ∑ b : Fin 8, tP36U a * z a * (G1t a b * (tP36U b * z b)) ≤ 2 * ∑ k : Fin 8, tP36U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_3_6 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 3 - (mlpT u).ofLp 6 - ((mlpT u').ofLp 3 - (mlpT u').ofLp 6)) ^ 2 ≤ 1972115633 / 1000000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP37U :

Fin 8 → ℝ

Pair (3,7): ρ = 1120.711, Lp = 33.4771 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP37U = ![-155 / 64, -21 / 32, 47 / 32, 61 / 64, -131 / 64, -189 / 128, 495 / 128, 7 / 2]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP37U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP37U = ![23685 / 1024, 47451 / 1024, 28759 / 1024, 8397 / 512, 34773 / 512, 59803 / 1024, 23279 / 512, 10627 / 256]

Instances For

theorem Proofs.LipschitzCertDemo.vP37U_eq (t : Fin 8) :

vP37U t = W2t 3 t - W2t 7 t

theorem Proofs.LipschitzCertDemo.tP37U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS37U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP37U k * z k) ^ 2 + 1 / (1120711457 / 1000000) * ∑ a : Fin 8, ∑ b : Fin 8, tP37U a * z a * (G1t a b * (tP37U b * z b)) ≤ 2 * ∑ k : Fin 8, tP37U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_3_7 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 3 - (mlpT u).ofLp 7 - ((mlpT u').ofLp 3 - (mlpT u').ofLp 7)) ^ 2 ≤ 1120711457 / 1000000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP45U :

Fin 8 → ℝ

Pair (4,5): ρ = 1681.545, Lp = 41.0067 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP45U = ![281 / 128, 75 / 64, -347 / 64, -249 / 128, 15 / 8, -319 / 128, 165 / 128, -23 / 16]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP45U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP45U = ![5129 / 64, 48039 / 512, 19965 / 512, 37979 / 512, 35701 / 1024, 43771 / 512, 13785 / 512, 40339 / 512]

Instances For

theorem Proofs.LipschitzCertDemo.vP45U_eq (t : Fin 8) :

vP45U t = W2t 4 t - W2t 5 t

theorem Proofs.LipschitzCertDemo.tP45U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS45U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP45U k * z k) ^ 2 + 1 / (16815449 / 10000) * ∑ a : Fin 8, ∑ b : Fin 8, tP45U a * z a * (G1t a b * (tP45U b * z b)) ≤ 2 * ∑ k : Fin 8, tP45U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_4_5 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 4 - (mlpT u).ofLp 5 - ((mlpT u').ofLp 4 - (mlpT u').ofLp 5)) ^ 2 ≤ 16815449 / 10000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP46U :

Fin 8 → ℝ

Pair (4,6): ρ = 1231.061, Lp = 35.0865 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP46U = ![17 / 4, 23 / 64, -73 / 32, -25 / 8, -255 / 128, -103 / 128, 39 / 128, 19 / 128]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP46U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP46U = ![30505 / 1024, 16567 / 512, 50127 / 1024, 36759 / 1024, 33415 / 1024, 20769 / 512, 5969 / 512, 2763 / 512]

Instances For

theorem Proofs.LipschitzCertDemo.vP46U_eq (t : Fin 8) :

vP46U t = W2t 4 t - W2t 6 t

theorem Proofs.LipschitzCertDemo.tP46U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS46U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP46U k * z k) ^ 2 + 1 / (1231060917 / 1000000) * ∑ a : Fin 8, ∑ b : Fin 8, tP46U a * z a * (G1t a b * (tP46U b * z b)) ≤ 2 * ∑ k : Fin 8, tP46U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_4_6 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 4 - (mlpT u).ofLp 6 - ((mlpT u').ofLp 4 - (mlpT u').ofLp 6)) ^ 2 ≤ 1231060917 / 1000000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP47U :

Fin 8 → ℝ

Pair (4,7): ρ = 1795.391, Lp = 42.3721 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP47U = ![87 / 128, -153 / 64, -591 / 128, 59 / 32, -101 / 128, -63 / 64, 359 / 128, 127 / 64]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP47U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP47U = ![22023 / 1024, 3595 / 64, 38897 / 1024, 23921 / 512, 23181 / 1024, 49449 / 1024, 20755 / 512, 28713 / 512]

Instances For

theorem Proofs.LipschitzCertDemo.vP47U_eq (t : Fin 8) :

vP47U t = W2t 4 t - W2t 7 t

theorem Proofs.LipschitzCertDemo.tP47U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS47U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP47U k * z k) ^ 2 + 1 / (897695409 / 500000) * ∑ a : Fin 8, ∑ b : Fin 8, tP47U a * z a * (G1t a b * (tP47U b * z b)) ≤ 2 * ∑ k : Fin 8, tP47U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_4_7 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 4 - (mlpT u).ofLp 7 - ((mlpT u').ofLp 4 - (mlpT u').ofLp 7)) ^ 2 ≤ 897695409 / 500000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP48U :

Fin 8 → ℝ

Pair (4,8): ρ = 1227.146, Lp = 35.0307 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP48U = ![21 / 16, -51 / 64, -205 / 64, -41 / 64, 147 / 128, 191 / 128, 195 / 64, -417 / 128]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP48U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP48U = ![61197 / 1024, 12481 / 512, 11917 / 512, 7595 / 256, 26423 / 1024, 40479 / 1024, 10581 / 256, 65037 / 1024]

Instances For

theorem Proofs.LipschitzCertDemo.vP48U_eq (t : Fin 8) :

vP48U t = W2t 4 t - W2t 8 t

theorem Proofs.LipschitzCertDemo.tP48U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS48U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP48U k * z k) ^ 2 + 1 / (1227146101 / 1000000) * ∑ a : Fin 8, ∑ b : Fin 8, tP48U a * z a * (G1t a b * (tP48U b * z b)) ≤ 2 * ∑ k : Fin 8, tP48U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_4_8 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 4 - (mlpT u).ofLp 8 - ((mlpT u').ofLp 4 - (mlpT u').ofLp 8)) ^ 2 ≤ 1227146101 / 1000000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP49U :

Fin 8 → ℝ

Pair (4,9): ρ = 990.367, Lp = 31.4701 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP49U = ![-157 / 128, -165 / 128, -287 / 128, 197 / 128, 93 / 128, 281 / 128, 345 / 128, -31 / 64]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP49U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP49U = ![8309 / 512, 30863 / 1024, 14841 / 1024, 36049 / 1024, 11681 / 1024, 18645 / 512, 28681 / 1024, 855 / 64]

Instances For

theorem Proofs.LipschitzCertDemo.vP49U_eq (t : Fin 8) :

vP49U t = W2t 4 t - W2t 9 t

theorem Proofs.LipschitzCertDemo.tP49U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS49U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP49U k * z k) ^ 2 + 1 / (495183309 / 500000) * ∑ a : Fin 8, ∑ b : Fin 8, tP49U a * z a * (G1t a b * (tP49U b * z b)) ≤ 2 * ∑ k : Fin 8, tP49U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_4_9 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 4 - (mlpT u).ofLp 9 - ((mlpT u').ofLp 4 - (mlpT u').ofLp 9)) ^ 2 ≤ 495183309 / 500000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP56U :

Fin 8 → ℝ

Pair (5,6): ρ = 1528.119, Lp = 39.0912 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP56U = ![263 / 128, -13 / 16, 201 / 64, -151 / 128, -495 / 128, 27 / 16, -63 / 64, 203 / 128]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP56U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP56U = ![12579 / 512, 90891 / 1024, 28289 / 1024, 28787 / 1024, 47831 / 1024, 87029 / 1024, 2751 / 128, 99187 / 1024]

Instances For

theorem Proofs.LipschitzCertDemo.vP56U_eq (t : Fin 8) :

vP56U t = W2t 5 t - W2t 6 t

theorem Proofs.LipschitzCertDemo.tP56U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS56U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP56U k * z k) ^ 2 + 1 / (1528119211 / 1000000) * ∑ a : Fin 8, ∑ b : Fin 8, tP56U a * z a * (G1t a b * (tP56U b * z b)) ≤ 2 * ∑ k : Fin 8, tP56U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_5_6 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 5 - (mlpT u).ofLp 6 - ((mlpT u').ofLp 5 - (mlpT u').ofLp 6)) ^ 2 ≤ 1528119211 / 1000000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP57U :

Fin 8 → ℝ

Pair (5,7): ρ = 1394.487, Lp = 37.3429 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP57U = ![-97 / 64, -57 / 16, 103 / 128, 485 / 128, -341 / 128, 193 / 128, 97 / 64, 219 / 64]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP57U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP57U = ![3571 / 128, 61855 / 1024, 19959 / 1024, 47449 / 1024, 51873 / 512, 14711 / 256, 16643 / 512, 10427 / 256]

Instances For

theorem Proofs.LipschitzCertDemo.vP57U_eq (t : Fin 8) :

vP57U t = W2t 5 t - W2t 7 t

theorem Proofs.LipschitzCertDemo.tP57U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS57U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP57U k * z k) ^ 2 + 1 / (697243359 / 500000) * ∑ a : Fin 8, ∑ b : Fin 8, tP57U a * z a * (G1t a b * (tP57U b * z b)) ≤ 2 * ∑ k : Fin 8, tP57U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_5_7 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 5 - (mlpT u).ofLp 7 - ((mlpT u').ofLp 5 - (mlpT u').ofLp 7)) ^ 2 ≤ 697243359 / 500000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP67U :

Fin 8 → ℝ

Pair (6,7): ρ = 2650.733, Lp = 51.4853 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP67U = ![-457 / 128, -11 / 4, -299 / 128, 159 / 32, 77 / 64, -23 / 128, 5 / 2, 235 / 128]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP67U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP67U = ![26521 / 512, 57989 / 512, 2305 / 64, 78839 / 1024, 17845 / 512, 48819 / 1024, 56151 / 1024, 1835 / 32]

Instances For

theorem Proofs.LipschitzCertDemo.vP67U_eq (t : Fin 8) :

vP67U t = W2t 6 t - W2t 7 t

theorem Proofs.LipschitzCertDemo.tP67U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS67U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP67U k * z k) ^ 2 + 1 / (1325366677 / 500000) * ∑ a : Fin 8, ∑ b : Fin 8, tP67U a * z a * (G1t a b * (tP67U b * z b)) ≤ 2 * ∑ k : Fin 8, tP67U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_6_7 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 6 - (mlpT u).ofLp 7 - ((mlpT u').ofLp 6 - (mlpT u').ofLp 7)) ^ 2 ≤ 1325366677 / 500000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP68U :

Fin 8 → ℝ

Pair (6,8): ρ = 1532.226, Lp = 39.1437 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP68U = ![-47 / 16, -37 / 32, -59 / 64, 159 / 64, 201 / 64, 147 / 64, 351 / 128, -109 / 32]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP68U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP68U = ![32427 / 1024, 59549 / 1024, 79 / 8, 24313 / 512, 2635 / 64, 34585 / 512, 22539 / 512, 25317 / 256]

Instances For

theorem Proofs.LipschitzCertDemo.vP68U_eq (t : Fin 8) :

vP68U t = W2t 6 t - W2t 8 t

theorem Proofs.LipschitzCertDemo.tP68U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS68U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP68U k * z k) ^ 2 + 1 / (1532226297 / 1000000) * ∑ a : Fin 8, ∑ b : Fin 8, tP68U a * z a * (G1t a b * (tP68U b * z b)) ≤ 2 * ∑ k : Fin 8, tP68U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_6_8 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 6 - (mlpT u).ofLp 8 - ((mlpT u').ofLp 6 - (mlpT u').ofLp 8)) ^ 2 ≤ 1532226297 / 1000000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP69U :

Fin 8 → ℝ

Pair (6,9): ρ = 2632.403, Lp = 51.3070 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP69U = ![-701 / 128, -211 / 128, 5 / 128, 597 / 128, 87 / 32, 3, 153 / 64, -81 / 128]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP69U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP69U = ![32337 / 512, 149173 / 1024, 819 / 1024, 11129 / 128, 30965 / 512, 201215 / 1024, 66317 / 1024, 23145 / 1024]

Instances For

theorem Proofs.LipschitzCertDemo.vP69U_eq (t : Fin 8) :

vP69U t = W2t 6 t - W2t 9 t

theorem Proofs.LipschitzCertDemo.tP69U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS69U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP69U k * z k) ^ 2 + 1 / (2632402727 / 1000000) * ∑ a : Fin 8, ∑ b : Fin 8, tP69U a * z a * (G1t a b * (tP69U b * z b)) ≤ 2 * ∑ k : Fin 8, tP69U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_6_9 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 6 - (mlpT u).ofLp 9 - ((mlpT u').ofLp 6 - (mlpT u').ofLp 9)) ^ 2 ≤ 2632402727 / 1000000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP78U :

Fin 8 → ℝ

Pair (7,8): ρ = 1162.533, Lp = 34.0960 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP78U = ![81 / 128, 51 / 32, 181 / 128, -159 / 64, 31 / 16, 317 / 128, 31 / 128, -671 / 128]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP78U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP78U = ![12013 / 1024, 47057 / 1024, 26531 / 1024, 15769 / 512, 62415 / 1024, 75729 / 1024, 5889 / 1024, 24075 / 512]

Instances For

theorem Proofs.LipschitzCertDemo.vP78U_eq (t : Fin 8) :

vP78U t = W2t 7 t - W2t 8 t

theorem Proofs.LipschitzCertDemo.tP78U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS78U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP78U k * z k) ^ 2 + 1 / (290633259 / 250000) * ∑ a : Fin 8, ∑ b : Fin 8, tP78U a * z a * (G1t a b * (tP78U b * z b)) ≤ 2 * ∑ k : Fin 8, tP78U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_7_8 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 7 - (mlpT u).ofLp 8 - ((mlpT u').ofLp 7 - (mlpT u').ofLp 8)) ^ 2 ≤ 290633259 / 250000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP79U :

Fin 8 → ℝ

Pair (7,9): ρ = 558.286, Lp = 23.6281 (√2·L-product criterion would need 90.22).

Equations

Proofs.LipschitzCertDemo.vP79U = ![-61 / 32, 141 / 128, 19 / 8, -39 / 128, 97 / 64, 407 / 128, -7 / 64, -79 / 32]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP79U :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP79U = ![8957 / 512, 7339 / 512, 4749 / 256, 1465 / 1024, 18913 / 1024, 27647 / 1024, 6061 / 1024, 34535 / 1024]

Instances For

theorem Proofs.LipschitzCertDemo.vP79U_eq (t : Fin 8) :

vP79U t = W2t 7 t - W2t 9 t

theorem Proofs.LipschitzCertDemo.tP79U_nonneg (k : Fin 8) :

theorem Proofs.LipschitzCertDemo.hS79U (z : Fin 8 → ℝ) :

(∑ k : Fin 8, vP79U k * z k) ^ 2 + 1 / (558285667 / 1000000) * ∑ a : Fin 8, ∑ b : Fin 8, tP79U a * z a * (G1t a b * (tP79U b * z b)) ≤ 2 * ∑ k : Fin 8, tP79U k * z k ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_7_9 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 7 - (mlpT u).ofLp 9 - ((mlpT u').ofLp 7 - (mlpT u').ofLp 9)) ^ 2 ≤ 558285667 / 1000000 * ‖u - u'‖ ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_1_0 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 1 - (mlpT u).ofLp 0 - ((mlpT u').ofLp 1 - (mlpT u').ofLp 0)) ^ 2 ≤ 1389652491 / 1000000 * ‖u - u'‖ ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_4_0 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 4 - (mlpT u).ofLp 0 - ((mlpT u').ofLp 4 - (mlpT u').ofLp 0)) ^ 2 ≤ 892519569 / 500000 * ‖u - u'‖ ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_4_1 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 4 - (mlpT u).ofLp 1 - ((mlpT u').ofLp 4 - (mlpT u').ofLp 1)) ^ 2 ≤ 206713291 / 125000 * ‖u - u'‖ ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_4_2 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 4 - (mlpT u).ofLp 2 - ((mlpT u').ofLp 4 - (mlpT u').ofLp 2)) ^ 2 ≤ 1027117507 / 500000 * ‖u - u'‖ ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_4_3 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 4 - (mlpT u).ofLp 3 - ((mlpT u').ofLp 4 - (mlpT u').ofLp 3)) ^ 2 ≤ 473158719 / 250000 * ‖u - u'‖ ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_6_0 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 6 - (mlpT u).ofLp 0 - ((mlpT u').ofLp 6 - (mlpT u').ofLp 0)) ^ 2 ≤ 680007581 / 500000 * ‖u - u'‖ ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_6_1 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 6 - (mlpT u).ofLp 1 - ((mlpT u').ofLp 6 - (mlpT u').ofLp 1)) ^ 2 ≤ 592364409 / 500000 * ‖u - u'‖ ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_6_2 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 6 - (mlpT u).ofLp 2 - ((mlpT u').ofLp 6 - (mlpT u').ofLp 2)) ^ 2 ≤ 225324373 / 200000 * ‖u - u'‖ ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_6_3 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 6 - (mlpT u).ofLp 3 - ((mlpT u').ofLp 6 - (mlpT u').ofLp 3)) ^ 2 ≤ 1972115633 / 1000000 * ‖u - u'‖ ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_6_4 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 6 - (mlpT u).ofLp 4 - ((mlpT u').ofLp 6 - (mlpT u').ofLp 4)) ^ 2 ≤ 1231060917 / 1000000 * ‖u - u'‖ ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_6_5 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 6 - (mlpT u).ofLp 5 - ((mlpT u').ofLp 6 - (mlpT u').ofLp 5)) ^ 2 ≤ 1528119211 / 1000000 * ‖u - u'‖ ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_7_0 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 7 - (mlpT u).ofLp 0 - ((mlpT u').ofLp 7 - (mlpT u').ofLp 0)) ^ 2 ≤ 1215933471 / 1000000 * ‖u - u'‖ ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_7_1 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 7 - (mlpT u).ofLp 1 - ((mlpT u').ofLp 7 - (mlpT u').ofLp 1)) ^ 2 ≤ 373811483 / 200000 * ‖u - u'‖ ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_7_2 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 7 - (mlpT u).ofLp 2 - ((mlpT u').ofLp 7 - (mlpT u').ofLp 2)) ^ 2 ≤ 1988400511 / 1000000 * ‖u - u'‖ ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_7_3 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 7 - (mlpT u).ofLp 3 - ((mlpT u').ofLp 7 - (mlpT u').ofLp 3)) ^ 2 ≤ 1120711457 / 1000000 * ‖u - u'‖ ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_7_4 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 7 - (mlpT u).ofLp 4 - ((mlpT u').ofLp 7 - (mlpT u').ofLp 4)) ^ 2 ≤ 897695409 / 500000 * ‖u - u'‖ ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_7_5 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 7 - (mlpT u).ofLp 5 - ((mlpT u').ofLp 7 - (mlpT u').ofLp 5)) ^ 2 ≤ 697243359 / 500000 * ‖u - u'‖ ^ 2

theorem Proofs.LipschitzCertDemo.pairSqU_7_6 (u u' : EuclideanSpace ℝ (Fin 49)) :

((mlpT u).ofLp 7 - (mlpT u).ofLp 6 - ((mlpT u').ofLp 7 - (mlpT u').ofLp 6)) ^ 2 ≤ 1325366677 / 500000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.hpreSU0 :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.hpreSU0 = ![1717482 / 522240, 792410 / 522240, 1542943 / 522240, -164427 / 522240, 693313 / 522240, 522014 / 522240, -317895 / 522240, 319339 / 522240]

Instances For

theorem Proofs.LipschitzCertDemo.hpreSU0_eval (k : Fin 8) :

(denseE W1t img0).ofLp k = hpreSU0 k

noncomputable def Proofs.LipschitzCertDemo.logitU0 :

Fin 10 → ℝ

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Proofs.LipschitzCertDemo.logitU0_eval (jj : Fin 10) :

(mlpT img0).ofLp jj = logitU0 jj

theorem Proofs.LipschitzCertDemo.certifiedSU0 (δ : EuclideanSpace ℝ (Fin 49)) (hδ : ‖δ‖ < 1 / 10) (j : Fin 10) :

j ≠ 7 → (mlpT (img0 + δ)).ofLp j < (mlpT (img0 + δ)).ofLp 7

Test #0 (digit 7): LipSDP-per-pair certified at ε = 1/10 — each of the 9 margins clears its own Lp·ε.

noncomputable def Proofs.LipschitzCertDemo.imgU2 :

EuclideanSpace ℝ (Fin 49)

MNIST test image #2 (digit 1), exact pixel sums /4080.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def Proofs.LipschitzCertDemo.hpreSU2 :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.hpreSU2 = ![239277 / 522240, 864005 / 522240, -90548 / 522240, 620813 / 522240, 104666 / 522240, 196749 / 522240, 138281 / 522240, 424291 / 522240]

Instances For

theorem Proofs.LipschitzCertDemo.hpreSU2_eval (k : Fin 8) :

(denseE W1t imgU2).ofLp k = hpreSU2 k

noncomputable def Proofs.LipschitzCertDemo.logitU2 :

Fin 10 → ℝ

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Proofs.LipschitzCertDemo.logitU2_eval (jj : Fin 10) :

(mlpT imgU2).ofLp jj = logitU2 jj

theorem Proofs.LipschitzCertDemo.certifiedSU2 (δ : EuclideanSpace ℝ (Fin 49)) (hδ : ‖δ‖ < 1 / 10) (j : Fin 10) :

j ≠ 1 → (mlpT (imgU2 + δ)).ofLp j < (mlpT (imgU2 + δ)).ofLp 1

Test #2 (digit 1): LipSDP-per-pair certified at ε = 1/10 — each of the 9 margins clears its own Lp·ε.

noncomputable def Proofs.LipschitzCertDemo.hpreSU3 :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.hpreSU3 = ![1725235 / 522240, 301896 / 522240, 1956814 / 522240, 1339878 / 522240, 2483278 / 522240, -600294 / 522240, 35259 / 522240, 1146612 / 522240]

Instances For

theorem Proofs.LipschitzCertDemo.hpreSU3_eval (k : Fin 8) :

(denseE W1t img3).ofLp k = hpreSU3 k

noncomputable def Proofs.LipschitzCertDemo.logitU3 :

Fin 10 → ℝ

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Proofs.LipschitzCertDemo.logitU3_eval (jj : Fin 10) :

(mlpT img3).ofLp jj = logitU3 jj

theorem Proofs.LipschitzCertDemo.certifiedSU3 (δ : EuclideanSpace ℝ (Fin 49)) (hδ : ‖δ‖ < 1 / 10) (j : Fin 10) :

j ≠ 0 → (mlpT (img3 + δ)).ofLp j < (mlpT (img3 + δ)).ofLp 0

Test #3 (digit 0): LipSDP-per-pair certified at ε = 1/10 — each of the 9 margins clears its own Lp·ε.

noncomputable def Proofs.LipschitzCertDemo.imgU4 :

EuclideanSpace ℝ (Fin 49)

MNIST test image #4 (digit 4), exact pixel sums /4080.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def Proofs.LipschitzCertDemo.hpreSU4 :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.hpreSU4 = ![1358428 / 522240, 162524 / 522240, -242326 / 522240, 333886 / 522240, 1398916 / 522240, 507244 / 522240, 630146 / 522240, 999205 / 522240]

Instances For

theorem Proofs.LipschitzCertDemo.hpreSU4_eval (k : Fin 8) :

(denseE W1t imgU4).ofLp k = hpreSU4 k

noncomputable def Proofs.LipschitzCertDemo.logitU4 :

Fin 10 → ℝ

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Proofs.LipschitzCertDemo.logitU4_eval (jj : Fin 10) :

(mlpT imgU4).ofLp jj = logitU4 jj

theorem Proofs.LipschitzCertDemo.certifiedSU4 (δ : EuclideanSpace ℝ (Fin 49)) (hδ : ‖δ‖ < 1 / 10) (j : Fin 10) :

j ≠ 4 → (mlpT (imgU4 + δ)).ofLp j < (mlpT (imgU4 + δ)).ofLp 4

Test #4 (digit 4): LipSDP-per-pair certified at ε = 1/10 — each of the 9 margins clears its own Lp·ε.

noncomputable def Proofs.LipschitzCertDemo.hpreSU5 :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.hpreSU5 = ![455007 / 522240, 1230058 / 522240, -120354 / 522240, 578233 / 522240, 95504 / 522240, 399121 / 522240, 165390 / 522240, 560349 / 522240]

Instances For

theorem Proofs.LipschitzCertDemo.hpreSU5_eval (k : Fin 8) :

(denseE W1t img5).ofLp k = hpreSU5 k

noncomputable def Proofs.LipschitzCertDemo.logitU5 :

Fin 10 → ℝ

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Proofs.LipschitzCertDemo.logitU5_eval (jj : Fin 10) :

(mlpT img5).ofLp jj = logitU5 jj

theorem Proofs.LipschitzCertDemo.certifiedSU5 (δ : EuclideanSpace ℝ (Fin 49)) (hδ : ‖δ‖ < 1 / 10) (j : Fin 10) :

j ≠ 1 → (mlpT (img5 + δ)).ofLp j < (mlpT (img5 + δ)).ofLp 1

Test #5 (digit 1): LipSDP-per-pair certified at ε = 1/10 — each of the 9 margins clears its own Lp·ε.

noncomputable def Proofs.LipschitzCertDemo.imgU6 :

EuclideanSpace ℝ (Fin 49)

MNIST test image #6 (digit 4), exact pixel sums /4080.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def Proofs.LipschitzCertDemo.hpreSU6 :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.hpreSU6 = ![2060344 / 522240, 525512 / 522240, 130902 / 522240, 955580 / 522240, 922054 / 522240, 616169 / 522240, 981877 / 522240, 901152 / 522240]

Instances For

theorem Proofs.LipschitzCertDemo.hpreSU6_eval (k : Fin 8) :

(denseE W1t imgU6).ofLp k = hpreSU6 k

noncomputable def Proofs.LipschitzCertDemo.logitU6 :

Fin 10 → ℝ

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Proofs.LipschitzCertDemo.logitU6_eval (jj : Fin 10) :

(mlpT imgU6).ofLp jj = logitU6 jj

theorem Proofs.LipschitzCertDemo.certifiedSU6 (δ : EuclideanSpace ℝ (Fin 49)) (hδ : ‖δ‖ < 1 / 10) (j : Fin 10) :

j ≠ 4 → (mlpT (imgU6 + δ)).ofLp j < (mlpT (imgU6 + δ)).ofLp 4

Test #6 (digit 4): LipSDP-per-pair certified at ε = 1/10 — each of the 9 margins clears its own Lp·ε.

noncomputable def Proofs.LipschitzCertDemo.hpreSU10 :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.hpreSU10 = ![1145613 / 522240, 144716 / 522240, 2302560 / 522240, 1637067 / 522240, 1687162 / 522240, -658913 / 522240, -158302 / 522240, 1636469 / 522240]

Instances For

theorem Proofs.LipschitzCertDemo.hpreSU10_eval (k : Fin 8) :

(denseE W1t img10).ofLp k = hpreSU10 k

noncomputable def Proofs.LipschitzCertDemo.logitU10 :

Fin 10 → ℝ

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Proofs.LipschitzCertDemo.logitU10_eval (jj : Fin 10) :

(mlpT img10).ofLp jj = logitU10 jj

theorem Proofs.LipschitzCertDemo.certifiedSU10 (δ : EuclideanSpace ℝ (Fin 49)) (hδ : ‖δ‖ < 1 / 10) (j : Fin 10) :

j ≠ 0 → (mlpT (img10 + δ)).ofLp j < (mlpT (img10 + δ)).ofLp 0

Test #10 (digit 0): LipSDP-per-pair certified at ε = 1/10 — each of the 9 margins clears its own Lp·ε.

noncomputable def Proofs.LipschitzCertDemo.imgU11 :

EuclideanSpace ℝ (Fin 49)

MNIST test image #11 (digit 6), exact pixel sums /4080.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def Proofs.LipschitzCertDemo.hpreSU11 :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.hpreSU11 = ![1177305 / 522240, 817026 / 522240, 158188 / 522240, 1289726 / 522240, 1813975 / 522240, 936203 / 522240, 685722 / 522240, 1776372 / 522240]

Instances For

theorem Proofs.LipschitzCertDemo.hpreSU11_eval (k : Fin 8) :

(denseE W1t imgU11).ofLp k = hpreSU11 k

noncomputable def Proofs.LipschitzCertDemo.logitU11 :

Fin 10 → ℝ

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Proofs.LipschitzCertDemo.logitU11_eval (jj : Fin 10) :

(mlpT imgU11).ofLp jj = logitU11 jj

theorem Proofs.LipschitzCertDemo.certifiedSU11 (δ : EuclideanSpace ℝ (Fin 49)) (hδ : ‖δ‖ < 1 / 10) (j : Fin 10) :

j ≠ 6 → (mlpT (imgU11 + δ)).ofLp j < (mlpT (imgU11 + δ)).ofLp 6

Test #11 (digit 6): LipSDP-per-pair certified at ε = 1/10 — each of the 9 margins clears its own Lp·ε.

noncomputable def Proofs.LipschitzCertDemo.sdpUnconCerts :

List (ℕ × EuclideanSpace ℝ (Fin 49) × Fin 10)

LipSDP-certified witnesses on the unconstrained net: (subset index, image, class).

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Proofs.LipschitzCertDemo.sdpUnconCerts_certified (p : ℕ × EuclideanSpace ℝ (Fin 49) × Fin 10) :

p ∈ sdpUnconCerts → CertifiedAt mlpT (1 / 10) p.2.1 p.2.2

theorem Proofs.LipschitzCertDemo.scorecard_sdp_uncon :

sdpUnconCerts.length = 8 ∧ ∀ p ∈ sdpUnconCerts, CertifiedAt mlpT (1 / 10) p.2.1 p.2.2

The LipSDP scorecard — MEASURED 63/100, vs 1/100 under the global √2·∏-norm criterion, same net, same ε, same images; the constant was the bottleneck, not the network. The 8 below are the emitted witnesses carrying CertifiedAt proofs, not that measurement.