CutBounds.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Real cut tests control complex label energies

This is the deterministic estimate (graph-cut-labels) in the manuscript. It makes no independence assumption about the labels and the kernel.

def OAI.JointDickman.cutSign line 18
Source documentation
Signs used in the finite cut maximum.
```
def cutSign (b : Bool) : ℝ := if b then 1 else -1
```
theorem OAI.JointDickman.abs_cutSign line 20

theorem OAI.JointDickman.linear_bound_of_signs line 24

Source documentation

A linear test bounded for all sign vectors is bounded throughout the cube.

theorem linear_bound_of_signs {ι : Type*} [Fintype ι] (a : ι → ℝ) (C : ℝ)
    (hsign : ∀ s : ι → Bool, |∑ i, a i * cutSign (s i)| ≤ C)
    (f : ι → ℝ) (hf : ∀ i, |f i| ≤ 1) : |∑ i, a i * f i| ≤ C := by
…

Mentions: OAI.JointDickman.cutSign

def OAI.JointDickman.realBilinear line 48
def OAI.JointDickman.complexEnergy line 52

theorem OAI.JointDickman.realBilinear_bound_of_signs line 58

Source documentation

The two applications of the linear sign lemma give the exact extension from the finite sign maximum to arbitrary real test coordinates in [-1,1].

theorem realBilinear_bound_of_signs {ι : Type*} [Fintype ι]
    (K : ι → ι → ℝ) (C : ℝ)
    (hcut : ∀ s t : ι → Bool,
      |realBilinear K (fun i => cutSign (s i)) (fun j => cutSign (t j))| ≤ C)
    (f g : ι → ℝ) (hf : ∀ i, |f i| ≤ 1) (hg : ∀ i, |g i| ≤ 1) :
    |realBilinear K f g| ≤ C := by
…

Mentions: OAI.JointDickman.realBilinear, OAI.JointDickman.cutSign

theorem OAI.JointDickman.realBilinear_rescale line 88
theorem OAI.JointDickman.realBilinear_bound_two line 99
theorem OAI.JointDickman.complexEnergy_re line 115
theorem OAI.JointDickman.complexEnergy_im line 123

theorem OAI.JointDickman.complexEnergy_le_sixteen line 132

Source documentation

The factor 16 is the one used when the centered labels have norm at most 2.

theorem complexEnergy_le_sixteen {ι : Type*} [Fintype ι]
    (K : ι → ι → ℝ) (C : ℝ)
    (hcut : ∀ f g : ι → ℝ, (∀ i, |f i| ≤ 1) → (∀ i, |g i| ≤ 1) →
      |realBilinear K f g| ≤ C)
    (z : ι → ℂ) (hz : ∀ i, ‖z i‖ ≤ 2) :
    ‖complexEnergy K z‖ ≤ 16 * C := by
…

Mentions: OAI.JointDickman.realBilinear, OAI.JointDickman.complexEnergy

theorem OAI.JointDickman.complexEnergy_le_sixteen_of_signs line 158

Source documentation

This uses exactly the finite sign tests in the manuscript's cut norm.

theorem complexEnergy_le_sixteen_of_signs {ι : Type*} [Fintype ι]
    (K : ι → ι → ℝ) (C : ℝ)
    (hcut : ∀ s t : ι → Bool,
      |realBilinear K (fun i => cutSign (s i)) (fun j => cutSign (t j))| ≤ C)
    (z : ι → ℂ) (hz : ∀ i, ‖z i‖ ≤ 2) :
    ‖complexEnergy K z‖ ≤ 16 * C :=
…

Mentions: OAI.JointDickman.realBilinear, OAI.JointDickman.cutSign, OAI.JointDickman.complexEnergy