OAI/Probability/CoordinateSweeps/Induction.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoordinateSweeps.Grid.Holes.onLine_row_iff line 38
2. lemma OAI.CoordinateSweeps.Grid.Holes.onLine_column_iff line 57
3. def OAI.CoordinateSweeps.Grid.Holes.rowOnLineEquiv line 76
4. def OAI.CoordinateSweeps.Grid.Holes.columnOnLineEquiv line 94
5. lemma OAI.CoordinateSweeps.Grid.Holes.lineCount_row line 112
6. lemma OAI.CoordinateSweeps.Grid.Holes.lineCount_column line 116
7. lemma OAI.CoordinateSweeps.Grid.Holes.cost_stage_row line 122

   Source comment

   One head stage contributes exactly the sum of its child row potentials.

   lemma cost_stage_row (j : Fin A.b) :
       (∑ L : (concat A B).Line (Fin.castAdd B.b j),
         Real.log (((2 ^ (concat A B).bits (Fin.castAdd B.b j) : ℕ) : ℝ) ^
             H.lineCount (Fin.castAdd B.b j) L /
           ((2 ^ (concat A B).bits (Fin.castAdd B.b j)).descFactorial
             (H.lineCount (Fin.castAdd B.b j) L) : ℝ)))=
         ∑ y : B.Slot, ∑ L : A.Line j,
           Real.log (((2^A.bits j : ℕ) : ℝ)^(H.rowHoles y).lineCount j L /
             ((2^A.bits j).descFactorial ((H.rowHoles y).lineCount j L) : ℝ)) := by
   …

   Mentions: OAI.CoordinateSweeps.Grid.concat, OAI.CoordinateSweeps.Grid.Line, OAI.CoordinateSweeps.Grid.Holes.lineCount

8. lemma OAI.CoordinateSweeps.Grid.Holes.cost_stage_column line 138
9. theorem OAI.CoordinateSweeps.Grid.Holes.cost_split line 155

   Source comment

   No conditioning cost is discarded in the induction split.

   theorem cost_split : H.cost=(∑ y, (H.rowHoles y).cost)+(∑ x, (H.columnHoles x).cost) := by
   …

   Mentions: OAI.CoordinateSweeps.Grid.Holes.cost

10. lemma OAI.CoordinateSweeps.Grid.Holes.row_column_index_injective line 184
11. lemma OAI.CoordinateSweeps.Grid.Holes.row_entropy_sum line 191
12. lemma OAI.CoordinateSweeps.Grid.Holes.column_entropy_sum line 205
13. theorem OAI.CoordinateSweeps.Grid.Holes.row_child_hook_bound line 221
14. theorem OAI.CoordinateSweeps.Grid.Holes.column_child_hook_bound line 243
15. theorem OAI.CoordinateSweeps.Grid.Holes.grid_projected_hook_bound line 267

    Source comment

    Exact row/column induction estimate on the literal free junction board. Only smaller-grid conditional estimates enter as hypotheses.

    theorem grid_projected_hook_bound (p : ℕ) (hp : 0 < p)
        (eF : Fin (Fintype.card H.JunctionFree) ≃ H.JunctionFree) (hf : H.Feasible)
        (z : ℝ) (q : ℕ) (hq : 0 < q) (c e : ℝ) (hc : 0 ≤ c) (hcq : c ≤ q)
        (s : ℕ) (hpS : p ≤ s) (hAS : A.size ≤ s) (hBS : B.size ≤ s)
        (ρ : UnitaryIrrep (Equiv.Perm (Fin (Fintype.card H.JunctionFree))))
        (hR : ∀ y : B.Slot, ∀ σ : UnitaryIrrep (H.rowHoles y).stabilizer,
          schattenMoment q ((H.rowHoles y).conditionalAverage (H.rowHoles y).feasible_of_disjoint z σ) ≤
            Real.exp (-c*Real.log σ.dimension+e*H.rowCount y*Real.log A.size-(H.rowHoles y).cost))
        (hC : ∀ x : A.Slot, ∀ σ : UnitaryIrrep (H.columnHoles x).stabilizer,
          schattenMoment q ((H.columnHoles x).conditionalAverage (H.columnHoles x).feasible_of_disjoint z σ) ≤
            Real.exp (-c*Real.log σ.dimension+e*H.columnCount x*Real.log B.size-(H.columnHoles x).cost)) :
        let X := H.rowAverage hf z (H.junctionTensorAction p eF)
    …

    Mentions: OAI.CoordinateSweeps.c, OAI.CoordinateSweeps.e, OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.Grid.Holes.stabilizer, OAI.CoordinateSweeps.schattenMoment, OAI.CoordinateSweeps.Grid.Holes.conditionalAverage, OAI.CoordinateSweeps.Grid.Holes.feasible_of_disjoint, OAI.CoordinateSweeps.Grid.Holes.cost

16. def OAI.CoordinateSweeps.Grid.Holes.junctionChart line 318
17. lemma OAI.CoordinateSweeps.Grid.Holes.junction_projector_commute_column line 322
18. theorem OAI.CoordinateSweeps.Grid.Holes.junction_projected_moment line 333

    Source comment

    The exact projected tensor moment on the literal junction board equals its genuine Hom multiplicity times the main theorem's conditional moment.

    theorem junction_projected_moment (p : ℕ) (hf : H.Feasible)
        (e : Fin (Fintype.card H.JunctionFree) ≃ H.JunctionFree) (z : ℝ)
        (ρ : UnitaryIrrep (Equiv.Perm (Fin (Fintype.card H.JunctionFree)))) {q : ℕ} (hq : q ≠ 0) :
        let X := H.rowAverage hf z (H.junctionTensorAction p e)
    …

    Mentions: OAI.CoordinateSweeps.e, OAI.CoordinateSweeps.UnitaryIrrep

19. theorem OAI.CoordinateSweeps.Grid.Holes.conditional_hook_moment_le_projected line 368

    Source comment

    Hook occurrence removes the multiplicity without normalizing the trace.

    theorem conditional_hook_moment_le_projected (p : ℕ) (hf : H.Feasible)
        (e : Fin (Fintype.card H.JunctionFree) ≃ H.JunctionFree) (z : ℝ)
        (ρ : UnitaryIrrep (Equiv.Perm (Fin (Fintype.card H.JunctionFree)))) {q : ℕ} (hq : q ≠ 0)
        (μ : YoungDiagram) (t : Fin (Fintype.card H.JunctionFree) ≃ Boxes μ)
        (hρ : hasShape μ t ρ.asRepresentation) (hhook : Hook μ p) :
        schattenMoment q (H.conditionalAverage hf z (ρ.pullback (H.junctionChart hf e))) ≤
          (Matrix.trace (((H.columnAverage hf z (H.junctionTensorAction p e)*
            ρ.projector (action p _)*H.rowAverage hf z (H.junctionTensorAction p e)).conjTranspose*
            (H.columnAverage hf z (H.junctionTensorAction p e)*
            ρ.projector (action p _)*H.rowAverage hf z (H.junctionTensorAction p e)))^q)).re := by
    …

    Mentions: OAI.CoordinateSweeps.e, OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.schattenMoment

20. theorem OAI.CoordinateSweeps.Grid.Holes.grid_conditional_hook_bound line 389