BidegreeLocalProductAverage.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.bidegree_average_eq_partitionCompositionMean line 11

theorem OAI.Problem335.LocalMoments.bidegree_average_layered_localProduct_le line 26

Source documentation

The second-moment occupation estimate on the actual canonical source exponent subtype, presented in the same local coordinates as the four paths.

theorem bidegree_average_layered_localProduct_le
    {ι κ : Type*} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ]
    (derivative : ι → Bool)
    [Nonempty {x : ι × κ // derivative x.1 = true}]
    [Nonempty {x : ι × κ // ¬ derivative x.1 = true}]
    (a b : ℕ)
    [Fintype {d : (ι × κ) →₀ ℕ //
      Finsupp.weight (bidegreeWeight (fun x => derivative x.1)) d = (a, b)}]
    (layers : Finset ι) (p q r : ι → κ) :
    (∑ d : {d : (ι × κ) →₀ ℕ //
        Finsupp.weight (bidegreeWeight (fun x => derivative x.1)) d = (a, b)},
      ∏ t ∈ layers, localPolynomial (derivative t) (fun x => d.val (t, x))
…

Mentions: OAI.Problem335.bidegreeWeight, OAI.Problem335.LocalMoments.localPolynomial