SwitchingNorm.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Norm estimates for the actual switching differences

These elementary estimates are applied to root outputs from one chronological switching experiment. The construction of those outputs and their before- and after-block bounds is separate from the linear-functional calculations here.

theorem OAI.ReflexiveFixedPoints.abs_functional_apply_le_norm line 23
Source documentation
A functional of operator norm at most one is bounded by the given norm.
```
theorem abs_functional_apply_le_norm (f : X →L[ℝ] ℝ) (hf : ‖f‖ ≤ 1) (z : X) :
    |f z| ≤ ‖z‖ := by
…
```
theorem OAI.ReflexiveFixedPoints.detector_transfer_le line 33
Source documentation
Transfer a detector from two comparison points to the actual before/after outputs. This uses linearity only of the detector, not of the node maps.
```
theorem detector_transfer_le (f : X →L[ℝ] ℝ) (hf : ‖f‖ ≤ 1)
    (U V y q : X) :
    f (y - q) - ‖U - y‖ - ‖V - q‖ ≤ f (U - V) := by
…
```

theorem OAI.ReflexiveFixedPoints.block_detection_of_norm_bounds line 47

Source documentation

The exact W - 5e detector estimate from the three already proved actual terminal, before-block, and after-block inequalities.

theorem block_detection_of_norm_bounds (f : X →L[ℝ] ℝ) (hf : ‖f‖ ≤ 1)
    (U V y q : X) (W e : ℝ)
    (hterminal : 1 - 2 * e ≤ f (y - q))
    (hbefore : ‖U - y‖ ≤ 1 - W + 2 * e)
    (hafter : ‖V - q‖ ≤ e) :
    W - 5 * e ≤ f (U - V) := by
…

theorem OAI.ReflexiveFixedPoints.normalized_switch_difference line 59
Source documentation
Normalization of a single actual root increment preserves its subspace, puts it in the unit ball, and reconstructs it upon multiplication by its weight. The weight may be arbitrarily small; only strict positivity is required.
```
theorem normalized_switch_difference (Y : Submodule ℝ X)
    (U V : X) (W : ℝ) (hW : 0 < W)
    (hmem : U - V ∈ Y) (hnorm : ‖U - V‖ ≤ W) :
    W⁻¹ • (U - V) ∈ Y ∧
      ‖W⁻¹ • (U - V)‖ ≤ 1 ∧
      W • (W⁻¹ • (U - V)) = U - V := by
…
```
theorem OAI.ReflexiveFixedPoints.functional_apply_le_one line 74
Source documentation
Unit-ball vectors have detector score at most one.
```
theorem functional_apply_le_one (f : X →L[ℝ] ℝ) (hf : ‖f‖ ≤ 1)
    (z : X) (hz : ‖z‖ ≤ 1) : f z ≤ 1 :=
…
```