WordSum.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Assembly of the numeric and finite-word estimates in the path-type sum. The remaining application-specific hypotheses describe the actual path weights.

lemma OAI.Problem335.WordSum.corrected_sum_le_exp_of_sum line 19

Source documentation

Combine exact smoothing fibers, surviving local corrections, and interior-run counting.

lemma corrected_sum_le_exp_of_sum (n k : ℕ) (a c : ℝ)
    (S : Finset (Fin (n + 1))) (R : Fin (n + 1) → Fin (n + 1) → Prop)
    (hS : ∀ i ∈ S, ∀ j, R i j → j ∉ S)
    (hcard : S.card ≤ k)
    (hk : 2 * (k : ℝ) ≤ ((n + 1 : ℕ) : ℝ))
    (ha : 0 ≤ a) (haN : a ≤ Real.sqrt ((n + 1 : ℕ) : ℝ))
    (hc : 0 ≤ c) (hcN : c ≤ 2 / (((n + 1 : ℕ) : ℝ) ^ 2))
    (W Z : (Fin (n + 1) → Bool) → ℝ)
    (hWnonneg : ∀ w, 0 ≤ W w) (hZnonneg : ∀ w, 0 ≤ Z w)
    (hratio : ∀ w, W w = W (IsolatedFlip.flip S R w) *
      c ^ (IsolatedFlip.removed S R w).card)
    (hfixed : ∀ w, IsolatedFlip.flip S R w = w →
…

Mentions: OAI.Problem335.IsolatedFlip.flip, OAI.Problem335.IsolatedFlip.removed

lemma OAI.Problem335.WordSum.sum_actual_weight_le_exp line 74

Source documentation

The actual word weights satisfy the square-root exponential bound once run intervals and the surviving coincidence corrections have been estimated.

lemma sum_actual_weight_le_exp (n : ℕ) (A B E : ℝ)
    (edges : Finset (Fin (n + 1) × Fin (n + 1)))
    (V S : Finset (Fin (n + 1))) (R : Fin (n + 1) → Fin (n + 1) → Prop)
    (hS : S ⊆ V) (hV : ∀ i ∈ V, ∀ j, R i j → j ∉ V)
    (hR : ∀ e ∈ edges, R e.1 e.2 ∧ R e.2 e.1)
    (hdegree : ∀ i ∈ S, SwitchRestoration.endpointDegree edges i = 2)
    (hswitch : ∀ w, SwitchRestoration.switchCount edges w = (WordSwitches.switches w).card)
    (hcard : 2 * (V.card : ℝ) ≤ ((n + 1 : ℕ) : ℝ))
    (hA : 1 ≤ A) (hAN : A ≤ Real.sqrt ((n + 1 : ℕ) : ℝ)) (hB : 0 ≤ B)
    (hE : E ≤ Real.sqrt ((n + 1 : ℕ) : ℝ))
    (hprod : ∀ w : Fin (n + 1) → Bool,
      A ^ (V.filter fun i => w i = true).card *
…

Mentions: OAI.Problem335.SwitchRestoration.endpointDegree, OAI.Problem335.SwitchRestoration.switchCount, OAI.Problem335.WordSwitches.switches

lemma OAI.Problem335.WordSum.sum_actual_weight_le_exp_of_endpoints line 139

Source documentation

Full corrected-word bound with the actual fixed-word correction estimate discharged. Only the graph structure and the per-word product-of-runs estimate remain as inputs.

lemma sum_actual_weight_le_exp_of_endpoints (n : ℕ) (A B E : ℝ)
    (edges : Finset (Fin (n + 1) × Fin (n + 1)))
    (V S : Finset (Fin (n + 1))) (R : Fin (n + 1) → Fin (n + 1) → Prop)
    (hS : S ⊆ V) (hV : ∀ i ∈ V, ∀ j, R i j → j ∉ V)
    (hR : ∀ e ∈ edges, R e.1 e.2 ∧ R e.2 e.1)
    (hdegree : ∀ i ∈ S, SwitchRestoration.endpointDegree edges i = 2)
    (hswitch : ∀ w, SwitchRestoration.switchCount edges w = (WordSwitches.switches w).card)
    (hend : (V \ S).card ≤ 1)
    (hcard : 2 * (V.card : ℝ) ≤ ((n + 1 : ℕ) : ℝ))
    (hA : 1 ≤ A) (hAN : A ≤ Real.sqrt ((n + 1 : ℕ) : ℝ)) (hB : 0 ≤ B)
    (hE : E ≤ Real.sqrt ((n + 1 : ℕ) : ℝ))
    (hprod : ∀ w : Fin (n + 1) → Bool,
…

Mentions: OAI.Problem335.SwitchRestoration.endpointDegree, OAI.Problem335.SwitchRestoration.switchCount, OAI.Problem335.WordSwitches.switches

lemma OAI.Problem335.WordSum.sum_weight_le_exp_of_discrepancy line 167

Source documentation

An interval-balanced independent layer partition gives the full word-sum estimate. This version has no assumed rank, trace, weight, or run-product inequalities.

lemma sum_weight_le_exp_of_discrepancy (n : ℕ) (α β ρ ε : ℝ)
    (edges : Finset (Fin (n + 1) × Fin (n + 1)))
    (V S : Finset (Fin (n + 1))) (R : Fin (n + 1) → Fin (n + 1) → Prop)
    (hS : S ⊆ V) (hV : ∀ i ∈ V, ∀ j, R i j → j ∉ V)
    (hR : ∀ e ∈ edges, R e.1 e.2 ∧ R e.2 e.1)
    (hdegree : ∀ i ∈ S, SwitchRestoration.endpointDegree edges i = 2)
    (hswitch : ∀ w, SwitchRestoration.switchCount edges w = (WordSwitches.switches w).card)
    (hend : (V \ S).card ≤ 1)
    (hcard : 2 * (V.card : ℝ) ≤ ((n + 1 : ℕ) : ℝ))
    (hα : 0 < α) (hα1 : α ≤ 1) (hβ : 0 ≤ β) (hρ : ρ ≤ 1) (hε : 0 ≤ ε)
    (hαN : α⁻¹ ≤ Real.sqrt ((n + 1 : ℕ) : ℝ))
    (hβupper : β ≤ α ^ ρ * Real.exp ε)
…

Mentions: OAI.Problem335.SwitchRestoration.endpointDegree, OAI.Problem335.SwitchRestoration.switchCount, OAI.Problem335.WordSwitches.switches