Documentation

LeanMlir.Proofs.Training.Trained.CnnDescentConv1

Descent at TRAINED weights — the CNN conv1 rungs, through two-layer twins #

REDUCED CERTIFICATE MODEL — the same 12×12-input, 2-channel MNIST CNN shape as Trained.CnnDescent, NOT the canonical 28×28, 32-channel cnnVerified, chosen so every table is exact rational arithmetic in the kernel.

cnn_conv1_exact_sgd_descends and cnn_conv1_bias_exact_sgd_descends — one exact-gradient SGD step on the FIRST conv's kernel, or its bias, decreases the cross-entropy loss — instantiated at TRAINED, /128-rationalized weights (biases /16384) and REAL MNIST test image #0 (label 7, classified correctly), every hypothesis discharged by exact arithmetic: trained_cnn_conv1_sgd_descends_concrete at learning rate 2⁻48 and trained_cnn_conv1_bias_sgd_descends_concrete at 2⁻45 (its radius sits inside the kernel rung's, so every relu and pool margin carries over by monotonicity).

This net has a trained conv1 bias. Trained.CnnDescent's bias-free conv1 cannot serve these rungs: their relu₁ margin needs every conv1 pre-activation nonzero, and a bias-free conv1 is exactly zero on a blank patch.

The pool hypothesis takes two-layer twins ConvPatchEq2 3 3 T0: conv2-output cells whose 5×5 receptive fields through both convs lie in a blank image region, every outer read in bounds (tw_*), so their conv2 outputs are equal for every conv1 kernel and bias. 2 live windows tie that way and 13 are dead; every other cell clears the margin (cert_*, through windowMarginUpTo_of_cert). No pool-tie regularizer was used in training.

Net: 24×24-center-cropped MNIST, 2×2 block sums to 12×12 (exact pixel sums /1020), conv 1→2 3×3 SAME + bias → relu → conv 2→2 3×3 SAME → relu → maxpool 2×2 → dense 72→8 → relu → dense 8→8 → relu → dense 8→10. The generator prints the net's test accuracy.

As in Trained.CnnDescent, the step is the exact gradient and the decrease lr·‖∇L‖₂²/2 is not shown positive. Generated by scripts/certs/trained_cnn_descent.py; weights and input are DATA.

noncomputable def Proofs.TrainedCnnDescentConv1.T0 :

Tensor3 1 12 12

Test image #0, center-cropped and 2×2-summed to 12×12, exact pixel sums /1020.

Equations

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

Instances For

noncomputable def Proofs.TrainedCnnDescentConv1.W1 :

Kernel4 2 1 3 3

conv1 kernel (1→2, 3×3), entries k/128.

Equations

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

Instances For

noncomputable def Proofs.TrainedCnnDescentConv1.b1 :

Equations

Proofs.TrainedCnnDescentConv1.b1 = ![787 / 8192, 1549 / 16384]

Instances For

noncomputable def Proofs.TrainedCnnDescentConv1.W2 :

Kernel4 2 2 3 3

conv2 kernel (2→2, 3×3), entries k/128.

Equations

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

Instances For

noncomputable def Proofs.TrainedCnnDescentConv1.b2 :

Equations

Proofs.TrainedCnnDescentConv1.b2 = ![-4555 / 16384, -3369 / 16384]

Instances For

noncomputable def Proofs.TrainedCnnDescentConv1.W3 :

Mat (2 * 6 * 6) 8

dense3 (72→8, input×output).

Equations

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

Instances For

noncomputable def Proofs.TrainedCnnDescentConv1.b3 :

Equations

Proofs.TrainedCnnDescentConv1.b3 = ![545 / 4096, -341 / 4096, 2927 / 16384, 943 / 4096, 197 / 2048, 4971 / 16384, 689 / 8192, 819 / 8192]

Instances For

noncomputable def Proofs.TrainedCnnDescentConv1.W4 :

Mat 8 8

Equations

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

Instances For

noncomputable def Proofs.TrainedCnnDescentConv1.b4 :

Equations

Proofs.TrainedCnnDescentConv1.b4 = ![3117 / 8192, 2503 / 16384, -5837 / 8192, 3485 / 16384, 49 / 512, 5891 / 16384, 793 / 8192, 7749 / 16384]

Instances For

noncomputable def Proofs.TrainedCnnDescentConv1.W5 :

Mat 8 10

Equations

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

Instances For

noncomputable def Proofs.TrainedCnnDescentConv1.b5 :

Vec 10

Equations

Proofs.TrainedCnnDescentConv1.b5 = ![-7579 / 16384, 2609 / 4096, -4699 / 16384, -1565 / 16384, -1591 / 16384, 2031 / 4096, 433 / 16384, 3493 / 16384, -1781 / 2048, 1799 / 4096]

Instances For

def Proofs.TrainedCnnDescentConv1.lbl :

Fin 10

The label of test image #0.

Equations

Proofs.TrainedCnnDescentConv1.lbl = 7

Instances For

theorem Proofs.TrainedCnnDescentConv1.x0_bound_r0_0 (wi : Fin 12) :

|T0 ⟨0, ⋯⟩ ⟨0, ⋯⟩ wi| ≤ 1

theorem Proofs.TrainedCnnDescentConv1.x0_bound_r0_1 (wi : Fin 12) :

|T0 ⟨0, ⋯⟩ ⟨1, ⋯⟩ wi| ≤ 1

theorem Proofs.TrainedCnnDescentConv1.x0_bound_r0_2 (wi : Fin 12) :

|T0 ⟨0, ⋯⟩ ⟨2, ⋯⟩ wi| ≤ 1

theorem Proofs.TrainedCnnDescentConv1.x0_bound_r0_3 (wi : Fin 12) :

|T0 ⟨0, ⋯⟩ ⟨3, ⋯⟩ wi| ≤ 1

theorem Proofs.TrainedCnnDescentConv1.x0_bound_r0_4 (wi : Fin 12) :

|T0 ⟨0, ⋯⟩ ⟨4, ⋯⟩ wi| ≤ 1

theorem Proofs.TrainedCnnDescentConv1.x0_bound_r0_5 (wi : Fin 12) :

|T0 ⟨0, ⋯⟩ ⟨5, ⋯⟩ wi| ≤ 1

theorem Proofs.TrainedCnnDescentConv1.x0_bound_r0_6 (wi : Fin 12) :

|T0 ⟨0, ⋯⟩ ⟨6, ⋯⟩ wi| ≤ 1

theorem Proofs.TrainedCnnDescentConv1.x0_bound_r0_7 (wi : Fin 12) :

|T0 ⟨0, ⋯⟩ ⟨7, ⋯⟩ wi| ≤ 1

theorem Proofs.TrainedCnnDescentConv1.x0_bound_r0_8 (wi : Fin 12) :

|T0 ⟨0, ⋯⟩ ⟨8, ⋯⟩ wi| ≤ 1

theorem Proofs.TrainedCnnDescentConv1.x0_bound_r0_9 (wi : Fin 12) :

|T0 ⟨0, ⋯⟩ ⟨9, ⋯⟩ wi| ≤ 1

theorem Proofs.TrainedCnnDescentConv1.x0_bound_r0_10 (wi : Fin 12) :

|T0 ⟨0, ⋯⟩ ⟨10, ⋯⟩ wi| ≤ 1

theorem Proofs.TrainedCnnDescentConv1.x0_bound_r0_11 (wi : Fin 12) :

|T0 ⟨0, ⋯⟩ ⟨11, ⋯⟩ wi| ≤ 1

theorem Proofs.TrainedCnnDescentConv1.x0_bound (o : Fin 1) (hi wi : Fin 12) :

|T0 o hi wi| ≤ 1

noncomputable def Proofs.TrainedCnnDescentConv1.c1V :

Tensor3 2 12 12

conv1 pre-activations at the image, exact.

Equations

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

Instances For

theorem Proofs.TrainedCnnDescentConv1.conv1_eq_r0_0 (wi : Fin 12) :

