OAI/Algebra/DepthFive/RelaxedWeightBound.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem335.MomentPairing.normalVLayers line 14

   Source documentation

   Normal pairing layers belonging to the derivative-variable group.

   def normalVLayers {L : ℕ} (isV : Fin (L + 1) → Bool)
       (τ : Fin (L + 1) → Kind) : Finset (Fin (L + 1)) :=
   …

2. def OAI.Problem335.MomentPairing.diagonalVCount line 18
3. def OAI.Problem335.MomentPairing.diagonalUCount line 22
4. def OAI.Problem335.MomentPairing.uLayerCount line 26
5. def OAI.Problem335.MomentPairing.normalVCorrection line 30

   Source documentation

   The V correction before averaging the path labels.

   def normalVCorrection {γ : Type*} [DecidableEq γ] {L : ℕ} (isV : Fin (L + 1) → Bool)
       (α : ℝ) (endpoint : γ) (τ : Fin (L + 1) → Kind)
       (x : Fin L → Labels γ) : ℝ :=
   …

6. theorem OAI.Problem335.MomentPairing.pathWeight_le_extracted line 37

   Source documentation

   Extract all diagonal weights and bound each U coincidence factor by 1+β.

   theorem pathWeight_le_extracted {γ : Type*} [DecidableEq γ] {L : ℕ}
       (isV : Fin (L + 1) → Bool) {α β : ℝ} (hα : 0 ≤ α) (hβ : 0 ≤ β)
       (endpoint : γ) (τ : Fin (L + 1) → Kind) (x : Fin L → Labels γ) :
       pathWeight isV α β endpoint τ x ≤
         α⁻¹ ^ diagonalVCount isV τ * β ^ diagonalUCount isV τ *
           (1 + β) ^ uLayerCount isV * normalVCorrection isV α endpoint τ x := by
   …

   Mentions: OAI.Problem335.MomentPairing.pathWeight, OAI.Problem335.MomentPairing.diagonalVCount, OAI.Problem335.MomentPairing.diagonalUCount, OAI.Problem335.MomentPairing.uLayerCount, OAI.Problem335.MomentPairing.normalVCorrection

