Documentation

LeanMlir.Proofs.Certificates.LipschitzCertScorecardSDP

Per-pair LipSDP scorecard — spectrally-capped /256 net (`mlpS`) #

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 34/100 to 69/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·ε (certifiedSC<i>). PGD bracket: 72/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 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.vP01C :

Fin 8 → ℝ

Pair (0,1): ρ = 326.853, Lp = 18.0791 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP01C = ![65 / 128, -207 / 64, 585 / 256, -557 / 256, 9 / 4, -261 / 256, -7 / 128, 423 / 256]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP01C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP01C = ![3599 / 256, 28371 / 1024, 11993 / 512, 7503 / 256, 21523 / 512, 76751 / 1024, 2487 / 256, 16443 / 512]

Instances For

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

vP01C t = W2s 0 t - W2s 1 t

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

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

(∑ k : Fin 8, vP01C k * z k) ^ 2 + 1 / (81713231 / 250000) * ∑ a : Fin 8, ∑ b : Fin 8, tP01C a * z a * (G1s a b * (tP01C b * z b)) ≤ 2 * ∑ k : Fin 8, tP01C k * z k ^ 2

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

((mlpS u).ofLp 0 - (mlpS u).ofLp 1 - ((mlpS u').ofLp 0 - (mlpS u').ofLp 1)) ^ 2 ≤ 81713231 / 250000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP02C :

Fin 8 → ℝ

Pair (0,2): ρ = 130.795, Lp = 11.4366 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP02C = ![51 / 128, -187 / 64, 37 / 32, 17 / 64, -11 / 64, 115 / 256, -77 / 128, 121 / 128]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP02C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP02C = ![3831 / 1024, 3075 / 256, 8455 / 1024, 12985 / 1024, 869 / 128, 16385 / 512, 22473 / 1024, 14281 / 1024]

Instances For

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

vP02C t = W2s 0 t - W2s 2 t

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

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

(∑ k : Fin 8, vP02C k * z k) ^ 2 + 1 / (26159033 / 200000) * ∑ a : Fin 8, ∑ b : Fin 8, tP02C a * z a * (G1s a b * (tP02C b * z b)) ≤ 2 * ∑ k : Fin 8, tP02C k * z k ^ 2

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

((mlpS u).ofLp 0 - (mlpS u).ofLp 2 - ((mlpS u').ofLp 0 - (mlpS u').ofLp 2)) ^ 2 ≤ 26159033 / 200000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP03C :

Fin 8 → ℝ

Pair (0,3): ρ = 124.221, Lp = 11.1455 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP03C = ![-73 / 256, -251 / 128, 179 / 256, -3 / 32, 299 / 128, -151 / 256, -509 / 256, -11 / 64]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP03C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP03C = ![2371 / 256, 5853 / 512, 14465 / 1024, 2133 / 512, 12231 / 1024, 10151 / 512, 25101 / 1024, 18109 / 1024]

Instances For

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

vP03C t = W2s 0 t - W2s 3 t

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

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

(∑ k : Fin 8, vP03C k * z k) ^ 2 + 1 / (24844101 / 200000) * ∑ a : Fin 8, ∑ b : Fin 8, tP03C a * z a * (G1s a b * (tP03C b * z b)) ≤ 2 * ∑ k : Fin 8, tP03C k * z k ^ 2

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

((mlpS u).ofLp 0 - (mlpS u).ofLp 3 - ((mlpS u').ofLp 0 - (mlpS u').ofLp 3)) ^ 2 ≤ 24844101 / 200000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP04C :

Fin 8 → ℝ

Pair (0,4): ρ = 242.261, Lp = 15.5648 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP04C = ![-27 / 32, -27 / 128, 629 / 256, -235 / 128, -21 / 256, 39 / 256, -9 / 4, 593 / 256]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP04C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP04C = ![25083 / 1024, 3505 / 256, 16147 / 1024, 10997 / 512, 521 / 128, 10709 / 1024, 15877 / 512, 10319 / 512]

Instances For

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

vP04C t = W2s 0 t - W2s 4 t

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

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

(∑ k : Fin 8, vP04C k * z k) ^ 2 + 1 / (4845227 / 20000) * ∑ a : Fin 8, ∑ b : Fin 8, tP04C a * z a * (G1s a b * (tP04C b * z b)) ≤ 2 * ∑ k : Fin 8, tP04C k * z k ^ 2

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

((mlpS u).ofLp 0 - (mlpS u).ofLp 4 - ((mlpS u').ofLp 0 - (mlpS u').ofLp 4)) ^ 2 ≤ 4845227 / 20000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP05C :

Fin 8 → ℝ

Pair (0,5): ρ = 86.344, Lp = 9.2922 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP05C = ![1 / 16, -57 / 128, 3 / 64, -301 / 128, 323 / 256, -423 / 256, -183 / 256, 143 / 256]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP05C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP05C = ![679 / 256, 8013 / 1024, 71 / 128, 1197 / 128, 1553 / 128, 7883 / 512, 11051 / 1024, 14525 / 1024]

Instances For

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

vP05C t = W2s 0 t - W2s 5 t

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

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

(∑ k : Fin 8, vP05C k * z k) ^ 2 + 1 / (43171817 / 500000) * ∑ a : Fin 8, ∑ b : Fin 8, tP05C a * z a * (G1s a b * (tP05C b * z b)) ≤ 2 * ∑ k : Fin 8, tP05C k * z k ^ 2

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

((mlpS u).ofLp 0 - (mlpS u).ofLp 5 - ((mlpS u').ofLp 0 - (mlpS u').ofLp 5)) ^ 2 ≤ 43171817 / 500000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP06C :

Fin 8 → ℝ