conv2d W1 b1 T0 ⟨0, ⋯⟩ ⟨0, ⋯⟩ wi = c1V ⟨0, ⋯⟩ ⟨0, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv1_eq_r0_1 (wi : Fin 12) :

conv2d W1 b1 T0 ⟨0, ⋯⟩ ⟨1, ⋯⟩ wi = c1V ⟨0, ⋯⟩ ⟨1, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv1_eq_r0_2 (wi : Fin 12) :

conv2d W1 b1 T0 ⟨0, ⋯⟩ ⟨2, ⋯⟩ wi = c1V ⟨0, ⋯⟩ ⟨2, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv1_eq_r0_3 (wi : Fin 12) :

conv2d W1 b1 T0 ⟨0, ⋯⟩ ⟨3, ⋯⟩ wi = c1V ⟨0, ⋯⟩ ⟨3, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv1_eq_r0_4 (wi : Fin 12) :

conv2d W1 b1 T0 ⟨0, ⋯⟩ ⟨4, ⋯⟩ wi = c1V ⟨0, ⋯⟩ ⟨4, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv1_eq_r0_5 (wi : Fin 12) :

conv2d W1 b1 T0 ⟨0, ⋯⟩ ⟨5, ⋯⟩ wi = c1V ⟨0, ⋯⟩ ⟨5, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv1_eq_r0_6 (wi : Fin 12) :

conv2d W1 b1 T0 ⟨0, ⋯⟩ ⟨6, ⋯⟩ wi = c1V ⟨0, ⋯⟩ ⟨6, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv1_eq_r0_7 (wi : Fin 12) :

conv2d W1 b1 T0 ⟨0, ⋯⟩ ⟨7, ⋯⟩ wi = c1V ⟨0, ⋯⟩ ⟨7, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv1_eq_r0_8 (wi : Fin 12) :

conv2d W1 b1 T0 ⟨0, ⋯⟩ ⟨8, ⋯⟩ wi = c1V ⟨0, ⋯⟩ ⟨8, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv1_eq_r0_9 (wi : Fin 12) :

conv2d W1 b1 T0 ⟨0, ⋯⟩ ⟨9, ⋯⟩ wi = c1V ⟨0, ⋯⟩ ⟨9, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv1_eq_r0_10 (wi : Fin 12) :

conv2d W1 b1 T0 ⟨0, ⋯⟩ ⟨10, ⋯⟩ wi = c1V ⟨0, ⋯⟩ ⟨10, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv1_eq_r0_11 (wi : Fin 12) :

conv2d W1 b1 T0 ⟨0, ⋯⟩ ⟨11, ⋯⟩ wi = c1V ⟨0, ⋯⟩ ⟨11, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv1_eq_r1_0 (wi : Fin 12) :

conv2d W1 b1 T0 ⟨1, ⋯⟩ ⟨0, ⋯⟩ wi = c1V ⟨1, ⋯⟩ ⟨0, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv1_eq_r1_1 (wi : Fin 12) :

conv2d W1 b1 T0 ⟨1, ⋯⟩ ⟨1, ⋯⟩ wi = c1V ⟨1, ⋯⟩ ⟨1, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv1_eq_r1_2 (wi : Fin 12) :

conv2d W1 b1 T0 ⟨1, ⋯⟩ ⟨2, ⋯⟩ wi = c1V ⟨1, ⋯⟩ ⟨2, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv1_eq_r1_3 (wi : Fin 12) :

conv2d W1 b1 T0 ⟨1, ⋯⟩ ⟨3, ⋯⟩ wi = c1V ⟨1, ⋯⟩ ⟨3, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv1_eq_r1_4 (wi : Fin 12) :

conv2d W1 b1 T0 ⟨1, ⋯⟩ ⟨4, ⋯⟩ wi = c1V ⟨1, ⋯⟩ ⟨4, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv1_eq_r1_5 (wi : Fin 12) :

conv2d W1 b1 T0 ⟨1, ⋯⟩ ⟨5, ⋯⟩ wi = c1V ⟨1, ⋯⟩ ⟨5, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv1_eq_r1_6 (wi : Fin 12) :

conv2d W1 b1 T0 ⟨1, ⋯⟩ ⟨6, ⋯⟩ wi = c1V ⟨1, ⋯⟩ ⟨6, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv1_eq_r1_7 (wi : Fin 12) :

conv2d W1 b1 T0 ⟨1, ⋯⟩ ⟨7, ⋯⟩ wi = c1V ⟨1, ⋯⟩ ⟨7, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv1_eq_r1_8 (wi : Fin 12) :

conv2d W1 b1 T0 ⟨1, ⋯⟩ ⟨8, ⋯⟩ wi = c1V ⟨1, ⋯⟩ ⟨8, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv1_eq_r1_9 (wi : Fin 12) :

conv2d W1 b1 T0 ⟨1, ⋯⟩ ⟨9, ⋯⟩ wi = c1V ⟨1, ⋯⟩ ⟨9, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv1_eq_r1_10 (wi : Fin 12) :

conv2d W1 b1 T0 ⟨1, ⋯⟩ ⟨10, ⋯⟩ wi = c1V ⟨1, ⋯⟩ ⟨10, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv1_eq_r1_11 (wi : Fin 12) :

conv2d W1 b1 T0 ⟨1, ⋯⟩ ⟨11, ⋯⟩ wi = c1V ⟨1, ⋯⟩ ⟨11, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv1_eq (o : Fin 2) (hi wi : Fin 12) :

conv2d W1 b1 T0 o hi wi = c1V o hi wi

theorem Proofs.TrainedCnnDescentConv1.conv1_fun :

conv2d W1 b1 T0 = c1V

theorem Proofs.TrainedCnnDescentConv1.c1_margin_r0_0 (wi : Fin 12) :

105015989295 / 576460752303423488 < |c1V ⟨0, ⋯⟩ ⟨0, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c1_margin_r0_1 (wi : Fin 12) :

105015989295 / 576460752303423488 < |c1V ⟨0, ⋯⟩ ⟨1, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c1_margin_r0_2 (wi : Fin 12) :

105015989295 / 576460752303423488 < |c1V ⟨0, ⋯⟩ ⟨2, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c1_margin_r0_3 (wi : Fin 12) :

105015989295 / 576460752303423488 < |c1V ⟨0, ⋯⟩ ⟨3, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c1_margin_r0_4 (wi : Fin 12) :

105015989295 / 576460752303423488 < |c1V ⟨0, ⋯⟩ ⟨4, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c1_margin_r0_5 (wi : Fin 12) :

105015989295 / 576460752303423488 < |c1V ⟨0, ⋯⟩ ⟨5, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c1_margin_r0_6 (wi : Fin 12) :

105015989295 / 576460752303423488 < |c1V ⟨0, ⋯⟩ ⟨6, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c1_margin_r0_7 (wi : Fin 12) :

105015989295 / 576460752303423488 < |c1V ⟨0, ⋯⟩ ⟨7, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c1_margin_r0_8 (wi : Fin 12) :

105015989295 / 576460752303423488 < |c1V ⟨0, ⋯⟩ ⟨8, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c1_margin_r0_9 (wi : Fin 12) :

105015989295 / 576460752303423488 < |c1V ⟨0, ⋯⟩ ⟨9, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c1_margin_r0_10 (wi : Fin 12) :

105015989295 / 576460752303423488 < |c1V ⟨0, ⋯⟩ ⟨10, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c1_margin_r0_11 (wi : Fin 12) :

105015989295 / 576460752303423488 < |c1V ⟨0, ⋯⟩ ⟨11, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c1_margin_r1_0 (wi : Fin 12) :

105015989295 / 576460752303423488 < |c1V ⟨1, ⋯⟩ ⟨0, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c1_margin_r1_1 (wi : Fin 12) :

105015989295 / 576460752303423488 < |c1V ⟨1, ⋯⟩ ⟨1, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c1_margin_r1_2 (wi : Fin 12) :

