OAI/Algebra/DepthFive/LocalProductAverage.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem335.LocalMoments.partitionCompositionMean_localProduct_le line 16

   Source documentation

   The actual occupation average of the full local four-path table is bounded by the product of its independent geometric local moments.

   theorem partitionCompositionMean_localProduct_le
       (side : σ → Bool) [Nonempty {i // side i = true}] [Nonempty {i // ¬ side i = true}]
       (a b : ℕ) (layers : Finset ι) (derivative : ι → Bool) (p q r : ι → σ)
       (hp : ∀ t ∈ layers, side (p t) = derivative t)
       (hq : ∀ t ∈ layers, side (q t) = derivative t)
       (hr : ∀ t ∈ layers, side (r t) = derivative t)
       (hdis : (layers : Set ι).Pairwise fun i j =>
         Disjoint ({p i, q i, r i} : Finset σ) {p j, q j, r j}) :
       partitionCompositionMean side
         (fun M => ∏ t ∈ layers, localPolynomial (derivative t) M (p t) (q t) (r t)) a b ≤
         ∏ t ∈ layers, localGeometricMass (derivative t)
           (if derivative t = true then (a : ℝ) / Fintype.card {i // side i = true}
   …

   Mentions: OAI.Problem335.partitionCompositionMean, OAI.Problem335.LocalMoments.localPolynomial, OAI.Problem335.LocalMoments.localGeometricMass

2. theorem OAI.Problem335.LocalMoments.partitionCompositionMean_layered_localProduct_le line 48

   Source documentation

   Specialization to the matrix-layer coordinate shape: disjoint supports and the common local mean are automatic, not additional analytic assumptions.

   theorem partitionCompositionMean_layered_localProduct_le
       {κ : Type*} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ]
       (derivative : ι → Bool)
       [Nonempty {x : ι × κ // derivative x.1 = true}]
       [Nonempty {x : ι × κ // ¬ derivative x.1 = true}]
       (a b : ℕ) (layers : Finset ι) (p q r : ι → κ) :
       partitionCompositionMean (fun x : ι × κ => derivative x.1)
         (fun M => ∏ t ∈ layers, localPolynomial (derivative t) M
           (t, p t) (t, q t) (t, r t)) a b ≤
         ∏ t ∈ layers, localGeometricMass (derivative t)
           (if derivative t = true then
             (a : ℝ) / Fintype.card {x : ι × κ // derivative x.1 = true}
   …

   Mentions: OAI.Problem335.partitionCompositionMean, OAI.Problem335.LocalMoments.localPolynomial, OAI.Problem335.LocalMoments.localGeometricMass

3. theorem OAI.Problem335.LocalMoments.localPolynomial_layered line 70

   Source documentation

   Coordinate-form conversion to the local table used in the four-path identity.

   @[simp] theorem localPolynomial_layered {κ : Type*} [DecidableEq ι] [DecidableEq κ]
       (d : Bool) (M : ι × κ → ℕ) (t : ι) (p q r : κ) :
       localPolynomial d M (t, p) (t, q) (t, r) =
         localPolynomial d (fun x => M (t, x)) p q r := by
   …

   Mentions: OAI.Problem335.LocalMoments.localPolynomial

4. theorem OAI.Problem335.LocalMoments.localGeometricMass_layered line 76
5. theorem OAI.Problem335.LocalMoments.partitionCompositionMean_layered_restrict_le line 82

   Source documentation

   Row-restriction presentation matching the actual four-path local table directly.

   theorem partitionCompositionMean_layered_restrict_le
       {κ : Type*} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ]
       (derivative : ι → Bool)
       [Nonempty {x : ι × κ // derivative x.1 = true}]
       [Nonempty {x : ι × κ // ¬ derivative x.1 = true}]
       (a b : ℕ) (layers : Finset ι) (p q r : ι → κ) :
       partitionCompositionMean (fun x : ι × κ => derivative x.1)
         (fun M => ∏ t ∈ layers, localPolynomial (derivative t) (fun x => M (t, x))
           (p t) (q t) (r t)) a b ≤
         ∏ t ∈ layers, localGeometricMass (derivative t)
           (if derivative t = true then
             (a : ℝ) / Fintype.card {x : ι × κ // derivative x.1 = true}
   …

   Mentions: OAI.Problem335.partitionCompositionMean, OAI.Problem335.LocalMoments.localPolynomial, OAI.Problem335.LocalMoments.localGeometricMass