Documentation

LeanMlir.Proofs.Certificates.Smoothing.NetSemantics

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). This file instantiates C as the argmax of a logit map and discharges both:

All results are propext / Classical.choice / Quot.sound-clean.

source
theorem Proofs.argmaxNet_nonempty {E : Type u_1} {k : ℕ} (f : E → Fin (k + 1) → ℝ) (x : E) :
{c : Fin (k + 1) | ∀ (j : Fin (k + 1)), f x j ≤ f x c}.Nonempty

Some logit is maximal: the maximizer set argmaxNet takes the least of is nonempty.

source
noncomputable def Proofs.argmaxNet {E : Type u_1} {k : ℕ} (f : E → Fin (k + 1) → ℝ) (x : E) :
Fin (k + 1)

The argmax classifier of a logit map, LOWEST index winning ties: the least index among the maximizers. Total and deterministic — the tie-break never matters at strict-argmax points.

Equations
Instances For
    source
    theorem Proofs.argmaxNet_isMax {E : Type u_1} {k : ℕ} (f : E → Fin (k + 1) → ℝ) (x : E) (j : Fin (k + 1)) :
    f x j ≤ f x (argmaxNet f x)
    source
    theorem Proofs.argmaxNet_eq_of_strict {E : Type u_1} {k : ℕ} {f : E → Fin (k + 1) → ℝ} {x : E} {c : Fin (k + 1)} (h : ∀ (j : Fin (k + 1)), j ≠ c → f x j < f x c) :
    argmaxNet f x = c

    At a STRICT argmax the tie-break is irrelevant: argmaxNet returns it.

    source
    theorem Proofs.measurable_argmaxNet {E : Type u_1} [MeasurableSpace E] {k : ℕ} {f : E → Fin (k + 1) → ℝ} (hf : ∀ (j : Fin (k + 1)), Measurable fun (x : E) => f x j) :
    Measurable (argmaxNet f)

    Fibers of argmaxNet from logit measurability: argmaxNet f x = c iff c maximizes at x and no smaller index does.

    source
    theorem Proofs.isOpen_strictRegion {E : Type u_1} [TopologicalSpace E] {k : ℕ} {f : E → Fin (k + 1) → ℝ} (hf : ∀ (j : Fin (k + 1)), Continuous fun (x : E) => f x j) (c : Fin (k + 1)) :
    IsOpen {x : E | ∀ (j : Fin (k + 1)), j ≠ c → f x j < f x c}
    source
    theorem Proofs.argmaxNet_smoothProb_mem_Ioo {n k : ℕ} {σ : ℝ} (hσ : 0 < σ) {f : EuclideanSpace ℝ (Fin (n + 1)) → Fin (k + 2) → ℝ} (hf : ∀ (j : Fin (k + 2)), Continuous fun (x : EuclideanSpace ℝ (Fin (n + 1))) => f x j) (w : Fin (k + 2) → EuclideanSpace ℝ (Fin (n + 1))) (hw : ∀ (c j : Fin (k + 2)), j ≠ c → f (w c) j < f (w c) c) (c : Fin (k + 1 + 1)) (x : EuclideanSpace ℝ (Fin (n + 1))) :
    ∫ (z : EuclideanSpace ℝ (Fin (n + 1))), if argmaxNet f (x + σ • z) = c then 1 else 0 ∂ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin (n + 1))) ∈ Set.Ioo 0 1

    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.

    source
    theorem Proofs.smoothing_cp_certified_net {n k : ℕ} {σ : ℝ} (hσ : 0 < σ) {f : EuclideanSpace ℝ (Fin (n + 1)) → Fin (k + 2) → ℝ} (hf : ∀ (j : Fin (k + 2)), Continuous fun (x : EuclideanSpace ℝ (Fin (n + 1))) => f x j) (w : Fin (k + 2) → EuclideanSpace ℝ (Fin (n + 1))) (hw : ∀ (c j : Fin (k + 2)), j ≠ c → f (w c) j < f (w c) c) (x : EuclideanSpace ℝ (Fin (n + 1))) (y : Fin (k + 2)) {N k₀ : ℕ} (hk₀ : k₀ ≤ N) {α q₀ : ℝ} (hα : 0 ≤ α) (hα1 : α < 1) (hq₀ : q₀ ∈ Set.Ioo 0 1) (htail : binomTail N k₀ q₀ ≤ α) :
    1 - α ≤ (MeasureTheory.Measure.pi fun (x : Fin N) => ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin (n + 1)))).real {ω : Fin N → EuclideanSpace ℝ (Fin (n + 1)) | (∑ i : Fin N, if argmaxNet f (x + σ • ω i) = y then 1 else 0) = k₀ → ∀ (δ : EuclideanSpace ℝ (Fin (n + 1))), ‖δ‖ < σ * stdNormalQuantile q₀ → ∀ (j : Fin (k + 2)), j ≠ y → ∫ (z : EuclideanSpace ℝ (Fin (n + 1))), if argmaxNet f (x + δ + σ • z) = j then 1 else 0 ∂ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin (n + 1))) < ∫ (z : EuclideanSpace ℝ (Fin (n + 1))), if argmaxNet f (x + δ + σ • z) = y then 1 else 0 ∂ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin (n + 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.