105015989295 / 576460752303423488 < |c1V ⟨1, ⋯⟩ ⟨2, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c1_margin_r1_3 (wi : Fin 12) :

105015989295 / 576460752303423488 < |c1V ⟨1, ⋯⟩ ⟨3, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c1_margin_r1_4 (wi : Fin 12) :

105015989295 / 576460752303423488 < |c1V ⟨1, ⋯⟩ ⟨4, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c1_margin_r1_5 (wi : Fin 12) :

105015989295 / 576460752303423488 < |c1V ⟨1, ⋯⟩ ⟨5, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c1_margin_r1_6 (wi : Fin 12) :

105015989295 / 576460752303423488 < |c1V ⟨1, ⋯⟩ ⟨6, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c1_margin_r1_7 (wi : Fin 12) :

105015989295 / 576460752303423488 < |c1V ⟨1, ⋯⟩ ⟨7, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c1_margin_r1_8 (wi : Fin 12) :

105015989295 / 576460752303423488 < |c1V ⟨1, ⋯⟩ ⟨8, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c1_margin_r1_9 (wi : Fin 12) :

105015989295 / 576460752303423488 < |c1V ⟨1, ⋯⟩ ⟨9, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c1_margin_r1_10 (wi : Fin 12) :

105015989295 / 576460752303423488 < |c1V ⟨1, ⋯⟩ ⟨10, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c1_margin_r1_11 (wi : Fin 12) :

105015989295 / 576460752303423488 < |c1V ⟨1, ⋯⟩ ⟨11, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c1_margin (o : Fin 2) (hi wi : Fin 12) :

105015989295 / 576460752303423488 < |c1V o hi wi|

noncomputable def Proofs.TrainedCnnDescentConv1.x1V :

Tensor3 2 12 12