Pair (0,6): ρ = 210.525, Lp = 14.5095 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP06C = ![3 / 4, -5 / 4, 131 / 64, -149 / 128, -223 / 256, -553 / 256, -95 / 128, 93 / 64]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP06C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP06C = ![271 / 32, 9313 / 512, 6587 / 512, 16461 / 1024, 4729 / 512, 23097 / 1024, 547 / 32, 18565 / 1024]

Instances For

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

vP06C t = W2s 0 t - W2s 6 t

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

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

(∑ k : Fin 8, vP06C k * z k) ^ 2 + 1 / (210525077 / 1000000) * ∑ a : Fin 8, ∑ b : Fin 8, tP06C a * z a * (G1s a b * (tP06C b * z b)) ≤ 2 * ∑ k : Fin 8, tP06C k * z k ^ 2

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

((mlpS u).ofLp 0 - (mlpS u).ofLp 6 - ((mlpS u').ofLp 0 - (mlpS u').ofLp 6)) ^ 2 ≤ 210525077 / 1000000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP07C :

Fin 8 → ℝ

Pair (0,7): ρ = 172.652, Lp = 13.1398 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP07C = ![-645 / 256, -203 / 128, 117 / 256, -37 / 256, 445 / 256, -99 / 256, -5 / 128, 543 / 256]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP07C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP07C = ![3709 / 256, 30685 / 1024, 8171 / 1024, 15393 / 512, 3035 / 256, 4281 / 512, 5675 / 512, 22197 / 1024]

Instances For

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

vP07C t = W2s 0 t - W2s 7 t

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

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

(∑ k : Fin 8, vP07C k * z k) ^ 2 + 1 / (86325969 / 500000) * ∑ a : Fin 8, ∑ b : Fin 8, tP07C a * z a * (G1s a b * (tP07C b * z b)) ≤ 2 * ∑ k : Fin 8, tP07C k * z k ^ 2

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

((mlpS u).ofLp 0 - (mlpS u).ofLp 7 - ((mlpS u').ofLp 0 - (mlpS u').ofLp 7)) ^ 2 ≤ 86325969 / 500000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP08C :

Fin 8 → ℝ

Pair (0,8): ρ = 122.119, Lp = 11.0508 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP08C = ![-171 / 256, -385 / 256, 251 / 128, -263 / 128, 181 / 256, 63 / 128, 9 / 64, -45 / 128]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP08C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP08C = ![18133 / 1024, 2727 / 256, 11127 / 1024, 11907 / 1024, 369 / 32, 19385 / 1024, 8703 / 512, 7999 / 1024]

Instances For

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

vP08C t = W2s 0 t - W2s 8 t

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

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

(∑ k : Fin 8, vP08C k * z k) ^ 2 + 1 / (24423853 / 200000) * ∑ a : Fin 8, ∑ b : Fin 8, tP08C a * z a * (G1s a b * (tP08C b * z b)) ≤ 2 * ∑ k : Fin 8, tP08C k * z k ^ 2

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

((mlpS u).ofLp 0 - (mlpS u).ofLp 8 - ((mlpS u').ofLp 0 - (mlpS u').ofLp 8)) ^ 2 ≤ 24423853 / 200000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP09C :

Fin 8 → ℝ

Pair (0,9): ρ = 207.395, Lp = 14.4013 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP09C = ![-625 / 256, -143 / 256, 23 / 8, -71 / 64, 157 / 128, -51 / 128, -5 / 8, 21 / 32]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP09C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP09C = ![8511 / 512, 6379 / 256, 20307 / 1024, 2157 / 128, 591 / 32, 38965 / 1024, 10183 / 512, 8733 / 1024]

Instances For

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

vP09C t = W2s 0 t - W2s 9 t

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

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

(∑ k : Fin 8, vP09C k * z k) ^ 2 + 1 / (207395497 / 1000000) * ∑ a : Fin 8, ∑ b : Fin 8, tP09C a * z a * (G1s a b * (tP09C b * z b)) ≤ 2 * ∑ k : Fin 8, tP09C k * z k ^ 2

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

((mlpS u).ofLp 0 - (mlpS u).ofLp 9 - ((mlpS u').ofLp 0 - (mlpS u').ofLp 9)) ^ 2 ≤ 207395497 / 1000000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP12C :

Fin 8 → ℝ

Pair (1,2): ρ = 140.445, Lp = 11.8510 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP12C = ![-7 / 64, 5 / 16, -289 / 256, 625 / 256, -155 / 64, 47 / 32, -35 / 64, -181 / 256]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP12C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP12C = ![9203 / 1024, 1919 / 256, 691 / 64, 14743 / 1024, 4151 / 256, 16679 / 512, 16153 / 512, 12513 / 1024]

Instances For

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

vP12C t = W2s 1 t - W2s 2 t

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

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

(∑ k : Fin 8, vP12C k * z k) ^ 2 + 1 / (140445379 / 1000000) * ∑ a : Fin 8, ∑ b : Fin 8, tP12C a * z a * (G1s a b * (tP12C b * z b)) ≤ 2 * ∑ k : Fin 8, tP12C k * z k ^ 2

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

((mlpS u).ofLp 1 - (mlpS u).ofLp 2 - ((mlpS u').ofLp 1 - (mlpS u').ofLp 2)) ^ 2 ≤ 140445379 / 1000000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP13C :

Fin 8 → ℝ

Pair (1,3): ρ = 168.366, Lp = 12.9757 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP13C = ![-203 / 256, 163 / 128, -203 / 128, 533 / 256, 11 / 128, 55 / 128, -495 / 256, -467 / 256]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP13C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP13C = ![9259 / 1024, 13051 / 1024, 10663 / 1024, 8425 / 512, 169 / 64, 17987 / 1024, 38569 / 1024, 9177 / 512]

Instances For

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

vP13C t = W2s 1 t - W2s 3 t

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

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

