OAI/Algebra/DepthFive/PairingOccupationAverage.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem335.MomentPairing.layerMeanV line 14
2. def OAI.Problem335.MomentPairing.layerMeanU line 18
3. def OAI.Problem335.MomentPairing.occupationPathMean line 22
4. theorem OAI.Problem335.MomentPairing.occupationPathMean_le_geometric line 32

   Source documentation

   The true two-group uniform average is bounded by the geometric local table. Both variable groups are nonempty; no moment hypothesis is assumed.

   theorem occupationPathMean_le_geometric {γ : Type*} [Fintype γ] [DecidableEq γ]
       {L : ℕ} (side : Fin (L + 1) → Bool)
       [Nonempty {v : Fin (L + 1) × (γ × γ) // side v.1 = true}]
       [Nonempty {v : Fin (L + 1) × (γ × γ) // ¬ side v.1 = true}]
       (a b : ℕ) (endpoint : γ) (x : Fin L → Labels γ) :
       occupationPathMean side a b endpoint x ≤
         pathGeometricMoment side (layerMeanV γ side a) (layerMeanU γ side b)
           endpoint (classifyWord endpoint x) x := by
   …

   Mentions: OAI.Problem335.MomentPairing.occupationPathMean, OAI.Problem335.MomentPairing.pathGeometricMoment, OAI.Problem335.MomentPairing.layerMeanV, OAI.Problem335.MomentPairing.layerMeanU, OAI.Problem335.MomentPairing.classifyWord

5. theorem OAI.Problem335.MomentPairing.sum_occupationPathMean_le line 48

   Source documentation

   Actual occupation averaging, normalizing, and relaxing the four-path classes combine without a residual analytic comparison hypothesis.

   theorem sum_occupationPathMean_le {γ : Type*} [Fintype γ] [DecidableEq γ]
       {L : ℕ} (side : Fin (L + 1) → Bool)
       [Nonempty {v : Fin (L + 1) × (γ × γ) // side v.1 = true}]
       [Nonempty {v : Fin (L + 1) × (γ × γ) // ¬ side v.1 = true}]
       (a b : ℕ) (ha : 0 < a) (endpoint : γ) :
       (∑ x : {x : Fin L → Labels γ // Compatible endpoint x},
         occupationPathMean side a b endpoint x.1) ≤
       pathMean side (layerMeanV γ side a) (layerMeanU γ side b) ^ 2 *
         ∑ τ : Fin (L + 1) → Kind, ∑ x : RelaxedPaths γ endpoint τ,
           pathWeight side
             (layerMeanV γ side a / (layerMeanV γ side a + 1))
             (layerMeanU γ side b / (layerMeanU γ side b + 1)) endpoint τ x.1 := by
   …

   Mentions: OAI.Problem335.MomentPairing.Compatible, OAI.Problem335.MomentPairing.occupationPathMean, OAI.Problem335.MomentPairing.pathMean, OAI.Problem335.MomentPairing.layerMeanV, OAI.Problem335.MomentPairing.layerMeanU, OAI.Problem335.MomentPairing.pathWeight