relu(conv1) at the image (conv2's input), exact.

Equations

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

Instances For

theorem Proofs.TrainedCnnDescentConv1.x1_cell_r0_0 (wi : Fin 12) :

x1V ⟨0, ⋯⟩ ⟨0, ⋯⟩ wi = if c1V ⟨0, ⋯⟩ ⟨0, ⋯⟩ wi > 0 then c1V ⟨0, ⋯⟩ ⟨0, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.x1_cell_r0_1 (wi : Fin 12) :

x1V ⟨0, ⋯⟩ ⟨1, ⋯⟩ wi = if c1V ⟨0, ⋯⟩ ⟨1, ⋯⟩ wi > 0 then c1V ⟨0, ⋯⟩ ⟨1, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.x1_cell_r0_2 (wi : Fin 12) :

x1V ⟨0, ⋯⟩ ⟨2, ⋯⟩ wi = if c1V ⟨0, ⋯⟩ ⟨2, ⋯⟩ wi > 0 then c1V ⟨0, ⋯⟩ ⟨2, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.x1_cell_r0_3 (wi : Fin 12) :

x1V ⟨0, ⋯⟩ ⟨3, ⋯⟩ wi = if c1V ⟨0, ⋯⟩ ⟨3, ⋯⟩ wi > 0 then c1V ⟨0, ⋯⟩ ⟨3, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.x1_cell_r0_4 (wi : Fin 12) :

x1V ⟨0, ⋯⟩ ⟨4, ⋯⟩ wi = if c1V ⟨0, ⋯⟩ ⟨4, ⋯⟩ wi > 0 then c1V ⟨0, ⋯⟩ ⟨4, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.x1_cell_r0_5 (wi : Fin 12) :

x1V ⟨0, ⋯⟩ ⟨5, ⋯⟩ wi = if c1V ⟨0, ⋯⟩ ⟨5, ⋯⟩ wi > 0 then c1V ⟨0, ⋯⟩ ⟨5, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.x1_cell_r0_6 (wi : Fin 12) :

x1V ⟨0, ⋯⟩ ⟨6, ⋯⟩ wi = if c1V ⟨0, ⋯⟩ ⟨6, ⋯⟩ wi > 0 then c1V ⟨0, ⋯⟩ ⟨6, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.x1_cell_r0_7 (wi : Fin 12) :

x1V ⟨0, ⋯⟩ ⟨7, ⋯⟩ wi = if c1V ⟨0, ⋯⟩ ⟨7, ⋯⟩ wi > 0 then c1V ⟨0, ⋯⟩ ⟨7, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.x1_cell_r0_8 (wi : Fin 12) :

x1V ⟨0, ⋯⟩ ⟨8, ⋯⟩ wi = if c1V ⟨0, ⋯⟩ ⟨8, ⋯⟩ wi > 0 then c1V ⟨0, ⋯⟩ ⟨8, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.x1_cell_r0_9 (wi : Fin 12) :

x1V ⟨0, ⋯⟩ ⟨9, ⋯⟩ wi = if c1V ⟨0, ⋯⟩ ⟨9, ⋯⟩ wi > 0 then c1V ⟨0, ⋯⟩ ⟨9, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.x1_cell_r0_10 (wi : Fin 12) :

x1V ⟨0, ⋯⟩ ⟨10, ⋯⟩ wi = if c1V ⟨0, ⋯⟩ ⟨10, ⋯⟩ wi > 0 then c1V ⟨0, ⋯⟩ ⟨10, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.x1_cell_r0_11 (wi : Fin 12) :

x1V ⟨0, ⋯⟩ ⟨11, ⋯⟩ wi = if c1V ⟨0, ⋯⟩ ⟨11, ⋯⟩ wi > 0 then c1V ⟨0, ⋯⟩ ⟨11, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.x1_cell_r1_0 (wi : Fin 12) :

x1V ⟨1, ⋯⟩ ⟨0, ⋯⟩ wi = if c1V ⟨1, ⋯⟩ ⟨0, ⋯⟩ wi > 0 then c1V ⟨1, ⋯⟩ ⟨0, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.x1_cell_r1_1 (wi : Fin 12) :

x1V ⟨1, ⋯⟩ ⟨1, ⋯⟩ wi = if c1V ⟨1, ⋯⟩ ⟨1, ⋯⟩ wi > 0 then c1V ⟨1, ⋯⟩ ⟨1, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.x1_cell_r1_2 (wi : Fin 12) :

x1V ⟨1, ⋯⟩ ⟨2, ⋯⟩ wi = if c1V ⟨1, ⋯⟩ ⟨2, ⋯⟩ wi > 0 then c1V ⟨1, ⋯⟩ ⟨2, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.x1_cell_r1_3 (wi : Fin 12) :

x1V ⟨1, ⋯⟩ ⟨3, ⋯⟩ wi = if c1V ⟨1, ⋯⟩ ⟨3, ⋯⟩ wi > 0 then c1V ⟨1, ⋯⟩ ⟨3, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.x1_cell_r1_4 (wi : Fin 12) :

x1V ⟨1, ⋯⟩ ⟨4, ⋯⟩ wi = if c1V ⟨1, ⋯⟩ ⟨4, ⋯⟩ wi > 0 then c1V ⟨1, ⋯⟩ ⟨4, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.x1_cell_r1_5 (wi : Fin 12) :

x1V ⟨1, ⋯⟩ ⟨5, ⋯⟩ wi = if c1V ⟨1, ⋯⟩ ⟨5, ⋯⟩ wi > 0 then c1V ⟨1, ⋯⟩ ⟨5, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.x1_cell_r1_6 (wi : Fin 12) :

x1V ⟨1, ⋯⟩ ⟨6, ⋯⟩ wi = if c1V ⟨1, ⋯⟩ ⟨6, ⋯⟩ wi > 0 then c1V ⟨1, ⋯⟩ ⟨6, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.x1_cell_r1_7 (wi : Fin 12) :

x1V ⟨1, ⋯⟩ ⟨7, ⋯⟩ wi = if c1V ⟨1, ⋯⟩ ⟨7, ⋯⟩ wi > 0 then c1V ⟨1, ⋯⟩ ⟨7, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.x1_cell_r1_8 (wi : Fin 12) :

x1V ⟨1, ⋯⟩ ⟨8, ⋯⟩ wi = if c1V ⟨1, ⋯⟩ ⟨8, ⋯⟩ wi > 0 then c1V ⟨1, ⋯⟩ ⟨8, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.x1_cell_r1_9 (wi : Fin 12) :

x1V ⟨1, ⋯⟩ ⟨9, ⋯⟩ wi = if c1V ⟨1, ⋯⟩ ⟨9, ⋯⟩ wi > 0 then c1V ⟨1, ⋯⟩ ⟨9, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.x1_cell_r1_10 (wi : Fin 12) :

x1V ⟨1, ⋯⟩ ⟨10, ⋯⟩ wi = if c1V ⟨1, ⋯⟩ ⟨10, ⋯⟩ wi > 0 then c1V ⟨1, ⋯⟩ ⟨10, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.x1_cell_r1_11 (wi : Fin 12) :

x1V ⟨1, ⋯⟩ ⟨11, ⋯⟩ wi = if c1V ⟨1, ⋯⟩ ⟨11, ⋯⟩ wi > 0 then c1V ⟨1, ⋯⟩ ⟨11, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.x1_cell (o : Fin 2) (hi wi : Fin 12) :

x1V o hi wi = if c1V o hi wi > 0 then c1V o hi wi else 0

theorem Proofs.TrainedCnnDescentConv1.relu_c1 :

relu (2 * (2 * 6) * (2 * 6)) c1V.flatten = x1V.flatten

theorem Proofs.TrainedCnnDescentConv1.x1_fun :

Tensor3.unflatten (relu (2 * (2 * 6) * (2 * 6)) (conv2d W1 b1 T0).flatten) = x1V

conv2's input is the real image's conv1 activation.

noncomputable def Proofs.TrainedCnnDescentConv1.c2V :

Tensor3 2 12 12

conv2 pre-activations at the image, exact.

Equations

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

Instances For

theorem Proofs.TrainedCnnDescentConv1.conv2_eq_r0_0 (wi : Fin 12) :

conv2d W2 b2 x1V ⟨0, ⋯⟩ ⟨0, ⋯⟩ wi = c2V ⟨0, ⋯⟩ ⟨0, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv2_eq_r0_1 (wi : Fin 12) :

conv2d W2 b2 x1V ⟨0, ⋯⟩ ⟨1, ⋯⟩ wi = c2V ⟨0, ⋯⟩ ⟨1, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv2_eq_r0_2 (wi : Fin 12) :

conv2d W2 b2 x1V ⟨0, ⋯⟩ ⟨2, ⋯⟩ wi = c2V ⟨0, ⋯⟩ ⟨2, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv2_eq_r0_3 (wi : Fin 12) :

conv2d W2 b2 x1V ⟨0, ⋯⟩ ⟨3, ⋯⟩ wi = c2V ⟨0, ⋯⟩ ⟨3, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv2_eq_r0_4 (wi : Fin 12) :

conv2d W2 b2 x1V ⟨0, ⋯⟩ ⟨4, ⋯⟩ wi = c2V ⟨0, ⋯⟩ ⟨4, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv2_eq_r0_5 (wi : Fin 12) :

conv2d W2 b2 x1V ⟨0, ⋯⟩ ⟨5, ⋯⟩ wi = c2V ⟨0, ⋯⟩ ⟨5, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv2_eq_r0_6 (wi : Fin 12) :

conv2d W2 b2 x1V ⟨0, ⋯⟩ ⟨6, ⋯⟩ wi = c2V ⟨0, ⋯⟩ ⟨6, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv2_eq_r0_7 (wi : Fin 12) :

conv2d W2 b2 x1V ⟨0, ⋯⟩ ⟨7, ⋯⟩ wi = c2V ⟨0, ⋯⟩ ⟨7, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv2_eq_r0_8 (wi : Fin 12) :

conv2d W2 b2 x1V ⟨0, ⋯⟩ ⟨8, ⋯⟩ wi = c2V ⟨0, ⋯⟩ ⟨8, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv2_eq_r0_9 (wi : Fin 12) :

conv2d W2 b2 x1V ⟨0, ⋯⟩ ⟨9, ⋯⟩ wi = c2V ⟨0, ⋯⟩ ⟨9, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv2_eq_r0_10 (wi : Fin 12) :

conv2d W2 b2 x1V ⟨0, ⋯⟩ ⟨10, ⋯⟩ wi = c2V ⟨0, ⋯⟩ ⟨10, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv2_eq_r0_11 (wi : Fin 12) :

conv2d W2 b2 x1V ⟨0, ⋯⟩ ⟨11, ⋯⟩ wi = c2V ⟨0, ⋯⟩ ⟨11, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv2_eq_r1_0 (wi : Fin 12) :

conv2d W2 b2 x1V ⟨1, ⋯⟩ ⟨0, ⋯⟩ wi = c2V ⟨1, ⋯⟩ ⟨0, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv2_eq_r1_1 (wi : Fin 12) :

conv2d W2 b2 x1V ⟨1, ⋯⟩ ⟨1, ⋯⟩ wi = c2V ⟨1, ⋯⟩ ⟨1, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv2_eq_r1_2 (wi : Fin 12) :

conv2d W2 b2 x1V ⟨1, ⋯⟩ ⟨2, ⋯⟩ wi = c2V ⟨1, ⋯⟩ ⟨2, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv2_eq_r1_3 (wi : Fin 12) :

conv2d W2 b2 x1V ⟨1, ⋯⟩ ⟨3, ⋯⟩ wi = c2V ⟨1, ⋯⟩ ⟨3, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv2_eq_r1_4 (wi : Fin 12) :

conv2d W2 b2 x1V ⟨1, ⋯⟩ ⟨4, ⋯⟩ wi = c2V ⟨1, ⋯⟩ ⟨4, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv2_eq_r1_5 (wi : Fin 12) :

conv2d W2 b2 x1V ⟨1, ⋯⟩ ⟨5, ⋯⟩ wi = c2V ⟨1, ⋯⟩ ⟨5, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv2_eq_r1_6 (wi : Fin 12) :

conv2d W2 b2 x1V ⟨1, ⋯⟩ ⟨6, ⋯⟩ wi = c2V ⟨1, ⋯⟩ ⟨6, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv2_eq_r1_7 (wi : Fin 12) :

conv2d W2 b2 x1V ⟨1, ⋯⟩ ⟨7, ⋯⟩ wi = c2V ⟨1, ⋯⟩ ⟨7, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv2_eq_r1_8 (wi : Fin 12) :

conv2d W2 b2 x1V ⟨1, ⋯⟩ ⟨8, ⋯⟩ wi = c2V ⟨1, ⋯⟩ ⟨8, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv2_eq_r1_9 (wi : Fin 12) :

conv2d W2 b2 x1V ⟨1, ⋯⟩ ⟨9, ⋯⟩ wi = c2V ⟨1, ⋯⟩ ⟨9, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv2_eq_r1_10 (wi : Fin 12) :

conv2d W2 b2 x1V ⟨1, ⋯⟩ ⟨10, ⋯⟩ wi = c2V ⟨1, ⋯⟩ ⟨10, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv2_eq_r1_11 (wi : Fin 12) :

conv2d W2 b2 x1V ⟨1, ⋯⟩ ⟨11, ⋯⟩ wi = c2V ⟨1, ⋯⟩ ⟨11, ⋯⟩ wi

theorem Proofs.TrainedCnnDescentConv1.conv2_eq (o : Fin 2) (hi wi : Fin 12) :

conv2d W2 b2 x1V o hi wi = c2V o hi wi

theorem Proofs.TrainedCnnDescentConv1.conv2_fun :

conv2d W2 b2 x1V = c2V

theorem Proofs.TrainedCnnDescentConv1.c2_margin_r0_0 (wi : Fin 12) :

138936153837285 / 36893488147419103232 < |c2V ⟨0, ⋯⟩ ⟨0, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c2_margin_r0_1 (wi : Fin 12) :

138936153837285 / 36893488147419103232 < |c2V ⟨0, ⋯⟩ ⟨1, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c2_margin_r0_2 (wi : Fin 12) :

138936153837285 / 36893488147419103232 < |c2V ⟨0, ⋯⟩ ⟨2, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c2_margin_r0_3 (wi : Fin 12) :

138936153837285 / 36893488147419103232 < |c2V ⟨0, ⋯⟩ ⟨3, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c2_margin_r0_4 (wi : Fin 12) :

138936153837285 / 36893488147419103232 < |c2V ⟨0, ⋯⟩ ⟨4, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c2_margin_r0_5 (wi : Fin 12) :

138936153837285 / 36893488147419103232 < |c2V ⟨0, ⋯⟩ ⟨5, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c2_margin_r0_6 (wi : Fin 12) :

138936153837285 / 36893488147419103232 < |c2V ⟨0, ⋯⟩ ⟨6, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c2_margin_r0_7 (wi : Fin 12) :

138936153837285 / 36893488147419103232 < |c2V ⟨0, ⋯⟩ ⟨7, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c2_margin_r0_8 (wi : Fin 12) :

138936153837285 / 36893488147419103232 < |c2V ⟨0, ⋯⟩ ⟨8, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c2_margin_r0_9 (wi : Fin 12) :

138936153837285 / 36893488147419103232 < |c2V ⟨0, ⋯⟩ ⟨9, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c2_margin_r0_10 (wi : Fin 12) :

138936153837285 / 36893488147419103232 < |c2V ⟨0, ⋯⟩ ⟨10, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c2_margin_r0_11 (wi : Fin 12) :

138936153837285 / 36893488147419103232 < |c2V ⟨0, ⋯⟩ ⟨11, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c2_margin_r1_0 (wi : Fin 12) :

138936153837285 / 36893488147419103232 < |c2V ⟨1, ⋯⟩ ⟨0, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c2_margin_r1_1 (wi : Fin 12) :

138936153837285 / 36893488147419103232 < |c2V ⟨1, ⋯⟩ ⟨1, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c2_margin_r1_2 (wi : Fin 12) :

138936153837285 / 36893488147419103232 < |c2V ⟨1, ⋯⟩ ⟨2, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c2_margin_r1_3 (wi : Fin 12) :

138936153837285 / 36893488147419103232 < |c2V ⟨1, ⋯⟩ ⟨3, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c2_margin_r1_4 (wi : Fin 12) :

138936153837285 / 36893488147419103232 < |c2V ⟨1, ⋯⟩ ⟨4, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c2_margin_r1_5 (wi : Fin 12) :

138936153837285 / 36893488147419103232 < |c2V ⟨1, ⋯⟩ ⟨5, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c2_margin_r1_6 (wi : Fin 12) :

138936153837285 / 36893488147419103232 < |c2V ⟨1, ⋯⟩ ⟨6, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c2_margin_r1_7 (wi : Fin 12) :

138936153837285 / 36893488147419103232 < |c2V ⟨1, ⋯⟩ ⟨7, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c2_margin_r1_8 (wi : Fin 12) :

138936153837285 / 36893488147419103232 < |c2V ⟨1, ⋯⟩ ⟨8, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c2_margin_r1_9 (wi : Fin 12) :

138936153837285 / 36893488147419103232 < |c2V ⟨1, ⋯⟩ ⟨9, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c2_margin_r1_10 (wi : Fin 12) :

138936153837285 / 36893488147419103232 < |c2V ⟨1, ⋯⟩ ⟨10, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c2_margin_r1_11 (wi : Fin 12) :

138936153837285 / 36893488147419103232 < |c2V ⟨1, ⋯⟩ ⟨11, ⋯⟩ wi|

theorem Proofs.TrainedCnnDescentConv1.c2_margin (o : Fin 2) (hi wi : Fin 12) :

138936153837285 / 36893488147419103232 < |c2V o hi wi|

noncomputable def Proofs.TrainedCnnDescentConv1.r2V :

Tensor3 2 12 12

relu(conv2) at the image (the max-pool input), exact.

Equations

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

Instances For

theorem Proofs.TrainedCnnDescentConv1.r2_cell_r0_0 (wi : Fin 12) :

r2V ⟨0, ⋯⟩ ⟨0, ⋯⟩ wi = if c2V ⟨0, ⋯⟩ ⟨0, ⋯⟩ wi > 0 then c2V ⟨0, ⋯⟩ ⟨0, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.r2_cell_r0_1 (wi : Fin 12) :

r2V ⟨0, ⋯⟩ ⟨1, ⋯⟩ wi = if c2V ⟨0, ⋯⟩ ⟨1, ⋯⟩ wi > 0 then c2V ⟨0, ⋯⟩ ⟨1, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.r2_cell_r0_2 (wi : Fin 12) :

r2V ⟨0, ⋯⟩ ⟨2, ⋯⟩ wi = if c2V ⟨0, ⋯⟩ ⟨2, ⋯⟩ wi > 0 then c2V ⟨0, ⋯⟩ ⟨2, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.r2_cell_r0_3 (wi : Fin 12) :

r2V ⟨0, ⋯⟩ ⟨3, ⋯⟩ wi = if c2V ⟨0, ⋯⟩ ⟨3, ⋯⟩ wi > 0 then c2V ⟨0, ⋯⟩ ⟨3, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.r2_cell_r0_4 (wi : Fin 12) :

r2V ⟨0, ⋯⟩ ⟨4, ⋯⟩ wi = if c2V ⟨0, ⋯⟩ ⟨4, ⋯⟩ wi > 0 then c2V ⟨0, ⋯⟩ ⟨4, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.r2_cell_r0_5 (wi : Fin 12) :

r2V ⟨0, ⋯⟩ ⟨5, ⋯⟩ wi = if c2V ⟨0, ⋯⟩ ⟨5, ⋯⟩ wi > 0 then c2V ⟨0, ⋯⟩ ⟨5, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.r2_cell_r0_6 (wi : Fin 12) :

r2V ⟨0, ⋯⟩ ⟨6, ⋯⟩ wi = if c2V ⟨0, ⋯⟩ ⟨6, ⋯⟩ wi > 0 then c2V ⟨0, ⋯⟩ ⟨6, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.r2_cell_r0_7 (wi : Fin 12) :

r2V ⟨0, ⋯⟩ ⟨7, ⋯⟩ wi = if c2V ⟨0, ⋯⟩ ⟨7, ⋯⟩ wi > 0 then c2V ⟨0, ⋯⟩ ⟨7, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.r2_cell_r0_8 (wi : Fin 12) :

r2V ⟨0, ⋯⟩ ⟨8, ⋯⟩ wi = if c2V ⟨0, ⋯⟩ ⟨8, ⋯⟩ wi > 0 then c2V ⟨0, ⋯⟩ ⟨8, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.r2_cell_r0_9 (wi : Fin 12) :

r2V ⟨0, ⋯⟩ ⟨9, ⋯⟩ wi = if c2V ⟨0, ⋯⟩ ⟨9, ⋯⟩ wi > 0 then c2V ⟨0, ⋯⟩ ⟨9, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.r2_cell_r0_10 (wi : Fin 12) :

r2V ⟨0, ⋯⟩ ⟨10, ⋯⟩ wi = if c2V ⟨0, ⋯⟩ ⟨10, ⋯⟩ wi > 0 then c2V ⟨0, ⋯⟩ ⟨10, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.r2_cell_r0_11 (wi : Fin 12) :

r2V ⟨0, ⋯⟩ ⟨11, ⋯⟩ wi = if c2V ⟨0, ⋯⟩ ⟨11, ⋯⟩ wi > 0 then c2V ⟨0, ⋯⟩ ⟨11, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.r2_cell_r1_0 (wi : Fin 12) :

r2V ⟨1, ⋯⟩ ⟨0, ⋯⟩ wi = if c2V ⟨1, ⋯⟩ ⟨0, ⋯⟩ wi > 0 then c2V ⟨1, ⋯⟩ ⟨0, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.r2_cell_r1_1 (wi : Fin 12) :

r2V ⟨1, ⋯⟩ ⟨1, ⋯⟩ wi = if c2V ⟨1, ⋯⟩ ⟨1, ⋯⟩ wi > 0 then c2V ⟨1, ⋯⟩ ⟨1, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.r2_cell_r1_2 (wi : Fin 12) :

r2V ⟨1, ⋯⟩ ⟨2, ⋯⟩ wi = if c2V ⟨1, ⋯⟩ ⟨2, ⋯⟩ wi > 0 then c2V ⟨1, ⋯⟩ ⟨2, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.r2_cell_r1_3 (wi : Fin 12) :

r2V ⟨1, ⋯⟩ ⟨3, ⋯⟩ wi = if c2V ⟨1, ⋯⟩ ⟨3, ⋯⟩ wi > 0 then c2V ⟨1, ⋯⟩ ⟨3, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.r2_cell_r1_4 (wi : Fin 12) :

r2V ⟨1, ⋯⟩ ⟨4, ⋯⟩ wi = if c2V ⟨1, ⋯⟩ ⟨4, ⋯⟩ wi > 0 then c2V ⟨1, ⋯⟩ ⟨4, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.r2_cell_r1_5 (wi : Fin 12) :

r2V ⟨1, ⋯⟩ ⟨5, ⋯⟩ wi = if c2V ⟨1, ⋯⟩ ⟨5, ⋯⟩ wi > 0 then c2V ⟨1, ⋯⟩ ⟨5, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.r2_cell_r1_6 (wi : Fin 12) :

r2V ⟨1, ⋯⟩ ⟨6, ⋯⟩ wi = if c2V ⟨1, ⋯⟩ ⟨6, ⋯⟩ wi > 0 then c2V ⟨1, ⋯⟩ ⟨6, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.r2_cell_r1_7 (wi : Fin 12) :

r2V ⟨1, ⋯⟩ ⟨7, ⋯⟩ wi = if c2V ⟨1, ⋯⟩ ⟨7, ⋯⟩ wi > 0 then c2V ⟨1, ⋯⟩ ⟨7, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.r2_cell_r1_8 (wi : Fin 12) :

r2V ⟨1, ⋯⟩ ⟨8, ⋯⟩ wi = if c2V ⟨1, ⋯⟩ ⟨8, ⋯⟩ wi > 0 then c2V ⟨1, ⋯⟩ ⟨8, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.r2_cell_r1_9 (wi : Fin 12) :

r2V ⟨1, ⋯⟩ ⟨9, ⋯⟩ wi = if c2V ⟨1, ⋯⟩ ⟨9, ⋯⟩ wi > 0 then c2V ⟨1, ⋯⟩ ⟨9, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.r2_cell_r1_10 (wi : Fin 12) :

r2V ⟨1, ⋯⟩ ⟨10, ⋯⟩ wi = if c2V ⟨1, ⋯⟩ ⟨10, ⋯⟩ wi > 0 then c2V ⟨1, ⋯⟩ ⟨10, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.r2_cell_r1_11 (wi : Fin 12) :

r2V ⟨1, ⋯⟩ ⟨11, ⋯⟩ wi = if c2V ⟨1, ⋯⟩ ⟨11, ⋯⟩ wi > 0 then c2V ⟨1, ⋯⟩ ⟨11, ⋯⟩ wi else 0

theorem Proofs.TrainedCnnDescentConv1.r2_cell (o : Fin 2) (hi wi : Fin 12) :

r2V o hi wi = if c2V o hi wi > 0 then c2V o hi wi else 0

theorem Proofs.TrainedCnnDescentConv1.relu_c2 :

relu (2 * (2 * 6) * (2 * 6)) c2V.flatten = r2V.flatten

noncomputable def Proofs.TrainedCnnDescentConv1.p2f :

Vec (2 * 6 * 6)

The pooled feature vector (flattened maxpool output), exact.

Equations

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

Instances For

theorem Proofs.TrainedCnnDescentConv1.pooled_eq :

maxPoolFlat 2 6 6 r2V.flatten = p2f

theorem Proofs.TrainedCnnDescentConv1.tw_6_1_7_1 :

ConvPatchEq2 3 3 T0 (⟨6, ⋯⟩, ⟨1, ⋯⟩) (⟨7, ⋯⟩, ⟨1, ⋯⟩)

theorem Proofs.TrainedCnnDescentConv1.tw_8_1_9_1 :

ConvPatchEq2 3 3 T0 (⟨8, ⋯⟩, ⟨1, ⋯⟩) (⟨9, ⋯⟩, ⟨1, ⋯⟩)

theorem Proofs.TrainedCnnDescentConv1.cert_0_0 (wo : Fin 6) :

(∀ (cd : Fin 2 × Fin 2), c2V ⟨0, ⋯⟩ (winRowInv ⟨0, ⋯⟩ cd.1) (winColInv wo cd.2) ≤ 0) ∨ ∃ (m : Fin 2 × Fin 2), ∀ (cd : Fin 2 × Fin 2), (winRowInv ⟨0, ⋯⟩ m.1, winColInv wo m.2) = (winRowInv ⟨0, ⋯⟩ cd.1, winColInv wo cd.2) ∨ ConvPatchEq2 3 3 T0 (winRowInv ⟨0, ⋯⟩ m.1, winColInv wo m.2) (winRowInv ⟨0, ⋯⟩ cd.1, winColInv wo cd.2) ∨ c2V ⟨0, ⋯⟩ (winRowInv ⟨0, ⋯⟩ cd.1) (winColInv wo cd.2) + 2 * (138936153837285 / 36893488147419103232) < c2V ⟨0, ⋯⟩ (winRowInv ⟨0, ⋯⟩ m.1) (winColInv wo m.2)

theorem Proofs.TrainedCnnDescentConv1.cert_0_1 (wo : Fin 6) :

(∀ (cd : Fin 2 × Fin 2), c2V ⟨0, ⋯⟩ (winRowInv ⟨1, ⋯⟩ cd.1) (winColInv wo cd.2) ≤ 0) ∨ ∃ (m : Fin 2 × Fin 2), ∀ (cd : Fin 2 × Fin 2), (winRowInv ⟨1, ⋯⟩ m.1, winColInv wo m.2) = (winRowInv ⟨1, ⋯⟩ cd.1, winColInv wo cd.2) ∨ ConvPatchEq2 3 3 T0 (winRowInv ⟨1, ⋯⟩ m.1, winColInv wo m.2) (winRowInv ⟨1, ⋯⟩ cd.1, winColInv wo cd.2) ∨ c2V ⟨0, ⋯⟩ (winRowInv ⟨1, ⋯⟩ cd.1) (winColInv wo cd.2) + 2 * (138936153837285 / 36893488147419103232) < c2V ⟨0, ⋯⟩ (winRowInv ⟨1, ⋯⟩ m.1) (winColInv wo m.2)

theorem Proofs.TrainedCnnDescentConv1.cert_0_2 (wo : Fin 6) :

(∀ (cd : Fin 2 × Fin 2), c2V ⟨0, ⋯⟩ (winRowInv ⟨2, ⋯⟩ cd.1) (winColInv wo cd.2) ≤ 0) ∨ ∃ (m : Fin 2 × Fin 2), ∀ (cd : Fin 2 × Fin 2), (winRowInv ⟨2, ⋯⟩ m.1, winColInv wo m.2) = (winRowInv ⟨2, ⋯⟩ cd.1, winColInv wo cd.2) ∨ ConvPatchEq2 3 3 T0 (winRowInv ⟨2, ⋯⟩ m.1, winColInv wo m.2) (winRowInv ⟨2, ⋯⟩ cd.1, winColInv wo cd.2) ∨ c2V ⟨0, ⋯⟩ (winRowInv ⟨2, ⋯⟩ cd.1) (winColInv wo cd.2) + 2 * (138936153837285 / 36893488147419103232) < c2V ⟨0, ⋯⟩ (winRowInv ⟨2, ⋯⟩ m.1) (winColInv wo m.2)

theorem Proofs.TrainedCnnDescentConv1.cert_0_3 (wo : Fin 6) :

(∀ (cd : Fin 2 × Fin 2), c2V ⟨0, ⋯⟩ (winRowInv ⟨3, ⋯⟩ cd.1) (winColInv wo cd.2) ≤ 0) ∨ ∃ (m : Fin 2 × Fin 2), ∀ (cd : Fin 2 × Fin 2), (winRowInv ⟨3, ⋯⟩ m.1, winColInv wo m.2) = (winRowInv ⟨3, ⋯⟩ cd.1, winColInv wo cd.2) ∨ ConvPatchEq2 3 3 T0 (winRowInv ⟨3, ⋯⟩ m.1, winColInv wo m.2) (winRowInv ⟨3, ⋯⟩ cd.1, winColInv wo cd.2) ∨ c2V ⟨0, ⋯⟩ (winRowInv ⟨3, ⋯⟩ cd.1) (winColInv wo cd.2) + 2 * (138936153837285 / 36893488147419103232) < c2V ⟨0, ⋯⟩ (winRowInv ⟨3, ⋯⟩ m.1) (winColInv wo m.2)

theorem Proofs.TrainedCnnDescentConv1.cert_0_4 (wo : Fin 6) :

(∀ (cd : Fin 2 × Fin 2), c2V ⟨0, ⋯⟩ (winRowInv ⟨4, ⋯⟩ cd.1) (winColInv wo cd.2) ≤ 0) ∨ ∃ (m : Fin 2 × Fin 2), ∀ (cd : Fin 2 × Fin 2), (winRowInv ⟨4, ⋯⟩ m.1, winColInv wo m.2) = (winRowInv ⟨4, ⋯⟩ cd.1, winColInv wo cd.2) ∨ ConvPatchEq2 3 3 T0 (winRowInv ⟨4, ⋯⟩ m.1, winColInv wo m.2) (winRowInv ⟨4, ⋯⟩ cd.1, winColInv wo cd.2) ∨ c2V ⟨0, ⋯⟩ (winRowInv ⟨4, ⋯⟩ cd.1) (winColInv wo cd.2) + 2 * (138936153837285 / 36893488147419103232) < c2V ⟨0, ⋯⟩ (winRowInv ⟨4, ⋯⟩ m.1) (winColInv wo m.2)

theorem Proofs.TrainedCnnDescentConv1.cert_0_5 (wo : Fin 6) :

(∀ (cd : Fin 2 × Fin 2), c2V ⟨0, ⋯⟩ (winRowInv ⟨5, ⋯⟩ cd.1) (winColInv wo cd.2) ≤ 0) ∨ ∃ (m : Fin 2 × Fin 2), ∀ (cd : Fin 2 × Fin 2), (winRowInv ⟨5, ⋯⟩ m.1, winColInv wo m.2) = (winRowInv ⟨5, ⋯⟩ cd.1, winColInv wo cd.2) ∨ ConvPatchEq2 3 3 T0 (winRowInv ⟨5, ⋯⟩ m.1, winColInv wo m.2) (winRowInv ⟨5, ⋯⟩ cd.1, winColInv wo cd.2) ∨ c2V ⟨0, ⋯⟩ (winRowInv ⟨5, ⋯⟩ cd.1) (winColInv wo cd.2) + 2 * (138936153837285 / 36893488147419103232) < c2V ⟨0, ⋯⟩ (winRowInv ⟨5, ⋯⟩ m.1) (winColInv wo m.2)

theorem Proofs.TrainedCnnDescentConv1.cert_1_0 (wo : Fin 6) :

(∀ (cd : Fin 2 × Fin 2), c2V ⟨1, ⋯⟩ (winRowInv ⟨0, ⋯⟩ cd.1) (winColInv wo cd.2) ≤ 0) ∨ ∃ (m : Fin 2 × Fin 2), ∀ (cd : Fin 2 × Fin 2), (winRowInv ⟨0, ⋯⟩ m.1, winColInv wo m.2) = (winRowInv ⟨0, ⋯⟩ cd.1, winColInv wo cd.2) ∨ ConvPatchEq2 3 3 T0 (winRowInv ⟨0, ⋯⟩ m.1, winColInv wo m.2) (winRowInv ⟨0, ⋯⟩ cd.1, winColInv wo cd.2) ∨ c2V ⟨1, ⋯⟩ (winRowInv ⟨0, ⋯⟩ cd.1) (winColInv wo cd.2) + 2 * (138936153837285 / 36893488147419103232) < c2V ⟨1, ⋯⟩ (winRowInv ⟨0, ⋯⟩ m.1) (winColInv wo m.2)

theorem Proofs.TrainedCnnDescentConv1.cert_1_1 (wo : Fin 6) :

(∀ (cd : Fin 2 × Fin 2), c2V ⟨1, ⋯⟩ (winRowInv ⟨1, ⋯⟩ cd.1) (winColInv wo cd.2) ≤ 0) ∨ ∃ (m : Fin 2 × Fin 2), ∀ (cd : Fin 2 × Fin 2), (winRowInv ⟨1, ⋯⟩ m.1, winColInv wo m.2) = (winRowInv ⟨1, ⋯⟩ cd.1, winColInv wo cd.2) ∨ ConvPatchEq2 3 3 T0 (winRowInv ⟨1, ⋯⟩ m.1, winColInv wo m.2) (winRowInv ⟨1, ⋯⟩ cd.1, winColInv wo cd.2) ∨ c2V ⟨1, ⋯⟩ (winRowInv ⟨1, ⋯⟩ cd.1) (winColInv wo cd.2) + 2 * (138936153837285 / 36893488147419103232) < c2V ⟨1, ⋯⟩ (winRowInv ⟨1, ⋯⟩ m.1) (winColInv wo m.2)

theorem Proofs.TrainedCnnDescentConv1.cert_1_2 (wo : Fin 6) :

(∀ (cd : Fin 2 × Fin 2), c2V ⟨1, ⋯⟩ (winRowInv ⟨2, ⋯⟩ cd.1) (winColInv wo cd.2) ≤ 0) ∨ ∃ (m : Fin 2 × Fin 2), ∀ (cd : Fin 2 × Fin 2), (winRowInv ⟨2, ⋯⟩ m.1, winColInv wo m.2) = (winRowInv ⟨2, ⋯⟩ cd.1, winColInv wo cd.2) ∨ ConvPatchEq2 3 3 T0 (winRowInv ⟨2, ⋯⟩ m.1, winColInv wo m.2) (winRowInv ⟨2, ⋯⟩ cd.1, winColInv wo cd.2) ∨ c2V ⟨1, ⋯⟩ (winRowInv ⟨2, ⋯⟩ cd.1) (winColInv wo cd.2) + 2 * (138936153837285 / 36893488147419103232) < c2V ⟨1, ⋯⟩ (winRowInv ⟨2, ⋯⟩ m.1) (winColInv wo m.2)

theorem Proofs.TrainedCnnDescentConv1.cert_1_3 (wo : Fin 6) :

(∀ (cd : Fin 2 × Fin 2), c2V ⟨1, ⋯⟩ (winRowInv ⟨3, ⋯⟩ cd.1) (winColInv wo cd.2) ≤ 0) ∨ ∃ (m : Fin 2 × Fin 2), ∀ (cd : Fin 2 × Fin 2), (winRowInv ⟨3, ⋯⟩ m.1, winColInv wo m.2) = (winRowInv ⟨3, ⋯⟩ cd.1, winColInv wo cd.2) ∨ ConvPatchEq2 3 3 T0 (winRowInv ⟨3, ⋯⟩ m.1, winColInv wo m.2) (winRowInv ⟨3, ⋯⟩ cd.1, winColInv wo cd.2) ∨ c2V ⟨1, ⋯⟩ (winRowInv ⟨3, ⋯⟩ cd.1) (winColInv wo cd.2) + 2 * (138936153837285 / 36893488147419103232) < c2V ⟨1, ⋯⟩ (winRowInv ⟨3, ⋯⟩ m.1) (winColInv wo m.2)

theorem Proofs.TrainedCnnDescentConv1.cert_1_4 (wo : Fin 6) :

(∀ (cd : Fin 2 × Fin 2), c2V ⟨1, ⋯⟩ (winRowInv ⟨4, ⋯⟩ cd.1) (winColInv wo cd.2) ≤ 0) ∨ ∃ (m : Fin 2 × Fin 2), ∀ (cd : Fin 2 × Fin 2), (winRowInv ⟨4, ⋯⟩ m.1, winColInv wo m.2) = (winRowInv ⟨4, ⋯⟩ cd.1, winColInv wo cd.2) ∨ ConvPatchEq2 3 3 T0 (winRowInv ⟨4, ⋯⟩ m.1, winColInv wo m.2) (winRowInv ⟨4, ⋯⟩ cd.1, winColInv wo cd.2) ∨ c2V ⟨1, ⋯⟩ (winRowInv ⟨4, ⋯⟩ cd.1) (winColInv wo cd.2) + 2 * (138936153837285 / 36893488147419103232) < c2V ⟨1, ⋯⟩ (winRowInv ⟨4, ⋯⟩ m.1) (winColInv wo m.2)

theorem Proofs.TrainedCnnDescentConv1.cert_1_5 (wo : Fin 6) :

(∀ (cd : Fin 2 × Fin 2), c2V ⟨1, ⋯⟩ (winRowInv ⟨5, ⋯⟩ cd.1) (winColInv wo cd.2) ≤ 0) ∨ ∃ (m : Fin 2 × Fin 2), ∀ (cd : Fin 2 × Fin 2), (winRowInv ⟨5, ⋯⟩ m.1, winColInv wo m.2) = (winRowInv ⟨5, ⋯⟩ cd.1, winColInv wo cd.2) ∨ ConvPatchEq2 3 3 T0 (winRowInv ⟨5, ⋯⟩ m.1, winColInv wo m.2) (winRowInv ⟨5, ⋯⟩ cd.1, winColInv wo cd.2) ∨ c2V ⟨1, ⋯⟩ (winRowInv ⟨5, ⋯⟩ cd.1) (winColInv wo cd.2) + 2 * (138936153837285 / 36893488147419103232) < c2V ⟨1, ⋯⟩ (winRowInv ⟨5, ⋯⟩ m.1) (winColInv wo m.2)

theorem Proofs.TrainedCnnDescentConv1.pool_margin :

MaxPool2MarginQUpTo (138936153837285 / 36893488147419103232) (ConvPatchEq2 3 3 T0) c2V

The pool margin up to two-layer twins holds at the trained weights, ties and all.

noncomputable def Proofs.TrainedCnnDescentConv1.d3V :

Fin 8 → ℝ

dense3 pre-activations at the image, exact.

Equations

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

Instances For

theorem Proofs.TrainedCnnDescentConv1.d3_eq (k : Fin 8) :

dense W3 b3 p2f k = d3V k

noncomputable def Proofs.TrainedCnnDescentConv1.r3V :

relu(dense3) at the image, exact.

Equations

Proofs.TrainedCnnDescentConv1.r3V = ![0, 0, 33160518331 / 68451041280, 0, 0, 625116588899 / 68451041280, 0, 0]

Instances For

theorem Proofs.TrainedCnnDescentConv1.r3_eq :

relu 8 (dense W3 b3 p2f) = r3V

noncomputable def Proofs.TrainedCnnDescentConv1.d4V :

Fin 8 → ℝ

dense4 pre-activations at the image, exact.

Equations

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

Instances For

theorem Proofs.TrainedCnnDescentConv1.d4_eq (k : Fin 8) :

dense W4 b4 r3V k = d4V k

theorem Proofs.TrainedCnnDescentConv1.head_feat :

maxPoolFlat 2 6 6 (relu (2 * (2 * 6) * (2 * 6)) (conv2d W2 b2 x1V).flatten) = p2f

theorem Proofs.TrainedCnnDescentConv1.hW2 (o cc : Fin 2) (kh kw : Fin 3) :

|W2 o cc kh kw| ≤ 147 / 128

theorem Proofs.TrainedCnnDescentConv1.hW3 (i : Fin (2 * 6 * 6)) (j : Fin 8) :

|W3 i j| ≤ 183 / 128

theorem Proofs.TrainedCnnDescentConv1.hW4 (i j : Fin 8) :

|W4 i j| ≤ 63 / 64

theorem Proofs.TrainedCnnDescentConv1.hW5 (i : Fin 8) (j : Fin 10) :

|W5 i j| ≤ 17 / 16

theorem Proofs.TrainedCnnDescentConv1.radius_eq :

1 * (1 / 2 ^ 48 * cnnConv1GradBound 1 2 6 6 8 8 10 3 3 1 (147 / 128) (183 / 128) (63 / 64) (17 / 16)) = 105015989295 / 576460752303423488

The relu₁ margin radius a·(lr·G) of the kernel instance, exact.

theorem Proofs.TrainedCnnDescentConv1.trained_cnn_conv1_sgd_descends_concrete :

cnnConv1KernelLoss b1 T0 W2 b2 W3 b3 W4 b4 W5 b5 lbl (W1.flatten - (1 / 2 ^ 48) • gradAt (cnnConv1KernelLoss b1 T0 W2 b2 W3 b3 W4 b4 W5 b5 lbl) W1.flatten) ≤ cnnConv1KernelLoss b1 T0 W2 b2 W3 b3 W4 b4 W5 b5 lbl W1.flatten - (1 / 2 ^ 48 * ∑ idx : Fin (2 * 1 * 3 * 3), gradAt (cnnConv1KernelLoss b1 T0 W2 b2 W3 b3 W4 b4 W5 b5 lbl) W1.flatten idx ^ 2) / 2

One exact-gradient SGD step on the conv1 kernel of a trained MNIST CNN, at a real test image with two-layer-twin pool ties, decreases the cross-entropy loss by at least lr·‖∇L‖₂²/2, at lr = 2⁻48. Every hypothesis of cnn_conv1_exact_sgd_descends is discharged above.

theorem Proofs.TrainedCnnDescentConv1.radius_bias_eq :

1 / 2 ^ 45 * cnnConv1BiasGradBound 2 6 6 8 8 10 3 3 (147 / 128) (183 / 128) (63 / 64) (17 / 16) = 11668443255 / 72057594037927936

The bias instance's radius lr·G_b, exact; it sits inside the kernel instance's a·lr·G.

theorem Proofs.TrainedCnnDescentConv1.trained_cnn_conv1_bias_sgd_descends_concrete :

cnnConv1BiasLoss W1 T0 W2 b2 W3 b3 W4 b4 W5 b5 lbl (b1 - (1 / 2 ^ 45) • gradAt (cnnConv1BiasLoss W1 T0 W2 b2 W3 b3 W4 b4 W5 b5 lbl) b1) ≤ cnnConv1BiasLoss W1 T0 W2 b2 W3 b3 W4 b4 W5 b5 lbl b1 - (1 / 2 ^ 45 * ∑ o : Fin 2, gradAt (cnnConv1BiasLoss W1 T0 W2 b2 W3 b3 W4 b4 W5 b5 lbl) b1 o ^ 2) / 2

One exact-gradient SGD step on the conv1 BIAS of the same trained MNIST CNN, at the same test image, decreases the cross-entropy loss by at least lr·‖∇L‖₂²/2, at lr = 2⁻45. Every hypothesis of cnn_conv1_bias_exact_sgd_descends is discharged above; the relu₁, relu₂ and pool margins are the kernel instance's (c1_margin, c2_margin, pool_margin) at a smaller radius.