BidegreeAverages.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.Problem335.BidegreeAverages.Composition line 11
Source documentation
A weak composition indexed by a finite variable set.
```
abbrev Composition (σ : Type*) [Fintype σ] (a : ℕ) :=
…
```
abbrev OAI.Problem335.BidegreeAverages.Index line 15
Source documentation
The exponent index set for the source of the mixed operator.
```
abbrev Index {σ : Type*} (isV : σ → Bool) (a b : ℕ) :=
…
```

theorem OAI.Problem335.BidegreeAverages.sum_split line 21

Source documentation

Summing a separated function over bihomogeneous exponent vectors factors into the two weak-composition sums. This is the independence of the two occupation groups, not independence of coordinates within either group.

theorem sum_split {σ : Type*} [Fintype σ] (isV : σ → Bool) (a b : ℕ)
    (f : ({x // isV x = true} → ℕ) → ℝ)
    (g : ({x // ¬ isV x = true} → ℕ) → ℝ) :
    (∑' d : Index isV a b,
      f (fun x => d.val x) * g (fun x => d.val x)) =
      (∑' v : Composition {x // isV x = true} a, f v.val) *
        (∑' u : Composition {x // ¬ isV x = true} b, g u.val) := by
…

Mentions: OAI.Problem335.BidegreeAverages.Index, OAI.Problem335.BidegreeAverages.Composition

theorem OAI.Problem335.BidegreeAverages.average_split line 48

Source documentation

The normalized form of sum_split: the uniform domain occupation average is the product of the two uniform weak-composition averages. Empty index sets are handled by the usual convention that division by zero is zero.

theorem average_split {σ : Type*} [Fintype σ] (isV : σ → Bool) (a b : ℕ)
    (f : ({x // isV x = true} → ℕ) → ℝ)
    (g : ({x // ¬ isV x = true} → ℕ) → ℝ) :
    (∑' d : Index isV a b,
      f (fun x => d.val x) * g (fun x => d.val x)) /
      (Nat.card (Index isV a b) : ℝ) =
      ((∑' v : Composition {x // isV x = true} a, f v.val) /
        (Nat.card (Composition {x // isV x = true} a) : ℝ)) *
      ((∑' u : Composition {x // ¬ isV x = true} b, g u.val) /
        (Nat.card (Composition {x // ¬ isV x = true} b) : ℝ)) := by
…

Mentions: OAI.Problem335.BidegreeAverages.Index, OAI.Problem335.BidegreeAverages.Composition

theorem OAI.Problem335.BidegreeAverages.sum_split_fintype line 63

Source documentation

Finite-sum version, compatible with any chosen enumerations of the three finite index types (in particular with matrix bases).

theorem sum_split_fintype {σ : Type*} [Fintype σ] (isV : σ → Bool) (a b : ℕ)
    [Fintype (Index isV a b)]
    [Fintype (Composition {x // isV x = true} a)]
    [Fintype (Composition {x // ¬ isV x = true} b)]
    (f : ({x // isV x = true} → ℕ) → ℝ)
    (g : ({x // ¬ isV x = true} → ℕ) → ℝ) :
    (∑ d : Index isV a b,
      f (fun x => d.val x) * g (fun x => d.val x)) =
      (∑ v : Composition {x // isV x = true} a, f v.val) *
        (∑ u : Composition {x // ¬ isV x = true} b, g u.val) := by
…

Mentions: OAI.Problem335.BidegreeAverages.Index, OAI.Problem335.BidegreeAverages.Composition

theorem OAI.Problem335.BidegreeAverages.average_split_multichoose line 76

Source documentation

The average identity with the exact stars-and-bars dimension factors.

theorem average_split_multichoose {σ : Type*} [Fintype σ]
    (isV : σ → Bool) (a b : ℕ)
    (f : ({x // isV x = true} → ℕ) → ℝ)
    (g : ({x // ¬ isV x = true} → ℕ) → ℝ) :
    (∑' d : Index isV a b,
      f (fun x => d.val x) * g (fun x => d.val x)) /
      (((Fintype.card {x // isV x = true}).multichoose a : ℝ) *
        ((Fintype.card {x // ¬ isV x = true}).multichoose b : ℝ)) =
      ((∑' v : Composition {x // isV x = true} a, f v.val) /
        ((Fintype.card {x // isV x = true}).multichoose a : ℝ)) *
      ((∑' u : Composition {x // ¬ isV x = true} b, g u.val) /
        ((Fintype.card {x // ¬ isV x = true}).multichoose b : ℝ)) := by
…

Mentions: OAI.Problem335.BidegreeAverages.Index, OAI.Problem335.BidegreeAverages.Composition