OAI/Algebra/DepthFive/CompositionAntidiag.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem335.BidegreeAverages.compositionAntidiagEquiv line 13

   Source documentation

   The function representation of a weak composition and the finite finsuppAntidiag representation used by occupation moments agree coordinatewise.

   def compositionAntidiagEquiv (σ : Type*) [Fintype σ] [DecidableEq σ] (a : ℕ) :
       Composition σ a ≃ (Finset.finsuppAntidiag (Finset.univ : Finset σ) a) := by
   …

   Mentions: OAI.Problem335.BidegreeAverages.Composition

2. theorem OAI.Problem335.BidegreeAverages.compositionAntidiagEquiv_apply line 20
3. theorem OAI.Problem335.BidegreeAverages.sum_compositions_eq_antidiag line 25

   Source documentation

   Convert a sum over function compositions to the canonical occupation finset.

   theorem sum_compositions_eq_antidiag {σ : Type*} [Fintype σ] [DecidableEq σ]
       (a : ℕ) (f : (σ → ℕ) → ℝ) :
       (∑' d : Composition σ a, f d.val) =
         ∑ M ∈ Finset.finsuppAntidiag (Finset.univ : Finset σ) a, f M := by
   …

   Mentions: OAI.Problem335.BidegreeAverages.Composition

4. theorem OAI.Problem335.BidegreeAverages.card_compositions_eq_antidiag line 37

   Source documentation

   Denominator conversion for the same index equivalence.

   theorem card_compositions_eq_antidiag {σ : Type*} [Fintype σ] [DecidableEq σ]
       (a : ℕ) :
       Nat.card (Composition σ a) =
         (Finset.finsuppAntidiag (Finset.univ : Finset σ) a).card := by
   …

   Mentions: OAI.Problem335.BidegreeAverages.Composition

5. theorem OAI.Problem335.BidegreeAverages.composition_average_eq_occupationAverage line 45

   Source documentation

   The function-composition average is exactly the canonical occupation average.

   theorem composition_average_eq_occupationAverage {σ : Type*}
       [Fintype σ] [DecidableEq σ] (a : ℕ) (f : (σ → ℕ) → ℝ) :
       (∑' d : Composition σ a, f d.val) / (Nat.card (Composition σ a) : ℝ) =
         occupationAverage a (fun M : σ →₀ ℕ => f M) := by
   …

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

6. theorem OAI.Problem335.BidegreeAverages.bidegree_average_eq_occupationAverage line 55

   Source documentation

   The actual bidegree-domain average, expressed directly using the canonical occupation-average API. This bridges the Fock/matrix source indices and both first- and second-moment inequalities.

   theorem bidegree_average_eq_occupationAverage {σ : Type*} [Fintype σ] [DecidableEq σ]
       (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) : ℝ) =
         occupationAverage a (fun M : {x // isV x = true} →₀ ℕ => f M) *
           occupationAverage b (fun M : {x // ¬ isV x = true} →₀ ℕ => g M) := by
   …

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

7. theorem OAI.Problem335.BidegreeAverages.bidegree_average_eq_occupationAverage_fintype line 69

   Source documentation

   Matrix-indexed finite-sum version of the bridge.

   theorem bidegree_average_eq_occupationAverage_fintype {σ : Type*}
       [Fintype σ] [DecidableEq σ] (isV : σ → Bool) (a b : ℕ)
       [Fintype (Index isV 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 (Index isV a b) : ℝ) =
         occupationAverage a (fun M : {x // isV x = true} →₀ ℕ => f M) *
           occupationAverage b (fun M : {x // ¬ isV x = true} →₀ ℕ => g M) := by
   …

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

8. theorem OAI.Problem335.BidegreeAverages.bidegree_first_moment_lower line 84

   Source documentation

   The first occupation-moment lower estimate on the ACTUAL bidegree exponent source, rather than on an auxiliary Cartesian product of composition finsets.

   theorem bidegree_first_moment_lower {σ : Type*} [Fintype σ] [DecidableEq σ]
       (isV : σ → Bool) (a b : ℕ)
       [Fintype (Index isV a b)]
       [Nonempty {x // isV x = true}] [Nonempty {x // ¬ isV x = true}]
       (s : Finset {x // isV x = true}) (z : Finset {x // ¬ isV x = true})
       (ha : 0 < a) (hb : 0 < b) (hs : 2 * s.card ≤ a) (hz : 2 * z.card ≤ b) :
       Real.exp ((-(s.card : ℝ) ^ 2 / a -
           (s.card : ℝ) ^ 2 / (2 * Fintype.card {x // isV x = true})) +
         (-(z.card : ℝ) ^ 2 / b -
           (z.card : ℝ) ^ 2 / (2 * Fintype.card {x // ¬ isV x = true}))) *
         (((a : ℝ) / Fintype.card {x // isV x = true}) ^ s.card *
           (1 + (b : ℝ) / Fintype.card {x // ¬ isV x = true}) ^ z.card) ≤
   …

   Mentions: OAI.Problem335.BidegreeAverages.Index