(∑ k : Fin 8, vP13C k * z k) ^ 2 + 1 / (168366447 / 1000000) * ∑ a : Fin 8, ∑ b : Fin 8, tP13C a * z a * (G1s a b * (tP13C b * z b)) ≤ 2 * ∑ k : Fin 8, tP13C k * z k ^ 2

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

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

noncomputable def Proofs.LipschitzCertDemo.vP14C :

Fin 8 → ℝ

Pair (1,4): ρ = 247.744, Lp = 15.7399 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP14C = ![-173 / 128, 387 / 128, 11 / 64, 87 / 256, -597 / 256, 75 / 64, -281 / 128, 85 / 128]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP14C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP14C = ![18959 / 1024, 9613 / 512, 187 / 32, 26385 / 1024, 6027 / 256, 50511 / 1024, 8459 / 256, 16079 / 1024]

Instances For

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

vP14C t = W2s 1 t - W2s 4 t

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

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

(∑ k : Fin 8, vP14C k * z k) ^ 2 + 1 / (3096799 / 12500) * ∑ a : Fin 8, ∑ b : Fin 8, tP14C a * z a * (G1s a b * (tP14C b * z b)) ≤ 2 * ∑ k : Fin 8, tP14C k * z k ^ 2

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

((mlpS u).ofLp 1 - (mlpS u).ofLp 4 - ((mlpS u').ofLp 1 - (mlpS u').ofLp 4)) ^ 2 ≤ 3096799 / 12500 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP15C :

Fin 8 → ℝ

Pair (1,5): ρ = 181.542, Lp = 13.4738 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP15C = ![-57 / 128, 357 / 128, -573 / 256, -45 / 256, -253 / 256, -81 / 128, -169 / 256, -35 / 32]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP15C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP15C = ![2095 / 256, 15587 / 1024, 16707 / 1024, 3971 / 512, 21567 / 1024, 24639 / 1024, 32099 / 1024, 7585 / 512]

Instances For

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

vP15C t = W2s 1 t - W2s 5 t

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

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

(∑ k : Fin 8, vP15C k * z k) ^ 2 + 1 / (36308333 / 200000) * ∑ a : Fin 8, ∑ b : Fin 8, tP15C a * z a * (G1s a b * (tP15C b * z b)) ≤ 2 * ∑ k : Fin 8, tP15C k * z k ^ 2

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

((mlpS u).ofLp 1 - (mlpS u).ofLp 5 - ((mlpS u').ofLp 1 - (mlpS u').ofLp 5)) ^ 2 ≤ 36308333 / 200000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP16C :

Fin 8 → ℝ

Pair (1,6): ρ = 198.902, Lp = 14.1033 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP16C = ![31 / 128, 127 / 64, -61 / 256, 259 / 256, -799 / 256, -73 / 64, -11 / 16, -51 / 256]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP16C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP16C = ![7223 / 1024, 17081 / 1024, 10469 / 1024, 23927 / 1024, 2099 / 128, 14579 / 1024, 18329 / 1024, 16571 / 1024]

Instances For

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

vP16C t = W2s 1 t - W2s 6 t

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

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

(∑ k : Fin 8, vP16C k * z k) ^ 2 + 1 / (49725519 / 250000) * ∑ a : Fin 8, ∑ b : Fin 8, tP16C a * z a * (G1s a b * (tP16C b * z b)) ≤ 2 * ∑ k : Fin 8, tP16C k * z k ^ 2

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

((mlpS u).ofLp 1 - (mlpS u).ofLp 6 - ((mlpS u').ofLp 1 - (mlpS u').ofLp 6)) ^ 2 ≤ 49725519 / 250000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP17C :

Fin 8 → ℝ

Pair (1,7): ρ = 272.719, Lp = 16.5142 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP17C = ![-775 / 256, 211 / 128, -117 / 64, 65 / 32, -131 / 256, 81 / 128, 1 / 64, 15 / 32]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP17C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP17C = ![5031 / 256, 8099 / 512, 21165 / 1024, 24159 / 1024, 11471 / 1024, 4075 / 256, 949 / 512, 33521 / 1024]

Instances For

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

vP17C t = W2s 1 t - W2s 7 t

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

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

(∑ k : Fin 8, vP17C k * z k) ^ 2 + 1 / (54543723 / 200000) * ∑ a : Fin 8, ∑ b : Fin 8, tP17C a * z a * (G1s a b * (tP17C b * z b)) ≤ 2 * ∑ k : Fin 8, tP17C k * z k ^ 2

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

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

noncomputable def Proofs.LipschitzCertDemo.vP18C :

Fin 8 → ℝ

Pair (1,8): ρ = 114.074, Lp = 10.6806 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP18C = ![-301 / 256, 443 / 256, -83 / 256, 31 / 256, -395 / 256, 387 / 256, 25 / 128, -513 / 256]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP18C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP18C = ![2103 / 256, 2405 / 256, 821 / 256, 2447 / 512, 18271 / 1024, 21617 / 1024, 351 / 32, 16749 / 1024]

Instances For

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

vP18C t = W2s 1 t - W2s 8 t

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

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

(∑ k : Fin 8, vP18C k * z k) ^ 2 + 1 / (114073579 / 1000000) * ∑ a : Fin 8, ∑ b : Fin 8, tP18C a * z a * (G1s a b * (tP18C b * z b)) ≤ 2 * ∑ k : Fin 8, tP18C k * z k ^ 2

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

((mlpS u).ofLp 1 - (mlpS u).ofLp 8 - ((mlpS u').ofLp 1 - (mlpS u').ofLp 8)) ^ 2 ≤ 114073579 / 1000000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP19C :

Fin 8 → ℝ

Pair (1,9): ρ = 248.003, Lp = 15.7482 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP19C = ![-755 / 256, 685 / 256, 151 / 256, 273 / 256, -131 / 128, 159 / 256, -73 / 128, -255 / 256]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP19C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP19C = ![8675 / 512, 18257 / 1024, 21679 / 1024, 2959 / 128, 17323 / 512, 21677 / 1024, 37235 / 1024, 14137 / 256]

