OAI/Combinatorics/PlanarL1/MainGain.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanarL1.Columns.Model.MainFamily.unique_at_padded line 15
2. lemma OAI.PlanarL1.Columns.Model.MainFamily.batch_inside_kept line 26
3. lemma OAI.PlanarL1.Columns.Model.MainFamily.batch_old_suppressed line 37
4. lemma OAI.PlanarL1.FiniteRandom.prob_second line 64
5. def OAI.PlanarL1.FiniteRandom.coinProduct line 72

   Source documentation

   Separate coins from all other finite independent local data, including when the local data type depends on the cell/group.

   def coinProduct {I : Type*} (D : I → Type*) :
       (∀ i, D i × Bool) ≃ (∀ i, D i) × (I → Bool) where
   …

6. lemma OAI.PlanarL1.FiniteRandom.prob_coinProduct line 78
7. abbrev OAI.PlanarL1.Columns.Model.MainFamily.Uncoined line 90
8. def OAI.PlanarL1.Columns.Model.MainFamily.restructure line 92
9. lemma OAI.PlanarL1.Columns.Model.MainFamily.prob_coins line 97
10. lemma OAI.PlanarL1.Columns.Model.MainFamily.prob_keep_suppress line 103
11. lemma OAI.PlanarL1.Columns.Model.MainFamily.batch_pair_kept_suppressed line 125
12. lemma OAI.PlanarL1.Columns.Model.MainFamily.padded_height line 146
13. lemma OAI.PlanarL1.Columns.Model.MainFamily.kept_shield line 156
14. lemma OAI.PlanarL1.Columns.Model.MainFamily.no_descent_gain line 183

    Source documentation

    A literal missing descent in an available padded cell produces the gain in the whole simultaneous main update on the keep/suppress coin event.

    lemma no_descent_gain (c d : CellIndex q L U phase) (hc : Available A S phase c)
        (x : M.Point (BandTrees.band broad (lower q L U c.1.1))
          (BandTrees.root M broad (lower q L U c.1.1) c.1.2))
        (ii : Fin (k+1)) (T : ℝ)
        (hx : x.column ∈ ColumnOrder.componentColumns c.2.2)
        (hy : T ∈ domain phase d ii)
        (hpx : Tiling.Padded a₁ q x.height (a₁/10)) (hpy : Tiling.Padded a₁ q T (a₁/10))
        (hr : BandTrees.RadialInterior D (phase c.1) x)
        (hn : S.name ii T=index A S phase c hc)
        (hT : T ∈ (S.chart (index A S phase c hc)).band)
        (hclose : |(S.chart (index A S phase c hc)).comparison.eval
            (x.widen (sub_old A S phase c hc))-
    …

    Mentions: OAI.PlanarL1.Columns.Model.MainFamily.CellIndex, OAI.PlanarL1.Columns.Model.MainFamily.Available, OAI.PlanarL1.Columns.Model.BandTrees.band, OAI.PlanarL1.Columns.Model.MainFamily.lower, OAI.PlanarL1.Columns.Model.BandTrees.root, OAI.PlanarL1.ColumnOrder.componentColumns, OAI.PlanarL1.Columns.Model.MainFamily.domain, OAI.PlanarL1.Tiling.Padded, OAI.PlanarL1.Columns.Model.BandTrees.RadialInterior, OAI.PlanarL1.Columns.Model.MainFamily.index, OAI.PlanarL1.Columns.Model.MainFamily.sub_old

15. lemma OAI.PlanarL1.Columns.Model.MainFamily.no_descent_probability line 240
16. def OAI.PlanarL1.Columns.Model.VertexBands.mainCell line 277
17. lemma OAI.PlanarL1.Columns.Model.VertexBands.mainCell_column line 281
18. lemma OAI.PlanarL1.Columns.Model.VertexBands.mainCell_mem line 284
19. lemma OAI.PlanarL1.Columns.Model.PairGeometry.main_available line 305
20. lemma OAI.PlanarL1.Columns.Model.PairGeometry.main_index line 307
21. lemma OAI.PlanarL1.Columns.Model.PairGeometry.comparison_coordinates line 310
22. lemma OAI.PlanarL1.Columns.Model.PairGeometry.no_descent_probability line 316