CircuitDegreeBounds.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.d5LeafDegree_le_one line 13
Source documentation
Every input leaf has formal degree at most one.
```
theorem d5LeafDegree_le_one (x : D5Leaf K n) : d5LeafDegree x ≤ 1 := by
…
```
Mentions: OAI.Problem335.D5Leaf, OAI.Problem335.d5LeafDegree
theorem OAI.Problem335.bottomDegree_le_one line 17
Source documentation
Bottom sums have degree zero or one, including empty bottom sums.
```
theorem bottomDegree_le_one (c : Depth5Circuit K n) (i : Fin c.bottomCount) :
    c.bottomDegree i ≤ 1 := by
…
```
Mentions: OAI.Problem335.Depth5Circuit
theorem OAI.Problem335.leaf_scalar_of_degree_zero line 28
Source documentation
A zero-degree leaf is a scalar, syntactically, even if its value is zero.
```
theorem leaf_scalar_of_degree_zero (x : D5Leaf K n) (h : d5LeafDegree x = 0) :
    ∃ a : K, x = D5Leaf.scalar a := by
…
```
Mentions: OAI.Problem335.D5Leaf, OAI.Problem335.d5LeafDegree
theorem OAI.Problem335.leaf_variable_of_degree_pos line 36
Source documentation
A positive-degree leaf is a variable.
```
theorem leaf_variable_of_degree_pos (x : D5Leaf K n) (h : 0 < d5LeafDegree x) :
    ∃ v, x = D5Leaf.variable v := by
…
```
Mentions: OAI.Problem335.D5Leaf, OAI.Problem335.d5LeafDegree

theorem OAI.Problem335.sum_map_eq_length_filter_one line 43

Source documentation

For a list of zeros and ones, the formal degree is the number of one inputs.

theorem sum_map_eq_length_filter_one {α : Type*} (d : α → ℕ) (l : List α)
    (hd : ∀ a ∈ l, d a ≤ 1) :
    (l.map d).sum = (l.filter fun a => d a = 1).length := by
…

theorem OAI.Problem335.lowerDegree_eq_linear_count line 55

Source documentation

Repeated lower-product inputs count separately in their formal degree.

theorem lowerDegree_eq_linear_count (c : Depth5Circuit K n) (i : Fin c.lowerCount) :
    ((c.lowerInputs i).map c.bottomDegree).sum =
      ((c.lowerInputs i).filter fun j => c.bottomDegree j = 1).length := by
…

Mentions: OAI.Problem335.Depth5Circuit

theorem OAI.Problem335.length_filter_pos_le_sum_map line 63
Source documentation
The number of positive-degree input occurrences is bounded by their total degree.
```
theorem length_filter_pos_le_sum_map {α : Type*} (d : α → ℕ) (l : List α) :
    (l.filter fun a => 0 < d a).length ≤ (l.map d).sum := by
…
```

theorem OAI.Problem335.upper_positive_count_le_degree line 75

Source documentation

The number of positive-degree middle factors is bounded by an upper product's degree.

theorem upper_positive_count_le_degree (c : Depth5Circuit K n) (i : Fin c.upperCount) :
    ((c.upperInputs i).filter fun j => 0 < c.middleDegree j).length ≤
      ((c.upperInputs i).map c.middleDegree).sum :=
…

Mentions: OAI.Problem335.Depth5Circuit

theorem OAI.Problem335.output_term_positive_count_le_degree line 81

Source documentation

An upper term that occurs at the output has at most outputDegree positive factors.

theorem output_term_positive_count_le_degree (c : Depth5Circuit K n)
    (entry : K × Fin c.upperCount) (hentry : entry ∈ c.outputInputs) :
    ((c.upperInputs entry.2).filter fun j => 0 < c.middleDegree j).length ≤
      c.outputDegree := by
…

Mentions: OAI.Problem335.Depth5Circuit

theorem OAI.Problem335.sum_eq_C_of_mem line 89

Source documentation

A finite sum of scalar polynomials is a scalar polynomial.

theorem sum_eq_C_of_mem {σ : Type*} (l : List (MvPolynomial σ K))
    (h : ∀ p ∈ l, ∃ a : K, p = MvPolynomial.C a) :
    ∃ a : K, l.sum = MvPolynomial.C a := by
…

theorem OAI.Problem335.bottomValue_eq_C_of_degree_zero line 100
Source documentation
Zero-degree bottom sums really compute scalars; cancellation is harmless.
```
theorem bottomValue_eq_C_of_degree_zero (c : Depth5Circuit K n)
    (i : Fin c.bottomCount) (hdeg : c.bottomDegree i = 0) :
    ∃ a : K, bottomValue c i = MvPolynomial.C a := by
…
```
Mentions: OAI.Problem335.Depth5Circuit, OAI.Problem335.bottomValue

theorem OAI.Problem335.threshold_mul_length_filter_le_sum line 112

Source documentation

Large-degree occurrences are bounded using their total formal degree.

theorem threshold_mul_length_filter_le_sum {α : Type*} (d : α → ℕ)
    (l : List α) (t : ℕ) :
    t * (l.filter fun a => t ≤ d a).length ≤ (l.map d).sum := by
…

theorem OAI.Problem335.output_term_high_count_bound line 124

Source documentation

The manuscript's number of high-degree occurrences bound for an upper term.

theorem output_term_high_count_bound (c : Depth5Circuit K n)
    (entry : K × Fin c.upperCount) (hentry : entry ∈ c.outputInputs) (t : ℕ) :
    t * ((c.upperInputs entry.2).filter fun j => t ≤ c.middleDegree j).length ≤
      c.outputDegree := by
…

Mentions: OAI.Problem335.Depth5Circuit

theorem OAI.Problem335.real_threshold_mul_length_filter_le_sum line 132

Source documentation

Real thresholds need not be rounded to bound the number of large factors.

theorem real_threshold_mul_length_filter_le_sum {α : Type*} (d : α → ℕ)
    (l : List α) (t : ℝ) :
    t * ((l.filter fun a => t ≤ (d a : ℝ)).length : ℝ) ≤ (l.map d).sum := by
…

theorem OAI.Problem335.output_term_high_count_le_div line 147

Source documentation

The number of high middle-factor occurrences is at most output degree / threshold.

theorem output_term_high_count_le_div (c : Depth5Circuit K n)
    (entry : K × Fin c.upperCount) (hentry : entry ∈ c.outputInputs)
    (t : ℝ) (ht : 0 < t) :
    (((c.upperInputs entry.2).filter fun j => t ≤ (c.middleDegree j : ℝ)).length : ℝ) ≤
      (c.outputDegree : ℝ) / t := by
…

Mentions: OAI.Problem335.Depth5Circuit