Instances For

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

vP19C t = W2s 1 t - W2s 9 t

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

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

(∑ k : Fin 8, vP19C k * z k) ^ 2 + 1 / (62000749 / 250000) * ∑ a : Fin 8, ∑ b : Fin 8, tP19C a * z a * (G1s a b * (tP19C b * z b)) ≤ 2 * ∑ k : Fin 8, tP19C k * z k ^ 2

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

((mlpS u).ofLp 1 - (mlpS u).ofLp 9 - ((mlpS u').ofLp 1 - (mlpS u').ofLp 9)) ^ 2 ≤ 62000749 / 250000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP24C :

Fin 8 → ℝ

Pair (2,4): ρ = 236.477, Lp = 15.3779 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP24C = ![-159 / 128, 347 / 128, 333 / 256, -269 / 128, 23 / 256, -19 / 64, -211 / 128, 351 / 256]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP24C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP24C = ![113 / 8, 9819 / 512, 7633 / 512, 24911 / 1024, 7233 / 1024, 18367 / 1024, 28015 / 1024, 17781 / 1024]

Instances For

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

vP24C t = W2s 2 t - W2s 4 t

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

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

(∑ k : Fin 8, vP24C k * z k) ^ 2 + 1 / (236476997 / 1000000) * ∑ a : Fin 8, ∑ b : Fin 8, tP24C a * z a * (G1s a b * (tP24C b * z b)) ≤ 2 * ∑ k : Fin 8, tP24C k * z k ^ 2

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

((mlpS u).ofLp 2 - (mlpS u).ofLp 4 - ((mlpS u').ofLp 2 - (mlpS u').ofLp 4)) ^ 2 ≤ 236476997 / 1000000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP27C :

Fin 8 → ℝ

Pair (2,7): ρ = 229.528, Lp = 15.1502 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP27C = ![-747 / 256, 171 / 128, -179 / 256, -105 / 256, 489 / 256, -107 / 128, 9 / 16, 301 / 256]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP27C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP27C = ![247 / 16, 13725 / 1024, 9573 / 512, 14247 / 512, 7813 / 512, 623 / 32, 16945 / 512, 34991 / 1024]

Instances For

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

vP27C t = W2s 2 t - W2s 7 t

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

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

(∑ k : Fin 8, vP27C k * z k) ^ 2 + 1 / (57382081 / 250000) * ∑ a : Fin 8, ∑ b : Fin 8, tP27C a * z a * (G1s a b * (tP27C b * z b)) ≤ 2 * ∑ k : Fin 8, tP27C k * z k ^ 2

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

((mlpS u).ofLp 2 - (mlpS u).ofLp 7 - ((mlpS u').ofLp 2 - (mlpS u').ofLp 7)) ^ 2 ≤ 57382081 / 250000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP29C :

Fin 8 → ℝ

Pair (2,9): ρ = 260.273, Lp = 16.1330 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP29C = ![-727 / 256, 605 / 256, 55 / 32, -11 / 8, 179 / 128, -217 / 256, -3 / 128, -37 / 128]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP29C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP29C = ![17767 / 1024, 20453 / 1024, 8315 / 256, 27519 / 1024, 5325 / 256, 13549 / 256, 2213 / 1024, 8787 / 1024]

Instances For

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

vP29C t = W2s 2 t - W2s 9 t

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

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

(∑ k : Fin 8, vP29C k * z k) ^ 2 + 1 / (65068279 / 250000) * ∑ a : Fin 8, ∑ b : Fin 8, tP29C a * z a * (G1s a b * (tP29C b * z b)) ≤ 2 * ∑ k : Fin 8, tP29C k * z k ^ 2

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

((mlpS u).ofLp 2 - (mlpS u).ofLp 9 - ((mlpS u').ofLp 2 - (mlpS u').ofLp 9)) ^ 2 ≤ 65068279 / 250000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP34C :

Fin 8 → ℝ

Pair (3,4): ρ = 271.821, Lp = 16.4870 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP34C = ![-143 / 256, 7 / 4, 225 / 128, -223 / 128, -619 / 256, 95 / 128, -67 / 256, 637 / 256]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP34C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP34C = ![19833 / 512, 21205 / 1024, 1887 / 128, 27055 / 1024, 5795 / 256, 29029 / 1024, 4883 / 512, 12475 / 512]

Instances For

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

vP34C t = W2s 3 t - W2s 4 t

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

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

(∑ k : Fin 8, vP34C k * z k) ^ 2 + 1 / (271820749 / 1000000) * ∑ a : Fin 8, ∑ b : Fin 8, tP34C a * z a * (G1s a b * (tP34C b * z b)) ≤ 2 * ∑ k : Fin 8, tP34C k * z k ^ 2

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

((mlpS u).ofLp 3 - (mlpS u).ofLp 4 - ((mlpS u').ofLp 3 - (mlpS u').ofLp 4)) ^ 2 ≤ 271820749 / 1000000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP37C :

Fin 8 → ℝ

Pair (3,7): ρ = 128.578, Lp = 11.3393 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP37C = ![-143 / 64, 3 / 8, -31 / 128, -13 / 256, -153 / 256, 13 / 64, 499 / 256, 587 / 256]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP37C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP37C = ![10659 / 1024, 4199 / 1024, 6019 / 1024, 2997 / 1024, 10769 / 1024, 983 / 256, 24365 / 1024, 533 / 32]

Instances For

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

vP37C t = W2s 3 t - W2s 7 t

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

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

(∑ k : Fin 8, vP37C k * z k) ^ 2 + 1 / (64289067 / 500000) * ∑ a : Fin 8, ∑ b : Fin 8, tP37C a * z a * (G1s a b * (tP37C b * z b)) ≤ 2 * ∑ k : Fin 8, tP37C k * z k ^ 2

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

