RunLayerWeights.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Concrete layer weights combined with contiguous true-run decomposition.

theorem OAI.Problem335.RunLayerWeights.prod_ite_eq_powers line 15

Source documentation

A product of two possible layer weights depends only on the two layer counts.

theorem prod_ite_eq_powers {R : Type*} [CommMonoid R]
    (p : ι → Bool) (l : List ι) (a b : R) :
    (l.map (fun i => if p i then a else b)).prod =
      a ^ l.countP p * b ^ l.countP (fun i => !p i) := by
…

theorem OAI.Problem335.RunLayerWeights.layer_product_eq line 25

Source documentation

The derivative/multiplication layer product in the notation of the manuscript.

theorem layer_product_eq (p : ι → Bool) (l : List ι) (α β : ℝ) (hα : 0 < α) :
    (l.map (fun i => if p i then α⁻¹ else β)).prod =
      α ^ (-(l.countP p : ℝ)) * β ^ l.countP (fun i => !p i) := by
…

theorem OAI.Problem335.RunLayerWeights.layer_loss_sum_eq line 33

Source documentation

The rounding loss counts only multiplication layers.

theorem layer_loss_sum_eq (p : ι → Bool) (l : List ι) (ε : ℝ) :
    (l.map (fun i => if p i then 0 else ε)).sum =
      ε * (l.countP (fun i => !p i) : ℝ) := by
…

theorem OAI.Problem335.RunLayerWeights.selected_layer_product_le line 42

Source documentation

An interval discrepancy bound gives the required majorant on each true block.

theorem selected_layer_product_le {n : ℕ}
    (isV w : Fin (n + 1) → Bool) {α β ρ ε N : ℝ}
    (hα : 0 < α) (hα1 : α ≤ 1) (hβ : 0 ≤ β)
    (hβupper : β ≤ α ^ ρ * Real.exp ε) (hscale : α ^ (-(1 + ρ)) ≤ N)
    (hdiscrepancy : ∀ b : List (Fin (n + 1)), b <:+: List.ofFn id →
      (b.countP isV : ℝ) - ρ * b.countP (fun i => !isV i) ≤ 1 + ρ) :
    ((((List.ofFn id).filter w).map (fun i => if isV i then α⁻¹ else β))).prod ≤
      N ^ WordRuns.runCount w *
        Real.exp (ε * (((List.ofFn id).filter w).countP (fun i => !isV i) : ℝ)) := by
…

Mentions: OAI.Problem335.WordRuns.runCount

theorem OAI.Problem335.RunLayerWeights.selected_layer_product_le_length line 61

Source documentation

The total rounding cost is bounded by the length of the entire word.

theorem selected_layer_product_le_length {n : ℕ}
    (isV w : Fin (n + 1) → Bool) {α β ρ ε N : ℝ}
    (hα : 0 < α) (hα1 : α ≤ 1) (hβ : 0 ≤ β) (hε : 0 ≤ ε)
    (hβupper : β ≤ α ^ ρ * Real.exp ε) (hscale : α ^ (-(1 + ρ)) ≤ N)
    (hdiscrepancy : ∀ b : List (Fin (n + 1)), b <:+: List.ofFn id →
      (b.countP isV : ℝ) - ρ * b.countP (fun i => !isV i) ≤ 1 + ρ) :
    ((((List.ofFn id).filter w).map (fun i => if isV i then α⁻¹ else β))).prod ≤
      N ^ WordRuns.runCount w * Real.exp (ε * (n + 1 : ℕ)) := by
…

Mentions: OAI.Problem335.WordRuns.runCount

theorem OAI.Problem335.RunLayerWeights.indexed_discrepancy_of_word_discrepancy line 78

Source documentation

Transfer discrepancy bounds from a Boolean layer schedule to lists of its positions.

theorem indexed_discrepancy_of_word_discrepancy {n : ℕ}
    (isV : Fin n → Bool) (ρ : ℝ)
    (h : ∀ l : List Bool, l <:+: List.ofFn isV →
      (l.count true : ℝ) - ρ * l.count false ≤ 1 + ρ) :
    ∀ b : List (Fin n), b <:+: List.ofFn id →
      (b.countP isV : ℝ) - ρ * b.countP (fun i => !isV i) ≤ 1 + ρ := by
…

theorem OAI.Problem335.RunLayerWeights.selected_countP_eq_card line 101

Source documentation

List counts on the selected positions coincide with the finite-set cardinality.

theorem selected_countP_eq_card {n : ℕ} (w : Fin n → Bool) (V : Finset (Fin n)) :
    ((List.ofFn id).filter w).countP (fun i => decide (i ∈ V)) =
      (V.filter (fun i => w i = true)).card := by
…

theorem OAI.Problem335.RunLayerWeights.selected_layer_product_eq_powers line 114

Source documentation

The local layer product is exactly the count-based weight used by isolated flipping.

theorem selected_layer_product_eq_powers {n : ℕ} (w : Fin n → Bool)
    (V : Finset (Fin n)) (A B : ℝ) :
    ((((List.ofFn id).filter w).map (fun i => if i ∈ V then A else B))).prod =
      A ^ (V.filter (fun i => w i = true)).card *
        B ^ ((Finset.univ \ V).filter (fun i => w i = true)).card := by
…

theorem OAI.Problem335.RunLayerWeights.count_weight_le_exp_mul_runCount line 127

Source documentation

Exact count-based per-word estimate consumed by the corrected word-sum proof.

theorem count_weight_le_exp_mul_runCount {n : ℕ} (w : Fin (n + 1) → Bool)
    (V : Finset (Fin (n + 1))) {α β ρ ε N : ℝ}
    (hα : 0 < α) (hα1 : α ≤ 1) (hβ : 0 ≤ β) (hε : 0 ≤ ε)
    (hβupper : β ≤ α ^ ρ * Real.exp ε) (hscale : α ^ (-(1 + ρ)) ≤ N)
    (hdiscrepancy : ∀ b : List (Fin (n + 1)), b <:+: List.ofFn id →
      (b.countP (fun i => decide (i ∈ V)) : ℝ) -
        ρ * b.countP (fun i => !decide (i ∈ V)) ≤ 1 + ρ) :
    (α⁻¹) ^ (V.filter (fun i => w i = true)).card *
        β ^ ((Finset.univ \ V).filter (fun i => w i = true)).card ≤
      Real.exp (ε * (n + 1 : ℕ)) * N ^ WordRuns.runCount w := by
…

Mentions: OAI.Problem335.WordRuns.runCount