NetOperator.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Finite quarter-net tests imply the operator bound 10 for real operators.

theorem OAI.Dixmier.SphereNet.operator_norm_le_ten line 16

Source documentation

The two quarter-net errors each cost at most a quarter of the operator norm. Tests bounded by 5 therefore give operator norm at most 10.

theorem operator_norm_le_ten (M : E →L[ℝ] F) (s : Finset E) (t : Finset F)
    (_hs : ∀ x ∈ s, ‖x‖ = 1) (ht : ∀ y ∈ t, ‖y‖ = 1)
    (hsnet : ∀ x : E, ‖x‖ = 1 → ∃ x₀ ∈ s, ‖x-x₀‖ ≤ (1/4 : ℝ))
    (htnet : ∀ y : F, ‖y‖ = 1 → ∃ y₀ ∈ t, ‖y-y₀‖ ≤ (1/4 : ℝ))
    (hM : ∀ x ∈ s, ∀ y ∈ t, |inner ℝ (M x) y| ≤ 5) : ‖M‖ ≤ 10 := by
…