EdgeRecovery.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Recovering constant-sign edges from grading energy

The counting argument is separated from construction of the grading matrix. Its hypotheses are explicit entrywise, total-energy, and distance-energy facts. No edge-count or anticommutator conclusion is assumed.

def OAI.LeanBlast.GotsmanLinial.distanceShell line 26
Source documentation
A finite distance layer, also useful for weights indexed by ordered pairs.
```
def distanceShell (d : α → ℕ) (k : ℕ) : Finset α :=
…
```
theorem OAI.LeanBlast.GotsmanLinial.mem_distanceShell line 29
theorem OAI.LeanBlast.GotsmanLinial.twice_mass_sub_neighbor_le_distance line 35
Source documentation
Pointwise distance counting: distance-zero entries are the only possible source of a deficit between total mass and distance-weighted mass.
```
theorem twice_mass_sub_neighbor_le_distance (d : α → ℕ) (w : α → ℝ)
    (hw : ∀ a, 0 ≤ w a) :
    2 * (∑ a, w a) - (∑ a ∈ distanceShell d 1, w a) ≤
      2 * (∑ a ∈ distanceShell d 0, w a) + ∑ a, (d a : ℝ) * w a := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.distanceShell

theorem OAI.LeanBlast.GotsmanLinial.neighbor_deficit_le_twice_zero_mass line 59

Source documentation

The sum of the nonnegative neighbor deficits is controlled by twice the distance-zero energy. Equivalently, A₀ + F ≤ 2 A₀.

theorem neighbor_deficit_le_twice_zero_mass (d : α → ℕ) (w : α → ℝ)
    (hw : ∀ a, 0 ≤ w a)
    (htotal : (∑ a, w a) = ((distanceShell d 1).card : ℝ) / 4)
    (henergy : (∑ a, (d a : ℝ) * w a) ≤ ∑ a, w a) :
    (∑ a ∈ distanceShell d 1, ((1 / 4 : ℝ) - w a)) ≤
      2 * (∑ a ∈ distanceShell d 0, w a) := by
…

Mentions: OAI.LeanBlast.GotsmanLinial.distanceShell

theorem OAI.LeanBlast.GotsmanLinial.selected_neighbor_card_le_eight_mass line 71

Source documentation

Restricting the nonnegative deficits to any chosen neighbor subset gives the counting bound needed before applying the anticommutator identity.

theorem selected_neighbor_card_le_eight_mass (d : α → ℕ) (w : α → ℝ)
    (s : Finset α) (hs : s ⊆ distanceShell d 1)
    (hw : ∀ a, 0 ≤ w a)
    (hcap : ∀ a ∈ distanceShell d 1, w a ≤ (1 / 4 : ℝ))
    (htotal : (∑ a, w a) = ((distanceShell d 1).card : ℝ) / 4)
    (henergy : (∑ a, (d a : ℝ) * w a) ≤ ∑ a, w a) :
    (s.card : ℝ) ≤ 8 * ((∑ a ∈ distanceShell d 0, w a) + ∑ a ∈ s, w a) := by
…

Mentions: OAI.LeanBlast.GotsmanLinial.distanceShell

theorem OAI.LeanBlast.GotsmanLinial.anticommutator_entry_sq_of_same_sign line 91

Source documentation

On an equal-sign pair the anticommutator has four times the squared entry mass. The diagonal is included as an equal-sign pair.

theorem anticommutator_entry_sq_of_same_sign [DecidableEq ι]
    (M : Matrix ι ι ℂ) (h : ι → ℝ) (hh : ∀ i, h i = 1 ∨ h i = -1)
    (i j : ι) (hij : h i = h j) :
    ‖(M * Matrix.diagonal (fun i => (h i : ℂ)) +
      Matrix.diagonal (fun i => (h i : ℂ)) * M) i j‖ ^ 2 =
      4 * ‖M i j‖ ^ 2 := by
…

theorem OAI.LeanBlast.GotsmanLinial.anticommutator_energy_ge_selected line 109

Source documentation

The diagonal and a disjoint set of equal-sign neighbor entries contribute four times their mass to the Hilbert--Schmidt squared norm.

theorem anticommutator_energy_ge_selected [DecidableEq ι]
    (ρ : ι → ι → ℕ) (hzero : ∀ i j, ρ i j = 0 → i = j)
    (M : Matrix ι ι ℂ) (h : ι → ℝ) (hh : ∀ i, h i = 1 ∨ h i = -1)
    (s : Finset (ι × ι))
    (hs : s ⊆ distanceShell (fun p : ι × ι => ρ p.1 p.2) 1)
    (hsign : ∀ p ∈ s, h p.1 = h p.2) :
    4 * ((∑ p ∈ distanceShell (fun p : ι × ι => ρ p.1 p.2) 0,
        ‖M p.1 p.2‖ ^ 2) + ∑ p ∈ s, ‖M p.1 p.2‖ ^ 2) ≤
      hsNormSq (M * Matrix.diagonal (fun i => (h i : ℂ)) +
        Matrix.diagonal (fun i => (h i : ℂ)) * M) := by
…

Mentions: OAI.LeanBlast.GotsmanLinial.distanceShell, OAI.LeanBlast.GotsmanLinial.hsNormSq

theorem OAI.LeanBlast.GotsmanLinial.edge_recovery_for_subset line 152

Source documentation

Abstract edge recovery from the exact finite matrix energy hypotheses. The chosen set may be any subset of constant-sign distance-one pairs.

theorem edge_recovery_for_subset [DecidableEq ι]
    (ρ : ι → ι → ℕ) (hzero : ∀ i j, ρ i j = 0 → i = j)
    (M : Matrix ι ι ℂ) (h : ι → ℝ) (hh : ∀ i, h i = 1 ∨ h i = -1)
    (s : Finset (ι × ι))
    (hs : s ⊆ distanceShell (fun p : ι × ι => ρ p.1 p.2) 1)
    (hsign : ∀ p ∈ s, h p.1 = h p.2)
    (hcap : ∀ i j, ρ i j = 1 → ‖M i j‖ ^ 2 ≤ (1 / 4 : ℝ))
    (htotal : hsNormSq M =
      ((distanceShell (fun p : ι × ι => ρ p.1 p.2) 1).card : ℝ) / 4)
    (henergy : (∑ i, ∑ j, (ρ i j : ℝ) * ‖M i j‖ ^ 2) ≤ hsNormSq M) :
    (s.card : ℝ) ≤ 2 * hsNormSq
      (M * Matrix.diagonal (fun i => (h i : ℂ)) +
…

Mentions: OAI.LeanBlast.GotsmanLinial.distanceShell, OAI.LeanBlast.GotsmanLinial.hsNormSq

theorem OAI.LeanBlast.GotsmanLinial.edge_recovery line 175

Source documentation

The edge-recovery inequality on the Boolean cube, from the three matrix facts established by the grading and commutator constructions.

theorem edge_recovery {n : ℕ} (M : Matrix (Cube n) (Cube n) ℂ)
    (h : Cube n → ℝ) (hh : ∀ x, h x = 1 ∨ h x = -1)
    (htotal : hsNormSq M = (n : ℝ) * (2 : ℝ) ^ n / 4)
    (hdistance : (∑ x, ∑ y, (hammingDist x y : ℝ) * ‖M x y‖ ^ 2) ≤ hsNormSq M)
    (hcap : ∀ x y, x ≠ y → ‖M x y‖ ^ 2 ≤ (1 / 4 : ℝ)) :
    ((orderedConstantEdges h).card : ℝ) ≤
      2 * hsNormSq (M * Matrix.diagonal (fun x => (h x : ℂ)) +
        Matrix.diagonal (fun x => (h x : ℂ)) * M) := by
…

Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.hsNormSq, OAI.LeanBlast.GotsmanLinial.orderedConstantEdges