WordLocalProduct.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.WordLocalProduct.localFactor line 14
Source documentation
A per-layer factor in the normalized four-path moment bound. True is the diagonal type; A = alpha⁻¹, B = beta, x = n⁻¹.
```
def localFactor (V : Finset ι) (R : ι → ι → Prop) (A B x : ℝ)
    (w : ι → Bool) (i : ι) : ℝ :=
…
```
lemma OAI.Problem335.WordLocalProduct.localFactor_eq_parts line 20
theorem OAI.Problem335.WordLocalProduct.weight_eq_local_product line 32
Source documentation
The count-based word summand is exactly the product of the normalized local factors, including the normal-V coincidences.
```
theorem weight_eq_local_product (edges : Finset (ι × ι)) (V : Finset ι)
    (R : ι → ι → Prop) (A B x : ℝ) (w : ι → Bool) :
    IsolatedWeight.weight edges V R A B x w =
      x ^ SwitchRestoration.switchCount edges w * ∏ i, localFactor V R A B x w i := by
…
```
Mentions: OAI.Problem335.IsolatedWeight.weight, OAI.Problem335.SwitchRestoration.switchCount, OAI.Problem335.WordLocalProduct.localFactor

theorem OAI.Problem335.WordLocalProduct.weight_eq_inverse_local_product line 43

Source documentation

An inverse-natural-power form matching the manuscript's original parameters.

theorem weight_eq_inverse_local_product (edges : Finset (ι × ι)) (V : Finset ι)
    (R : ι → ι → Prop) (a b d : ℝ) (w : ι → Bool) :
    IsolatedWeight.weight edges V R a⁻¹ b d⁻¹ w =
      (d ^ SwitchRestoration.switchCount edges w)⁻¹ *
        ∏ i, if i ∈ V then
          if w i = true then a⁻¹ else
            1 + a⁻¹ * (d ^ (IsolatedWeight.falseNeighbors R w i).card)⁻¹
        else if w i = true then b else 1 := by
…

Mentions: OAI.Problem335.IsolatedWeight.weight, OAI.Problem335.SwitchRestoration.switchCount, OAI.Problem335.IsolatedWeight.falseNeighbors

lemma OAI.Problem335.WordLocalProduct.localFactor_nonneg line 54
def OAI.Problem335.WordLocalProduct.momentLocalFactor line 62
Source documentation
Before discarding U-coincidence factors, a normal U layer may have weight 1+B. The Boolean coincides records the relevant equality event.
```
def momentLocalFactor (V : Finset ι) (R : ι → ι → Prop) (A B x : ℝ)
    (w coincides : ι → Bool) (i : ι) : ℝ :=
…
```
lemma OAI.Problem335.WordLocalProduct.momentLocalFactor_nonneg line 67
lemma OAI.Problem335.WordLocalProduct.momentLocalFactor_le line 76

theorem OAI.Problem335.WordLocalProduct.prod_momentLocalFactor_le line 88

Source documentation

The global U-coincidence cost is at most (1+B)^|U|, without any independence assumption on U layers.

theorem prod_momentLocalFactor_le (V : Finset ι) (R : ι → ι → Prop)
    {A B x : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (hx : 0 ≤ x)
    (w coincides : ι → Bool) :
    (∏ i, momentLocalFactor V R A B x w coincides i) ≤
      (∏ i, localFactor V R A B x w i) * (1 + B) ^ (Finset.univ \ V).card := by
…

Mentions: OAI.Problem335.WordLocalProduct.momentLocalFactor, OAI.Problem335.WordLocalProduct.localFactor

theorem OAI.Problem335.WordLocalProduct.switchWeighted_momentLocalFactor_le line 102

Source documentation

A switch-weighted local moment product is controlled by the canonical word weight and the single global U-coincidence factor.

theorem switchWeighted_momentLocalFactor_le (edges : Finset (ι × ι))
    (V : Finset ι) (R : ι → ι → Prop) {A B x : ℝ}
    (hA : 0 ≤ A) (hB : 0 ≤ B) (hx : 0 ≤ x) (w coincides : ι → Bool) :
    x ^ SwitchRestoration.switchCount edges w *
        (∏ i, momentLocalFactor V R A B x w coincides i) ≤
      (1 + B) ^ (Finset.univ \ V).card * IsolatedWeight.weight edges V R A B x w := by
…

Mentions: OAI.Problem335.SwitchRestoration.switchCount, OAI.Problem335.WordLocalProduct.momentLocalFactor, OAI.Problem335.IsolatedWeight.weight

theorem OAI.Problem335.WordLocalProduct.sum_switchWeighted_momentLocalFactor_le line 116

Source documentation

The global moment reduction may discard all U-coincidence events, even when they depend jointly on the entire word.

theorem sum_switchWeighted_momentLocalFactor_le (edges : Finset (ι × ι))
    (V : Finset ι) (R : ι → ι → Prop) {A B x : ℝ}
    (hA : 0 ≤ A) (hB : 0 ≤ B) (hx : 0 ≤ x)
    (coincides : (ι → Bool) → ι → Bool) :
    (∑ w : ι → Bool, x ^ SwitchRestoration.switchCount edges w *
      (∏ i, momentLocalFactor V R A B x w (coincides w) i)) ≤
      (1 + B) ^ (Finset.univ \ V).card *
        ∑ w : ι → Bool, IsolatedWeight.weight edges V R A B x w := by
…

Mentions: OAI.Problem335.SwitchRestoration.switchCount, OAI.Problem335.WordLocalProduct.momentLocalFactor, OAI.Problem335.IsolatedWeight.weight