((mlpS u).ofLp 3 - (mlpS u).ofLp 7 - ((mlpS u').ofLp 3 - (mlpS u').ofLp 7)) ^ 2 ≤ 64289067 / 500000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP39C :

Fin 8 → ℝ

Pair (3,9): ρ = 177.684, Lp = 13.3299 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP39C = ![-69 / 32, 359 / 256, 557 / 256, -65 / 64, -71 / 64, 49 / 256, 349 / 256, 53 / 64]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP39C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP39C = ![15749 / 1024, 3035 / 256, 3743 / 256, 16293 / 1024, 9303 / 512, 7059 / 512, 14453 / 256, 9303 / 1024]

Instances For

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

vP39C t = W2s 3 t - W2s 9 t

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

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

(∑ k : Fin 8, vP39C k * z k) ^ 2 + 1 / (177683991 / 1000000) * ∑ a : Fin 8, ∑ b : Fin 8, tP39C a * z a * (G1s a b * (tP39C b * z b)) ≤ 2 * ∑ k : Fin 8, tP39C k * z k ^ 2

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

((mlpS u).ofLp 3 - (mlpS u).ofLp 9 - ((mlpS u').ofLp 3 - (mlpS u').ofLp 9)) ^ 2 ≤ 177683991 / 1000000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP45C :

Fin 8 → ℝ

Pair (4,5): ρ = 176.781, Lp = 13.2960 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP45C = ![29 / 32, -15 / 64, -617 / 256, -33 / 64, 43 / 32, -231 / 128, 393 / 256, -225 / 128]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP45C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP45C = ![535 / 32, 839 / 128, 6857 / 512, 12325 / 512, 16503 / 1024, 2829 / 64, 2867 / 128, 6601 / 512]

Instances For

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

vP45C t = W2s 4 t - W2s 5 t

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

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

(∑ k : Fin 8, vP45C k * z k) ^ 2 + 1 / (176781459 / 1000000) * ∑ a : Fin 8, ∑ b : Fin 8, tP45C a * z a * (G1s a b * (tP45C b * z b)) ≤ 2 * ∑ k : Fin 8, tP45C k * z k ^ 2

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

((mlpS u).ofLp 4 - (mlpS u).ofLp 5 - ((mlpS u').ofLp 4 - (mlpS u').ofLp 5)) ^ 2 ≤ 176781459 / 1000000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP46C :

Fin 8 → ℝ

Pair (4,6): ρ = 139.150, Lp = 11.7962 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP46C = ![51 / 32, -133 / 128, -105 / 256, 43 / 64, -101 / 128, -37 / 16, 193 / 128, -221 / 256]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP46C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP46C = ![4275 / 512, 4647 / 512, 13701 / 1024, 17575 / 1024, 7255 / 1024, 18609 / 1024, 3281 / 128, 1421 / 128]

Instances For

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

vP46C t = W2s 4 t - W2s 6 t

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

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

(∑ k : Fin 8, vP46C k * z k) ^ 2 + 1 / (139149989 / 1000000) * ∑ a : Fin 8, ∑ b : Fin 8, tP46C a * z a * (G1s a b * (tP46C b * z b)) ≤ 2 * ∑ k : Fin 8, tP46C k * z k ^ 2

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

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

noncomputable def Proofs.LipschitzCertDemo.vP47C :

Fin 8 → ℝ

Pair (4,7): ρ = 236.731, Lp = 15.3861 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP47C = ![-429 / 256, -11 / 8, -2, 433 / 256, 233 / 128, -69 / 128, 283 / 128, -25 / 128]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP47C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP47C = ![9375 / 512, 1993 / 64, 17343 / 1024, 2551 / 128, 14645 / 1024, 11401 / 1024, 15121 / 512, 1087 / 256]

Instances For

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

vP47C t = W2s 4 t - W2s 7 t

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

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

(∑ k : Fin 8, vP47C k * z k) ^ 2 + 1 / (236730533 / 1000000) * ∑ a : Fin 8, ∑ b : Fin 8, tP47C a * z a * (G1s a b * (tP47C b * z b)) ≤ 2 * ∑ k : Fin 8, tP47C k * z k ^ 2

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

((mlpS u).ofLp 4 - (mlpS u).ofLp 7 - ((mlpS u').ofLp 4 - (mlpS u').ofLp 7)) ^ 2 ≤ 236730533 / 1000000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP48C :

Fin 8 → ℝ

Pair (4,8): ρ = 152.955, Lp = 12.3676 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP48C = ![45 / 256, -331 / 256, -127 / 256, -7 / 32, 101 / 128, 87 / 256, 153 / 64, -683 / 256]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP48C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP48C = ![7615 / 1024, 10953 / 1024, 4417 / 1024, 27063 / 1024, 2499 / 256, 4569 / 512, 21429 / 1024, 8423 / 512]

Instances For

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

vP48C t = W2s 4 t - W2s 8 t

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

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

(∑ k : Fin 8, vP48C k * z k) ^ 2 + 1 / (76477547 / 500000) * ∑ a : Fin 8, ∑ b : Fin 8, tP48C a * z a * (G1s a b * (tP48C b * z b)) ≤ 2 * ∑ k : Fin 8, tP48C k * z k ^ 2

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

((mlpS u).ofLp 4 - (mlpS u).ofLp 8 - ((mlpS u').ofLp 4 - (mlpS u').ofLp 8)) ^ 2 ≤ 76477547 / 500000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP49C :

Fin 8 → ℝ

Pair (4,9): ρ = 107.859, Lp = 10.3856 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP49C = ![-409 / 256, -89 / 256, 107 / 256, 93 / 128, 335 / 256, -141 / 256, 13 / 8, -425 / 256]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP49C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP49C = ![8353 / 1024, 8059 / 512, 2021 / 512, 5173 / 512, 457 / 64, 9677 / 1024, 15347 / 1024, 13365 / 1024]