7. theorem OAI.Problem335.MomentPairing.sum_relaxed_pathWeight_le line 83

   Source documentation

   The full weighted relaxed-quadruple bound used in the second trace.

   theorem sum_relaxed_pathWeight_le {γ : Type*} [Fintype γ] [DecidableEq γ]
       [Nonempty γ] {L : ℕ} (isV : Fin (L + 1) → Bool)
       {α β : ℝ} (hα : 0 ≤ α) (hβ : 0 ≤ β) (endpoint : γ)
       (τ : Fin (L + 1) → Kind)
       (hs : Pairwise (fun t u : normalVLayers isV τ =>
         Disjoint (internalEndpointSet t.1) (internalEndpointSet u.1))) :
       (∑ x : RelaxedPaths γ endpoint τ, pathWeight isV α β endpoint τ x.1) ≤
         α⁻¹ ^ diagonalVCount isV τ * β ^ diagonalUCount isV τ *
           (1 + β) ^ uLayerCount isV *
           ((Fintype.card γ : ℝ) ^ (2 * L - adjacentSwitches τ) *
             ∏ t : normalVLayers isV τ,
               (1 + α⁻¹ * (Fintype.card γ : ℝ)⁻¹ ^
   …

   Mentions: OAI.Problem335.MomentPairing.normalVLayers, OAI.Problem335.MomentPairing.pathWeight, OAI.Problem335.MomentPairing.diagonalVCount, OAI.Problem335.MomentPairing.diagonalUCount, OAI.Problem335.MomentPairing.uLayerCount

8. def OAI.Problem335.MomentPairing.relaxedWordWeight line 111

   Source documentation

   The normalized pairing-word summand in the second-moment reduction.

   def relaxedWordWeight {L : ℕ} (isV : Fin (L + 1) → Bool)
       (N α β : ℝ) (τ : Fin (L + 1) → Kind) : ℝ :=
   …

9. theorem OAI.Problem335.MomentPairing.assignmentPower_eq_normalized line 118

   Source documentation

   Separate the free two-path count from the switch penalty.

   theorem assignmentPower_eq_normalized {L : ℕ} (τ : Fin (L + 1) → Kind)
       {N : ℝ} (hN : N ≠ 0) :
       N ^ (2 * L - adjacentSwitches τ) = N ^ (2 * L) * N⁻¹ ^ adjacentSwitches τ := by
   …

10. theorem OAI.Problem335.MomentPairing.sum_relaxed_pathWeight_le_wordSum line 132

    Source documentation

    Full combinatorial moment reduction, summed over all pairing words.

    theorem sum_relaxed_pathWeight_le_wordSum {γ : Type*} [Fintype γ] [DecidableEq γ]
        [Nonempty γ] {L : ℕ} (isV : Fin (L + 1) → Bool)
        {α β : ℝ} (hα : 0 ≤ α) (hβ : 0 ≤ β) (endpoint : γ)
        (hs : ∀ τ : Fin (L + 1) → Kind,
          Pairwise (fun t u : normalVLayers isV τ =>
            Disjoint (internalEndpointSet t.1) (internalEndpointSet u.1))) :
        (∑ τ : Fin (L + 1) → Kind, ∑ x : RelaxedPaths γ endpoint τ,
          pathWeight isV α β endpoint τ x.1) ≤
          (1 + β) ^ uLayerCount isV * (Fintype.card γ : ℝ) ^ (2 * L) *
            ∑ τ : Fin (L + 1) → Kind, relaxedWordWeight isV (Fintype.card γ) α β τ := by
    …

    Mentions: OAI.Problem335.MomentPairing.normalVLayers, OAI.Problem335.MomentPairing.pathWeight, OAI.Problem335.MomentPairing.uLayerCount, OAI.Problem335.MomentPairing.relaxedWordWeight

11. theorem OAI.Problem335.MomentPairing.sum_relaxedWordWeight_eq_bool line 157

    Source documentation

    Reindex all pairing words using the canonical false-normal, true-diagonal encoding.

    theorem sum_relaxedWordWeight_eq_bool {L : ℕ} (isV : Fin (L + 1) → Bool)
        (N α β : ℝ) :
        (∑ τ : Fin (L + 1) → Kind, relaxedWordWeight isV N α β τ) =
          ∑ w : Fin (L + 1) → Bool,
            relaxedWordWeight isV N α β (fun t => boolKindEquiv (w t)) := by
    …

    Mentions: OAI.Problem335.MomentPairing.relaxedWordWeight

12. theorem OAI.Problem335.MomentPairing.sum_relaxed_pathWeight_le_of_boolWordSum line 166

    Source documentation

    Consume a Boolean-word estimate after the full relaxed-path averaging.

    theorem sum_relaxed_pathWeight_le_of_boolWordSum {γ : Type*} [Fintype γ]
        [DecidableEq γ] [Nonempty γ] {L : ℕ} (isV : Fin (L + 1) → Bool)
        {α β B : ℝ} (hα : 0 ≤ α) (hβ : 0 ≤ β) (endpoint : γ)
        (hs : ∀ τ : Fin (L + 1) → Kind,
          Pairwise (fun t u : normalVLayers isV τ =>
            Disjoint (internalEndpointSet t.1) (internalEndpointSet u.1)))
        (hword : (∑ w : Fin (L + 1) → Bool,
          relaxedWordWeight isV (Fintype.card γ) α β (fun t => boolKindEquiv (w t))) ≤ B) :
        (∑ τ : Fin (L + 1) → Kind, ∑ x : RelaxedPaths γ endpoint τ,
          pathWeight isV α β endpoint τ x.1) ≤
          (1 + β) ^ uLayerCount isV * (Fintype.card γ : ℝ) ^ (2 * L) * B := by
    …

    Mentions: OAI.Problem335.MomentPairing.normalVLayers, OAI.Problem335.MomentPairing.relaxedWordWeight, OAI.Problem335.MomentPairing.pathWeight, OAI.Problem335.MomentPairing.uLayerCount