Net semantics for the smoothing chain — the classifier becomes a NET #
The smoothing chain up through smoothing_cp_certified_solved quantifies over
an ABSTRACT measurable classifier C with an interiority hypothesis
hp : ∀ c x, p_c(x) ∈ (0,1) — the last informality flagged in the scorecard
headers. This file closes it:
argmaxNet— the argmax classifier of a logit map (lowest index wins ties; the tie-break is irrelevant at strict-argmax points), withmeasurable_argmaxNetfrom logit measurability alone (fibers are finite boolean combinations of{f·j ≤ f·c}sets);isOpen_strictRegion— strict decision regions of continuous logits are open;stdGaussianfull support —IsOpenPosMeasureinstances forgaussianReal 0 1(fromstdGaussian_Ioo_pos) and for the multivariatestdGaussian E(pushforward of the pi-Gaussian under the surjective continuous basis sum;pi.isOpenPosMeasuredoes the product);argmaxNet_smoothProb_mem_Ioo— thehpdischarge: ONE strict-argmax witness per class ⇒ every smoothed class probability at every point is in(0,1)(the witness's open region has positive Gaussian mass everywhere; any OTHER class's region caps it below 1);smoothing_cp_certified_net— the capstone: CERTIFY's guarantee with the classifier INSTANTIATED asargmaxNet f, measurability andhpboth discharged from continuity + witnesses;mlpT_logit_continuous— the trained /128-rationalized pooled-MNIST MLP's logits are continuous (the concrete instantiation lives in the generatedSmoothingNetWitness.lean).
All results are propext / Classical.choice / Quot.sound-clean.
Fibers of argmaxNet from logit measurability: argmaxNet f x = c iff
c maximizes at x and no smaller index does.
N(0,1) charges every nonempty open set (the pdf is everywhere positive) —
packaged as the Mathlib IsOpenPosMeasure class.
The standard Gaussian on a finite-dimensional inner-product space charges
every nonempty open set: it is the pushforward of the pi-Gaussian (open-pos
by pi.isOpenPosMeasure) under the surjective continuous basis sum.
hp interiority from per-class witnesses. If every class has a point
where it is the STRICT argmax of the continuous logits, then under
Gaussian smoothing EVERY class probability at EVERY point is in (0,1):
exactly the hp hypothesis of the smoothing chain. Needs ≥ 2 classes
(Fin (k+2)) — with one class p ≡ 1.
The net-semantics capstone. smoothing_cp_certified_solved with the
classifier INSTANTIATED as the argmax of a concrete continuous logit map:
measurability and hp interiority are DISCHARGED (from continuity and
per-class strict-argmax witnesses). With probability ≥ 1 − α over the
N Gaussian samples: if the vote count for class y comes out k₀
(where binomTail N k₀ q₀ ≤ α is one kernel check), every perturbation
‖δ‖ < σ·Φ⁻¹(q₀) leaves y the strict argmax of the SMOOTHED net.
Each logit of the trained pooled-MNIST MLP is continuous: the coordinate
formula ∑ k, W2ⱼₖ·max(∑ l, W1ₖₗ·xₗ, 0) is definitional.