Instances For

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

vP49C t = W2s 4 t - W2s 9 t

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

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

(∑ k : Fin 8, vP49C k * z k) ^ 2 + 1 / (53929533 / 500000) * ∑ a : Fin 8, ∑ b : Fin 8, tP49C a * z a * (G1s a b * (tP49C b * z b)) ≤ 2 * ∑ k : Fin 8, tP49C k * z k ^ 2

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

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

noncomputable def Proofs.LipschitzCertDemo.vP57C :

Fin 8 → ℝ

Pair (5,7): ρ = 187.028, Lp = 13.6759 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP57C = ![-661 / 256, -73 / 64, 105 / 256, 565 / 256, 61 / 128, 81 / 64, 173 / 256, 25 / 16]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP57C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP57C = ![7195 / 512, 13217 / 512, 509 / 16, 2473 / 128, 6127 / 1024, 16649 / 1024, 25113 / 1024, 5417 / 256]

Instances For

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

vP57C t = W2s 5 t - W2s 7 t

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

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

(∑ k : Fin 8, vP57C k * z k) ^ 2 + 1 / (23378523 / 125000) * ∑ a : Fin 8, ∑ b : Fin 8, tP57C a * z a * (G1s a b * (tP57C b * z b)) ≤ 2 * ∑ k : Fin 8, tP57C k * z k ^ 2

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

((mlpS u).ofLp 5 - (mlpS u).ofLp 7 - ((mlpS u').ofLp 5 - (mlpS u').ofLp 7)) ^ 2 ≤ 23378523 / 125000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP59C :

Fin 8 → ℝ

Pair (5,9): ρ = 165.891, Lp = 12.8799 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP59C = ![-641 / 256, -29 / 256, 181 / 64, 159 / 128, -9 / 256, 321 / 256, 23 / 256, 25 / 256]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP59C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP59C = ![1733 / 128, 3877 / 1024, 20283 / 1024, 3349 / 128, 327 / 256, 6003 / 256, 173 / 16, 1379 / 1024]

Instances For

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

vP59C t = W2s 5 t - W2s 9 t

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

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

(∑ k : Fin 8, vP59C k * z k) ^ 2 + 1 / (165891061 / 1000000) * ∑ a : Fin 8, ∑ b : Fin 8, tP59C a * z a * (G1s a b * (tP59C b * z b)) ≤ 2 * ∑ k : Fin 8, tP59C k * z k ^ 2

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

((mlpS u).ofLp 5 - (mlpS u).ofLp 9 - ((mlpS u').ofLp 5 - (mlpS u').ofLp 9)) ^ 2 ≤ 165891061 / 1000000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP67C :

Fin 8 → ℝ

Pair (6,7): ρ = 380.417, Lp = 19.5043 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP67C = ![-837 / 256, -43 / 128, -407 / 256, 261 / 256, 167 / 64, 227 / 128, 45 / 64, 171 / 256]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP67C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP67C = ![13175 / 512, 3839 / 256, 12027 / 512, 6851 / 256, 359 / 16, 27373 / 1024, 29739 / 1024, 1601 / 32]

Instances For

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

vP67C t = W2s 6 t - W2s 7 t

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

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

(∑ k : Fin 8, vP67C k * z k) ^ 2 + 1 / (3804171 / 10000) * ∑ a : Fin 8, ∑ b : Fin 8, tP67C a * z a * (G1s a b * (tP67C b * z b)) ≤ 2 * ∑ k : Fin 8, tP67C k * z k ^ 2

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

((mlpS u).ofLp 6 - (mlpS u).ofLp 7 - ((mlpS u').ofLp 6 - (mlpS u').ofLp 7)) ^ 2 ≤ 3804171 / 10000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP69C :

Fin 8 → ℝ

Pair (6,9): ρ = 273.484, Lp = 16.5374 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP69C = ![-817 / 256, 177 / 256, 53 / 64, 7 / 128, 537 / 256, 451 / 256, 15 / 128, -51 / 64]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP69C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP69C = ![19023 / 1024, 6889 / 512, 11073 / 512, 5295 / 1024, 8439 / 512, 23735 / 1024, 9455 / 1024, 12233 / 256]

Instances For

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

vP69C t = W2s 6 t - W2s 9 t

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

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

(∑ k : Fin 8, vP69C k * z k) ^ 2 + 1 / (136741937 / 500000) * ∑ a : Fin 8, ∑ b : Fin 8, tP69C a * z a * (G1s a b * (tP69C b * z b)) ≤ 2 * ∑ k : Fin 8, tP69C k * z k ^ 2

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

((mlpS u).ofLp 6 - (mlpS u).ofLp 9 - ((mlpS u').ofLp 6 - (mlpS u').ofLp 9)) ^ 2 ≤ 136741937 / 500000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP78C :

Fin 8 → ℝ

Pair (7,8): ρ = 159.433, Lp = 12.6267 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP78C = ![237 / 128, 21 / 256, 385 / 256, -489 / 256, -33 / 32, 225 / 256, 23 / 128, -633 / 256]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP78C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP78C = ![11561 / 1024, 383 / 256, 2687 / 128, 1863 / 128, 1133 / 128, 17699 / 1024, 18107 / 1024, 14375 / 512]

Instances For

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

vP78C t = W2s 7 t - W2s 8 t

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

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

(∑ k : Fin 8, vP78C k * z k) ^ 2 + 1 / (6377309 / 40000) * ∑ a : Fin 8, ∑ b : Fin 8, tP78C a * z a * (G1s a b * (tP78C b * z b)) ≤ 2 * ∑ k : Fin 8, tP78C k * z k ^ 2

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

((mlpS u).ofLp 7 - (mlpS u).ofLp 8 - ((mlpS u').ofLp 7 - (mlpS u').ofLp 8)) ^ 2 ≤ 6377309 / 40000 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.vP79C :

