Documentation

LeanMlir.Proofs.Training.Trained.CnnDescent

Descent at TRAINED weights — the CNN conv2 rungs, through tied pool windows #

REDUCED CERTIFICATE MODEL — this file's net is a 12×12-input, 2-channel MNIST CNN with an 8-wide dense head, NOT the canonical 28×28, 32-channel cnnVerified; chosen so every table is exact rational arithmetic in the kernel. The canonical net's pool condition is measured on all 10000 test images by scripts/probes/mnist_pool_twin_probe.py.

cnn_conv2_exact_sgd_descends — one exact-gradient SGD step on the conv2 kernel 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_conv2_sgd_descends_concrete, at learning rate 2⁻42. The conv2-bias rung cnn_conv2_bias_exact_sgd_descends on the same net and image is trained_cnn_conv2_bias_sgd_descends_concrete, at 2⁻36: its radius sits inside the kernel rung's, so the relu₂ and pool margins carry over by monotonicity. The conv1 rungs need a net with a conv1 bias (Trained.CnnDescentConv1).

What the instance shows is the pool hypothesis. The image's blank corners make conv1's output zero there (conv1 is bias-free, so a zero patch gives the padding's value), the cells of a corner window then read identical all-zero patches, and their conv2 outputs are EQUAL — the conv2 bias, positive in one channel. 5 live windows tie that way and 7 are dead. The old MaxPool2MarginQ fails at every such window for every margin; MaxPool2MarginQUpTo takes the twins ConvPatchEq 3 3 x1V (ConvPatchEq.of_zero per tied cell, zp_*), and every other cell clears the margin (cert_*, through windowMarginUpTo_of_cert). No pool-tie regularizer was used in training; the ties are the data's.

Net: 24×24-center-cropped MNIST, 2×2 block sums to 12×12 (exact pixel sums /1020), conv 1→2 3×3 SAME without bias → relu → conv 2→2 3×3 SAME → relu → maxpool 2×2 → dense 72→8 → relu → dense 8→8 → relu → dense 8→10. The rungs move the conv2 kernel or bias; x1V = relu(conv1 image) is their frozen input (x1_eq). The generator prints the net's test accuracy.

The step is the exact gradient, so the conclusion bounds the true loss, but the decrease lr·‖∇L‖₂²/2 is not shown positive: that needs a lower bound on the gradient, which the softmax makes transcendental (Trained.LinearDescent gets one from a misclassified example). Generated by scripts/certs/trained_cnn_descent.py; weights and input are DATA.

noncomputable def Proofs.TrainedCnnDescent.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.TrainedCnnDescent.W1 :

Kernel4 2 1 3 3

conv1 kernel (1→2, 3×3), entries k/128; conv1 has no bias.

Equations

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

Instances For

noncomputable def Proofs.TrainedCnnDescent.b1 :

Equations

Proofs.TrainedCnnDescent.b1 = ![0, 0]

Instances For

noncomputable def Proofs.TrainedCnnDescent.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.TrainedCnnDescent.b2 :

Equations

Proofs.TrainedCnnDescent.b2 = ![-9 / 16384, 63 / 2048]

Instances For

noncomputable def Proofs.TrainedCnnDescent.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.TrainedCnnDescent.b3 :

Equations

Proofs.TrainedCnnDescent.b3 = ![599 / 4096, -3643 / 16384, 3881 / 16384, 2351 / 8192, 401 / 4096, 5053 / 16384, 1455 / 16384, 819 / 8192]

Instances For

noncomputable def Proofs.TrainedCnnDescent.W4 :

Mat 8 8

Equations

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

Instances For

noncomputable def Proofs.TrainedCnnDescent.b4 :

Equations

Proofs.TrainedCnnDescent.b4 = ![1289 / 4096, 1707 / 16384, -6681 / 8192, 2755 / 16384, 1579 / 16384, 5441 / 16384, 1429 / 8192, 9217 / 16384]

Instances For

noncomputable def Proofs.TrainedCnnDescent.W5 :

Mat 8 10

Equations

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

Instances For

noncomputable def Proofs.TrainedCnnDescent.b5 :

Vec 10

Equations

Proofs.TrainedCnnDescent.b5 = ![-8093 / 16384, 10649 / 16384, -1357 / 4096, -1141 / 16384, -47 / 512, 2237 / 4096, 119 / 2048, 519 / 2048, -15603 / 16384, 7069 / 16384]

Instances For

def Proofs.TrainedCnnDescent.lbl :

Fin 10

The label of test image #0.

Equations

Proofs.TrainedCnnDescent.lbl = 7

Instances For

noncomputable def Proofs.TrainedCnnDescent.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.TrainedCnnDescent.conv1_eq_r0_0 (wi : Fin 12) :

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

noncomputable def Proofs.TrainedCnnDescent.x1V :

Tensor3 2 12 12

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

Equations

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

Instances For

theorem Proofs.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.x1_eq :

x1V = fun (o : Fin 2) (hi wi : Fin 12) => if conv2d W1 b1 T0 o hi wi > 0 then conv2d W1 b1 T0 o hi wi else 0

The rung's input is the real image's conv1 activation.

theorem Proofs.TrainedCnnDescent.x1_bound_r0_0 (wi : Fin 12) :

|x1V ⟨0, ⋯⟩ ⟨0, ⋯⟩ wi| ≤ 5 / 2

theorem Proofs.TrainedCnnDescent.x1_bound_r0_1 (wi : Fin 12) :

|x1V ⟨0, ⋯⟩ ⟨1, ⋯⟩ wi| ≤ 5 / 2

theorem Proofs.TrainedCnnDescent.x1_bound_r0_2 (wi : Fin 12) :

|x1V ⟨0, ⋯⟩ ⟨2, ⋯⟩ wi| ≤ 5 / 2

theorem Proofs.TrainedCnnDescent.x1_bound_r0_3 (wi : Fin 12) :

|x1V ⟨0, ⋯⟩ ⟨3, ⋯⟩ wi| ≤ 5 / 2

theorem Proofs.TrainedCnnDescent.x1_bound_r0_4 (wi : Fin 12) :

|x1V ⟨0, ⋯⟩ ⟨4, ⋯⟩ wi| ≤ 5 / 2

theorem Proofs.TrainedCnnDescent.x1_bound_r0_5 (wi : Fin 12) :

|x1V ⟨0, ⋯⟩ ⟨5, ⋯⟩ wi| ≤ 5 / 2

theorem Proofs.TrainedCnnDescent.x1_bound_r0_6 (wi : Fin 12) :

|x1V ⟨0, ⋯⟩ ⟨6, ⋯⟩ wi| ≤ 5 / 2

theorem Proofs.TrainedCnnDescent.x1_bound_r0_7 (wi : Fin 12) :

|x1V ⟨0, ⋯⟩ ⟨7, ⋯⟩ wi| ≤ 5 / 2

theorem Proofs.TrainedCnnDescent.x1_bound_r0_8 (wi : Fin 12) :

|x1V ⟨0, ⋯⟩ ⟨8, ⋯⟩ wi| ≤ 5 / 2

theorem Proofs.TrainedCnnDescent.x1_bound_r0_9 (wi : Fin 12) :

|x1V ⟨0, ⋯⟩ ⟨9, ⋯⟩ wi| ≤ 5 / 2

theorem Proofs.TrainedCnnDescent.x1_bound_r0_10 (wi : Fin 12) :

|x1V ⟨0, ⋯⟩ ⟨10, ⋯⟩ wi| ≤ 5 / 2

theorem Proofs.TrainedCnnDescent.x1_bound_r0_11 (wi : Fin 12) :

|x1V ⟨0, ⋯⟩ ⟨11, ⋯⟩ wi| ≤ 5 / 2

theorem Proofs.TrainedCnnDescent.x1_bound_r1_0 (wi : Fin 12) :

|x1V ⟨1, ⋯⟩ ⟨0, ⋯⟩ wi| ≤ 5 / 2

theorem Proofs.TrainedCnnDescent.x1_bound_r1_1 (wi : Fin 12) :

|x1V ⟨1, ⋯⟩ ⟨1, ⋯⟩ wi| ≤ 5 / 2

theorem Proofs.TrainedCnnDescent.x1_bound_r1_2 (wi : Fin 12) :

|x1V ⟨1, ⋯⟩ ⟨2, ⋯⟩ wi| ≤ 5 / 2

theorem Proofs.TrainedCnnDescent.x1_bound_r1_3 (wi : Fin 12) :

|x1V ⟨1, ⋯⟩ ⟨3, ⋯⟩ wi| ≤ 5 / 2

theorem Proofs.TrainedCnnDescent.x1_bound_r1_4 (wi : Fin 12) :

|x1V ⟨1, ⋯⟩ ⟨4, ⋯⟩ wi| ≤ 5 / 2

theorem Proofs.TrainedCnnDescent.x1_bound_r1_5 (wi : Fin 12) :

|x1V ⟨1, ⋯⟩ ⟨5, ⋯⟩ wi| ≤ 5 / 2

theorem Proofs.TrainedCnnDescent.x1_bound_r1_6 (wi : Fin 12) :

|x1V ⟨1, ⋯⟩ ⟨6, ⋯⟩ wi| ≤ 5 / 2

theorem Proofs.TrainedCnnDescent.x1_bound_r1_7 (wi : Fin 12) :

|x1V ⟨1, ⋯⟩ ⟨7, ⋯⟩ wi| ≤ 5 / 2

theorem Proofs.TrainedCnnDescent.x1_bound_r1_8 (wi : Fin 12) :

|x1V ⟨1, ⋯⟩ ⟨8, ⋯⟩ wi| ≤ 5 / 2

theorem Proofs.TrainedCnnDescent.x1_bound_r1_9 (wi : Fin 12) :

|x1V ⟨1, ⋯⟩ ⟨9, ⋯⟩ wi| ≤ 5 / 2

theorem Proofs.TrainedCnnDescent.x1_bound_r1_10 (wi : Fin 12) :

|x1V ⟨1, ⋯⟩ ⟨10, ⋯⟩ wi| ≤ 5 / 2

theorem Proofs.TrainedCnnDescent.x1_bound_r1_11 (wi : Fin 12) :

|x1V ⟨1, ⋯⟩ ⟨11, ⋯⟩ wi| ≤ 5 / 2

theorem Proofs.TrainedCnnDescent.x1_bound (o : Fin 2) (hi wi : Fin 12) :

|x1V o hi wi| ≤ 5 / 2

noncomputable def Proofs.TrainedCnnDescent.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.TrainedCnnDescent.conv2_eq_r0_0 (wi : Fin 12) :

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Proofs.TrainedCnnDescent.conv2_fun :

conv2d W2 b2 x1V = c2V

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

26090859375 / 4503599627370496 < |c2V ⟨0, ⋯⟩ ⟨0, ⋯⟩ wi|

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

26090859375 / 4503599627370496 < |c2V ⟨0, ⋯⟩ ⟨1, ⋯⟩ wi|

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

26090859375 / 4503599627370496 < |c2V ⟨0, ⋯⟩ ⟨2, ⋯⟩ wi|

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

26090859375 / 4503599627370496 < |c2V ⟨0, ⋯⟩ ⟨3, ⋯⟩ wi|

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

26090859375 / 4503599627370496 < |c2V ⟨0, ⋯⟩ ⟨4, ⋯⟩ wi|

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

26090859375 / 4503599627370496 < |c2V ⟨0, ⋯⟩ ⟨5, ⋯⟩ wi|

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

26090859375 / 4503599627370496 < |c2V ⟨0, ⋯⟩ ⟨6, ⋯⟩ wi|

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

26090859375 / 4503599627370496 < |c2V ⟨0, ⋯⟩ ⟨7, ⋯⟩ wi|

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

26090859375 / 4503599627370496 < |c2V ⟨0, ⋯⟩ ⟨8, ⋯⟩ wi|

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

26090859375 / 4503599627370496 < |c2V ⟨0, ⋯⟩ ⟨9, ⋯⟩ wi|

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

26090859375 / 4503599627370496 < |c2V ⟨0, ⋯⟩ ⟨10, ⋯⟩ wi|

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

26090859375 / 4503599627370496 < |c2V ⟨0, ⋯⟩ ⟨11, ⋯⟩ wi|

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

26090859375 / 4503599627370496 < |c2V ⟨1, ⋯⟩ ⟨0, ⋯⟩ wi|

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

26090859375 / 4503599627370496 < |c2V ⟨1, ⋯⟩ ⟨1, ⋯⟩ wi|

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

26090859375 / 4503599627370496 < |c2V ⟨1, ⋯⟩ ⟨2, ⋯⟩ wi|

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

26090859375 / 4503599627370496 < |c2V ⟨1, ⋯⟩ ⟨3, ⋯⟩ wi|

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

26090859375 / 4503599627370496 < |c2V ⟨1, ⋯⟩ ⟨4, ⋯⟩ wi|

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

26090859375 / 4503599627370496 < |c2V ⟨1, ⋯⟩ ⟨5, ⋯⟩ wi|

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

26090859375 / 4503599627370496 < |c2V ⟨1, ⋯⟩ ⟨6, ⋯⟩ wi|

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

26090859375 / 4503599627370496 < |c2V ⟨1, ⋯⟩ ⟨7, ⋯⟩ wi|

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

26090859375 / 4503599627370496 < |c2V ⟨1, ⋯⟩ ⟨8, ⋯⟩ wi|

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

26090859375 / 4503599627370496 < |c2V ⟨1, ⋯⟩ ⟨9, ⋯⟩ wi|

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

26090859375 / 4503599627370496 < |c2V ⟨1, ⋯⟩ ⟨10, ⋯⟩ wi|

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

26090859375 / 4503599627370496 < |c2V ⟨1, ⋯⟩ ⟨11, ⋯⟩ wi|

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

26090859375 / 4503599627370496 < |c2V o hi wi|

noncomputable def Proofs.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.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.TrainedCnnDescent.relu_c2 :

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

noncomputable def Proofs.TrainedCnnDescent.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.TrainedCnnDescent.pooled_eq :

maxPoolFlat 2 6 6 r2V.flatten = p2f

theorem Proofs.TrainedCnnDescent.zp_6_0 (cc : Fin 2) (kh kw : Fin 3) :

convPad 3 3 x1V cc kh kw ⟨6, ⋯⟩ ⟨0, ⋯⟩ = 0

theorem Proofs.TrainedCnnDescent.zp_6_1 (cc : Fin 2) (kh kw : Fin 3) :

convPad 3 3 x1V cc kh kw ⟨6, ⋯⟩ ⟨1, ⋯⟩ = 0

theorem Proofs.TrainedCnnDescent.zp_7_0 (cc : Fin 2) (kh kw : Fin 3) :

convPad 3 3 x1V cc kh kw ⟨7, ⋯⟩ ⟨0, ⋯⟩ = 0

theorem Proofs.TrainedCnnDescent.zp_7_1 (cc : Fin 2) (kh kw : Fin 3) :

convPad 3 3 x1V cc kh kw ⟨7, ⋯⟩ ⟨1, ⋯⟩ = 0

theorem Proofs.TrainedCnnDescent.zp_8_0 (cc : Fin 2) (kh kw : Fin 3) :

convPad 3 3 x1V cc kh kw ⟨8, ⋯⟩ ⟨0, ⋯⟩ = 0

theorem Proofs.TrainedCnnDescent.zp_8_1 (cc : Fin 2) (kh kw : Fin 3) :

convPad 3 3 x1V cc kh kw ⟨8, ⋯⟩ ⟨1, ⋯⟩ = 0

theorem Proofs.TrainedCnnDescent.zp_8_10 (cc : Fin 2) (kh kw : Fin 3) :

convPad 3 3 x1V cc kh kw ⟨8, ⋯⟩ ⟨10, ⋯⟩ = 0

theorem Proofs.TrainedCnnDescent.zp_8_11 (cc : Fin 2) (kh kw : Fin 3) :

convPad 3 3 x1V cc kh kw ⟨8, ⋯⟩ ⟨11, ⋯⟩ = 0

theorem Proofs.TrainedCnnDescent.zp_9_0 (cc : Fin 2) (kh kw : Fin 3) :

convPad 3 3 x1V cc kh kw ⟨9, ⋯⟩ ⟨0, ⋯⟩ = 0

theorem Proofs.TrainedCnnDescent.zp_9_1 (cc : Fin 2) (kh kw : Fin 3) :

convPad 3 3 x1V cc kh kw ⟨9, ⋯⟩ ⟨1, ⋯⟩ = 0

theorem Proofs.TrainedCnnDescent.zp_9_10 (cc : Fin 2) (kh kw : Fin 3) :

convPad 3 3 x1V cc kh kw ⟨9, ⋯⟩ ⟨10, ⋯⟩ = 0

theorem Proofs.TrainedCnnDescent.zp_9_11 (cc : Fin 2) (kh kw : Fin 3) :

convPad 3 3 x1V cc kh kw ⟨9, ⋯⟩ ⟨11, ⋯⟩ = 0

theorem Proofs.TrainedCnnDescent.zp_10_0 (cc : Fin 2) (kh kw : Fin 3) :

convPad 3 3 x1V cc kh kw ⟨10, ⋯⟩ ⟨0, ⋯⟩ = 0

theorem Proofs.TrainedCnnDescent.zp_10_1 (cc : Fin 2) (kh kw : Fin 3) :

convPad 3 3 x1V cc kh kw ⟨10, ⋯⟩ ⟨1, ⋯⟩ = 0

theorem Proofs.TrainedCnnDescent.zp_10_10 (cc : Fin 2) (kh kw : Fin 3) :

convPad 3 3 x1V cc kh kw ⟨10, ⋯⟩ ⟨10, ⋯⟩ = 0

theorem Proofs.TrainedCnnDescent.zp_10_11 (cc : Fin 2) (kh kw : Fin 3) :

convPad 3 3 x1V cc kh kw ⟨10, ⋯⟩ ⟨11, ⋯⟩ = 0

theorem Proofs.TrainedCnnDescent.zp_11_0 (cc : Fin 2) (kh kw : Fin 3) :

convPad 3 3 x1V cc kh kw ⟨11, ⋯⟩ ⟨0, ⋯⟩ = 0

theorem Proofs.TrainedCnnDescent.zp_11_1 (cc : Fin 2) (kh kw : Fin 3) :

convPad 3 3 x1V cc kh kw ⟨11, ⋯⟩ ⟨1, ⋯⟩ = 0

theorem Proofs.TrainedCnnDescent.zp_11_10 (cc : Fin 2) (kh kw : Fin 3) :

convPad 3 3 x1V cc kh kw ⟨11, ⋯⟩ ⟨10, ⋯⟩ = 0

theorem Proofs.TrainedCnnDescent.zp_11_11 (cc : Fin 2) (kh kw : Fin 3) :

convPad 3 3 x1V cc kh kw ⟨11, ⋯⟩ ⟨11, ⋯⟩ = 0

theorem Proofs.TrainedCnnDescent.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) ∨ ConvPatchEq 3 3 x1V (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 * (26090859375 / 4503599627370496) < c2V ⟨0, ⋯⟩ (winRowInv ⟨0, ⋯⟩ m.1) (winColInv wo m.2)

theorem Proofs.TrainedCnnDescent.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) ∨ ConvPatchEq 3 3 x1V (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 * (26090859375 / 4503599627370496) < c2V ⟨0, ⋯⟩ (winRowInv ⟨1, ⋯⟩ m.1) (winColInv wo m.2)

theorem Proofs.TrainedCnnDescent.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) ∨ ConvPatchEq 3 3 x1V (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 * (26090859375 / 4503599627370496) < c2V ⟨0, ⋯⟩ (winRowInv ⟨2, ⋯⟩ m.1) (winColInv wo m.2)

theorem Proofs.TrainedCnnDescent.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) ∨ ConvPatchEq 3 3 x1V (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 * (26090859375 / 4503599627370496) < c2V ⟨0, ⋯⟩ (winRowInv ⟨3, ⋯⟩ m.1) (winColInv wo m.2)

theorem Proofs.TrainedCnnDescent.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) ∨ ConvPatchEq 3 3 x1V (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 * (26090859375 / 4503599627370496) < c2V ⟨0, ⋯⟩ (winRowInv ⟨4, ⋯⟩ m.1) (winColInv wo m.2)

theorem Proofs.TrainedCnnDescent.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) ∨ ConvPatchEq 3 3 x1V (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 * (26090859375 / 4503599627370496) < c2V ⟨0, ⋯⟩ (winRowInv ⟨5, ⋯⟩ m.1) (winColInv wo m.2)

theorem Proofs.TrainedCnnDescent.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) ∨ ConvPatchEq 3 3 x1V (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 * (26090859375 / 4503599627370496) < c2V ⟨1, ⋯⟩ (winRowInv ⟨0, ⋯⟩ m.1) (winColInv wo m.2)

theorem Proofs.TrainedCnnDescent.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) ∨ ConvPatchEq 3 3 x1V (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 * (26090859375 / 4503599627370496) < c2V ⟨1, ⋯⟩ (winRowInv ⟨1, ⋯⟩ m.1) (winColInv wo m.2)

theorem Proofs.TrainedCnnDescent.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) ∨ ConvPatchEq 3 3 x1V (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 * (26090859375 / 4503599627370496) < c2V ⟨1, ⋯⟩ (winRowInv ⟨2, ⋯⟩ m.1) (winColInv wo m.2)

theorem Proofs.TrainedCnnDescent.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) ∨ ConvPatchEq 3 3 x1V (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 * (26090859375 / 4503599627370496) < c2V ⟨1, ⋯⟩ (winRowInv ⟨3, ⋯⟩ m.1) (winColInv wo m.2)

theorem Proofs.TrainedCnnDescent.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) ∨ ConvPatchEq 3 3 x1V (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 * (26090859375 / 4503599627370496) < c2V ⟨1, ⋯⟩ (winRowInv ⟨4, ⋯⟩ m.1) (winColInv wo m.2)

theorem Proofs.TrainedCnnDescent.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) ∨ ConvPatchEq 3 3 x1V (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 * (26090859375 / 4503599627370496) < c2V ⟨1, ⋯⟩ (winRowInv ⟨5, ⋯⟩ m.1) (winColInv wo m.2)

theorem Proofs.TrainedCnnDescent.pool_margin :

MaxPool2MarginQUpTo (26090859375 / 4503599627370496) (ConvPatchEq 3 3 x1V) c2V

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

noncomputable def Proofs.TrainedCnnDescent.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.TrainedCnnDescent.d3_eq (k : Fin 8) :

dense W3 b3 p2f k = d3V k

noncomputable def Proofs.TrainedCnnDescent.r3V :

relu(dense3) at the image, exact.

Equations

Proofs.TrainedCnnDescent.r3V = ![0, 0, 469269101 / 534773760, 0, 0, 18293036663 / 2139095040, 0, 0]

Instances For

theorem Proofs.TrainedCnnDescent.r3_eq :

relu 8 (dense W3 b3 p2f) = r3V

noncomputable def Proofs.TrainedCnnDescent.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.TrainedCnnDescent.d4_eq (k : Fin 8) :

dense W4 b4 r3V k = d4V k

theorem Proofs.TrainedCnnDescent.head_feat :

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

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

|W3 i j| ≤ 155 / 128

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

|W4 i j| ≤ 125 / 128

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

|W5 i j| ≤ 133 / 128

theorem Proofs.TrainedCnnDescent.radius_eq :

5 / 2 * (1 / 2 ^ 42 * cnnConv2GradBound 2 6 6 8 8 10 3 3 (5 / 2) (155 / 128) (125 / 128) (133 / 128)) = 26090859375 / 4503599627370496

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

theorem Proofs.TrainedCnnDescent.trained_cnn_conv2_sgd_descends_concrete :

cnnConv2KernelLoss b2 x1V W3 b3 W4 b4 W5 b5 lbl (W2.flatten - (1 / 2 ^ 42) • gradAt (cnnConv2KernelLoss b2 x1V W3 b3 W4 b4 W5 b5 lbl) W2.flatten) ≤ cnnConv2KernelLoss b2 x1V W3 b3 W4 b4 W5 b5 lbl W2.flatten - (1 / 2 ^ 42 * ∑ idx : Fin (2 * 2 * 3 * 3), gradAt (cnnConv2KernelLoss b2 x1V W3 b3 W4 b4 W5 b5 lbl) W2.flatten idx ^ 2) / 2

One exact-gradient SGD step on the conv2 kernel of a trained MNIST CNN, at a real test image with tied pool windows, decreases the cross-entropy loss by at least lr·‖∇L‖₂²/2, at lr = 2⁻42. Every hypothesis of cnn_conv2_exact_sgd_descends is discharged above.

theorem Proofs.TrainedCnnDescent.radius_bias_eq :

1 / 2 ^ 36 * cnnConv2BiasGradBound 2 6 6 8 8 10 (155 / 128) (125 / 128) (133 / 128) = 115959375 / 35184372088832

The conv2-bias rung's radius lr·G_b, exact; it sits inside the kernel rung's.

theorem Proofs.TrainedCnnDescent.trained_cnn_conv2_bias_sgd_descends_concrete :

cnnConv2BiasLoss W2 x1V W3 b3 W4 b4 W5 b5 lbl (b2 - (1 / 2 ^ 36) • gradAt (cnnConv2BiasLoss W2 x1V W3 b3 W4 b4 W5 b5 lbl) b2) ≤ cnnConv2BiasLoss W2 x1V W3 b3 W4 b4 W5 b5 lbl b2 - (1 / 2 ^ 36 * ∑ o : Fin 2, gradAt (cnnConv2BiasLoss W2 x1V W3 b3 W4 b4 W5 b5 lbl) b2 o ^ 2) / 2

One exact-gradient SGD step on the conv2 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⁻36. Every hypothesis of cnn_conv2_bias_exact_sgd_descends is discharged above; the relu₂ and pool margins are the kernel rung's (c2_margin, pool_margin) at a smaller radius.