DegreeDiscrepancy.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.sum_positive_eq_half_sum_abs line 13
Source documentation
For a zero-sum finite family, its total positive discrepancy is half of its total absolute discrepancy. This is the algebraic identity used when ordering the factors in the product-rank argument.
```
theorem sum_positive_eq_half_sum_abs {ι : Type*} (s : Finset ι) (δ : ι → ℝ)
    (hδ : ∑ j ∈ s, δ j = 0) :
    ∑ j ∈ s.filter (fun j => 0 < δ j), δ j =
      (∑ j ∈ s, |δ j|) / 2 := by
…
```

theorem OAI.Problem335.sum_degree_discrepancy_eq_zero line 33

Source documentation

The proportional bidegree discrepancies sum to zero.

theorem sum_degree_discrepancy_eq_zero {ι : Type*} (s : Finset ι)
    (e i : ι → ℝ) (lam n k : ℝ)
    (he : ∑ j ∈ s, e j = n) (hi : ∑ j ∈ s, i j = k)
    (hlam : lam * n = k) :
    ∑ j ∈ s, (i j - lam * e j) = 0 := by
…

theorem OAI.Problem335.positive_bidegree_identity line 42

Source documentation

Collecting factors with positive proportional discrepancy expresses precisely the dimension-saving exponent in terms of absolute discrepancies.

theorem positive_bidegree_identity {ι : Type*} (s : Finset ι)
    (e i : ι → ℝ) (ρ lam : ℝ)
    (hlam : (1 + ρ) * lam = ρ)
    (hδ : ∑ j ∈ s, (i j - lam * e j) = 0) :
    (∑ j ∈ s.filter (fun j => 0 < i j - lam * e j), i j) -
      ρ * (∑ j ∈ s.filter (fun j => 0 < i j - lam * e j), (e j - i j)) =
      (1 + ρ) / 2 * (∑ j ∈ s, |i j - lam * e j|) := by
…

theorem OAI.Problem335.positive_bidegree_rpow line 61

Source documentation

Conversion of the intermediate-dimension exponent to a product of individual discrepancy weights.

theorem positive_bidegree_rpow {ι : Type*} (s : Finset ι)
    (e i : ι → ℝ) (ρ lam α : ℝ) (hα : 0 < α)
    (hlam : (1 + ρ) * lam = ρ)
    (hδ : ∑ j ∈ s, (i j - lam * e j) = 0) :
    α ^ ((∑ j ∈ s.filter (fun j => 0 < i j - lam * e j), i j) -
      ρ * (∑ j ∈ s.filter (fun j => 0 < i j - lam * e j), (e j - i j))) =
      ∏ j ∈ s, (α ^ ((1 + ρ) / 2)) ^ |i j - lam * e j| := by
…

theorem OAI.Problem335.constrained_sum_prod_le_prod_sum line 74

Source documentation

Dropping a constraint on independent choices and then distributing the finite sums is valid for nonnegative weights.

theorem constrained_sum_prod_le_prod_sum {ι : Type*} [Fintype ι] [DecidableEq ι]
    {κ : ι → Type*} (t : (j : ι) → Finset (κ j))
    (w : (j : ι) → κ j → ℝ)
    (hw : ∀ j x, x ∈ t j → 0 ≤ w j x)
    (P : ((j : ι) → κ j) → Prop) [DecidablePred P] :
    (∑ x ∈ (Fintype.piFinset t).filter P, ∏ j, w j (x j)) ≤
      ∏ j, ∑ x ∈ t j, w j x := by
…

def OAI.Problem335.degreeWeight line 90
Source documentation
The one-factor bidegree weight used in the manuscript.
```
def degreeWeight (q lam : ℝ) (e : ℕ) : ℝ :=
…
```

theorem OAI.Problem335.bidegree_weight_sum_le line 95

Source documentation

The bidegree-constrained sum in the product-rank bound is at most the product of the individual degree weights.

theorem bidegree_weight_sum_le {ι : Type*} [Fintype ι] [DecidableEq ι]
    (e : ι → ℕ) (k : ℕ) (q lam : ℝ) (hq : 0 ≤ q) :
    (∑ i ∈ (Fintype.piFinset (fun j => Finset.range (e j + 1))).filter
        (fun i => ∑ j, i j = k),
      ∏ j, q ^ |(i j : ℝ) - lam * e j|) ≤
      ∏ j, degreeWeight q lam (e j) := by
…

Mentions: OAI.Problem335.degreeWeight