Fin 8 → ℝ

Pair (7,9): ρ = 94.597, Lp = 9.7261 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP79C = ![5 / 64, 263 / 256, 619 / 256, -247 / 256, -131 / 256, -3 / 256, -75 / 128, -375 / 256]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP79C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP79C = ![12205 / 1024, 10665 / 1024, 9059 / 1024, 7231 / 1024, 4401 / 1024, 55 / 256, 3961 / 512, 889 / 64]

Instances For

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

vP79C t = W2s 7 t - W2s 9 t

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

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

(∑ k : Fin 8, vP79C k * z k) ^ 2 + 1 / (94596901 / 1000000) * ∑ a : Fin 8, ∑ b : Fin 8, tP79C a * z a * (G1s a b * (tP79C b * z b)) ≤ 2 * ∑ k : Fin 8, tP79C k * z k ^ 2

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

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

noncomputable def Proofs.LipschitzCertDemo.vP89C :

Fin 8 → ℝ

Pair (8,9): ρ = 97.979, Lp = 9.8985 (√2·L-product criterion would need 27.95).

Equations

Proofs.LipschitzCertDemo.vP89C = ![-227 / 128, 121 / 128, 117 / 128, 121 / 128, 133 / 256, -57 / 64, -49 / 64, 129 / 128]

Instances For

noncomputable def Proofs.LipschitzCertDemo.tP89C :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.tP89C = ![7403 / 1024, 2987 / 512, 2183 / 256, 12561 / 1024, 9809 / 1024, 3029 / 128, 5825 / 512, 509 / 64]

Instances For

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

vP89C t = W2s 8 t - W2s 9 t

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

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

(∑ k : Fin 8, vP89C k * z k) ^ 2 + 1 / (1224737 / 12500) * ∑ a : Fin 8, ∑ b : Fin 8, tP89C a * z a * (G1s a b * (tP89C b * z b)) ≤ 2 * ∑ k : Fin 8, tP89C k * z k ^ 2

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

((mlpS u).ofLp 8 - (mlpS u).ofLp 9 - ((mlpS u').ofLp 8 - (mlpS u').ofLp 9)) ^ 2 ≤ 1224737 / 12500 * ‖u - u'‖ ^ 2

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

((mlpS u).ofLp 1 - (mlpS u).ofLp 0 - ((mlpS u').ofLp 1 - (mlpS u').ofLp 0)) ^ 2 ≤ 81713231 / 250000 * ‖u - u'‖ ^ 2

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

((mlpS u).ofLp 4 - (mlpS u).ofLp 0 - ((mlpS u').ofLp 4 - (mlpS u').ofLp 0)) ^ 2 ≤ 4845227 / 20000 * ‖u - u'‖ ^ 2

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

((mlpS u).ofLp 4 - (mlpS u).ofLp 1 - ((mlpS u').ofLp 4 - (mlpS u').ofLp 1)) ^ 2 ≤ 3096799 / 12500 * ‖u - u'‖ ^ 2

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

((mlpS u).ofLp 4 - (mlpS u).ofLp 2 - ((mlpS u').ofLp 4 - (mlpS u').ofLp 2)) ^ 2 ≤ 236476997 / 1000000 * ‖u - u'‖ ^ 2

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

((mlpS u).ofLp 4 - (mlpS u).ofLp 3 - ((mlpS u').ofLp 4 - (mlpS u').ofLp 3)) ^ 2 ≤ 271820749 / 1000000 * ‖u - u'‖ ^ 2

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

((mlpS u).ofLp 7 - (mlpS u).ofLp 0 - ((mlpS u').ofLp 7 - (mlpS u').ofLp 0)) ^ 2 ≤ 86325969 / 500000 * ‖u - u'‖ ^ 2

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

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

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

((mlpS u).ofLp 7 - (mlpS u).ofLp 2 - ((mlpS u').ofLp 7 - (mlpS u').ofLp 2)) ^ 2 ≤ 57382081 / 250000 * ‖u - u'‖ ^ 2

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

((mlpS u).ofLp 7 - (mlpS u).ofLp 3 - ((mlpS u').ofLp 7 - (mlpS u').ofLp 3)) ^ 2 ≤ 64289067 / 500000 * ‖u - u'‖ ^ 2

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

((mlpS u).ofLp 7 - (mlpS u).ofLp 4 - ((mlpS u').ofLp 7 - (mlpS u').ofLp 4)) ^ 2 ≤ 236730533 / 1000000 * ‖u - u'‖ ^ 2

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

((mlpS u).ofLp 7 - (mlpS u).ofLp 5 - ((mlpS u').ofLp 7 - (mlpS u').ofLp 5)) ^ 2 ≤ 23378523 / 125000 * ‖u - u'‖ ^ 2

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

((mlpS u).ofLp 7 - (mlpS u).ofLp 6 - ((mlpS u').ofLp 7 - (mlpS u').ofLp 6)) ^ 2 ≤ 3804171 / 10000 * ‖u - u'‖ ^ 2

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

((mlpS u).ofLp 9 - (mlpS u).ofLp 0 - ((mlpS u').ofLp 9 - (mlpS u').ofLp 0)) ^ 2 ≤ 207395497 / 1000000 * ‖u - u'‖ ^ 2

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

((mlpS u).ofLp 9 - (mlpS u).ofLp 1 - ((mlpS u').ofLp 9 - (mlpS u').ofLp 1)) ^ 2 ≤ 62000749 / 250000 * ‖u - u'‖ ^ 2

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

((mlpS u).ofLp 9 - (mlpS u).ofLp 2 - ((mlpS u').ofLp 9 - (mlpS u').ofLp 2)) ^ 2 ≤ 65068279 / 250000 * ‖u - u'‖ ^ 2

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

((mlpS u).ofLp 9 - (mlpS u).ofLp 3 - ((mlpS u').ofLp 9 - (mlpS u').ofLp 3)) ^ 2 ≤ 177683991 / 1000000 * ‖u - u'‖ ^ 2

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

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

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

((mlpS u).ofLp 9 - (mlpS u).ofLp 5 - ((mlpS u').ofLp 9 - (mlpS u').ofLp 5)) ^ 2 ≤ 165891061 / 1000000 * ‖u - u'‖ ^ 2

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

((mlpS u).ofLp 9 - (mlpS u).ofLp 6 - ((mlpS u').ofLp 9 - (mlpS u').ofLp 6)) ^ 2 ≤ 136741937 / 500000 * ‖u - u'‖ ^ 2

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

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

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

((mlpS u).ofLp 9 - (mlpS u).ofLp 8 - ((mlpS u').ofLp 9 - (mlpS u').ofLp 8)) ^ 2 ≤ 1224737 / 12500 * ‖u - u'‖ ^ 2

noncomputable def Proofs.LipschitzCertDemo.logitC0 :

Fin 10 → ℝ

Equations

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

Instances For

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

(mlpS img0).ofLp jj = logitC0 jj

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

j ≠ 7 → (mlpS (img0 + δ)).ofLp j < (mlpS (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.img2 :

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.hpreSC2 :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.hpreSC2 = ![250140 / 1044480, 1657842 / 1044480, -28945 / 1044480, 1260177 / 1044480, 128905 / 1044480, 5451 / 1044480, 122262 / 1044480, 145311 / 1044480]

Instances For

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

(denseE W1s img2).ofLp k = hpreSC2 k

noncomputable def Proofs.LipschitzCertDemo.logitC2 :

Fin 10 → ℝ

Equations

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

Instances For

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

(mlpS img2).ofLp jj = logitC2 jj

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

j ≠ 1 → (mlpS (img2 + δ)).ofLp j < (mlpS (img2 + δ)).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.logitC3 :

Fin 10 → ℝ

Equations

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

Instances For

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

(mlpS img3).ofLp jj = logitC3 jj

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

j ≠ 0 → (mlpS (img3 + δ)).ofLp j < (mlpS (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.img4 :

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.hpreSC4 :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.hpreSC4 = ![1758289 / 1044480, 159850 / 1044480, 192729 / 1044480, 385343 / 1044480, 2448526 / 1044480, -136103 / 1044480, 1263072 / 1044480, 346246 / 1044480]

Instances For

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

(denseE W1s img4).ofLp k = hpreSC4 k

noncomputable def Proofs.LipschitzCertDemo.logitC4 :

Fin 10 → ℝ

Equations

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

Instances For

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

(mlpS img4).ofLp jj = logitC4 jj

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

j ≠ 4 → (mlpS (img4 + δ)).ofLp j < (mlpS (img4 + δ)).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.logitC5 :

Fin 10 → ℝ

Equations

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

Instances For

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

(mlpS img5).ofLp jj = logitC5 jj

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

j ≠ 1 → (mlpS (img5 + δ)).ofLp j < (mlpS (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.img6 :

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.hpreSC6 :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.hpreSC6 = ![1979379 / 1044480, 101552 / 1044480, 348154 / 1044480, 1847224 / 1044480, 1283821 / 1044480, 77322 / 1044480, 1902224 / 1044480, 433740 / 1044480]

Instances For

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

(denseE W1s img6).ofLp k = hpreSC6 k

noncomputable def Proofs.LipschitzCertDemo.logitC6 :

Fin 10 → ℝ

Equations

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

Instances For

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

(mlpS img6).ofLp jj = logitC6 jj

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

j ≠ 4 → (mlpS (img6 + δ)).ofLp j < (mlpS (img6 + δ)).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.img7 :

EuclideanSpace ℝ (Fin 49)

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

Equations

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

Instances For

noncomputable def Proofs.LipschitzCertDemo.hpreSC7 :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.hpreSC7 = ![2223409 / 1044480, 111943 / 1044480, 201603 / 1044480, 1232868 / 1044480, 984869 / 1044480, 684666 / 1044480, 1212606 / 1044480, 1015202 / 1044480]

Instances For

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

(denseE W1s img7).ofLp k = hpreSC7 k

noncomputable def Proofs.LipschitzCertDemo.logitC7 :

Fin 10 → ℝ

Equations

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

Instances For

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

(mlpS img7).ofLp jj = logitC7 jj

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

j ≠ 9 → (mlpS (img7 + δ)).ofLp j < (mlpS (img7 + δ)).ofLp 9

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

noncomputable def Proofs.LipschitzCertDemo.img9 :

EuclideanSpace ℝ (Fin 49)

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

Equations

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

Instances For

noncomputable def Proofs.LipschitzCertDemo.hpreSC9 :

Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.hpreSC9 = ![3747783 / 1044480, 65104 / 1044480, 624723 / 1044480, 1968160 / 1044480, 1271717 / 1044480, -439488 / 1044480, 1433475 / 1044480, 543095 / 1044480]

Instances For

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

(denseE W1s img9).ofLp k = hpreSC9 k

noncomputable def Proofs.LipschitzCertDemo.logitC9 :

Fin 10 → ℝ

Equations

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

Instances For

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

(mlpS img9).ofLp jj = logitC9 jj

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

j ≠ 9 → (mlpS (img9 + δ)).ofLp j < (mlpS (img9 + δ)).ofLp 9

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

noncomputable def Proofs.LipschitzCertDemo.sdpCappedCerts :

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

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

Equations

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

Instances For

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

p ∈ sdpCappedCerts → CertifiedAt mlpS (1 / 10) p.2.1 p.2.2

theorem Proofs.LipschitzCertDemo.scorecard_sdp :

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

The LipSDP scorecard — MEASURED 69/100, vs 34/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.