OAI/Combinatorics/PlanarL1/Gluing.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanarL1.Gluing.frontier_between_right line 12
2. lemma OAI.PlanarL1.Gluing.frontier_between_left line 34
3. lemma OAI.PlanarL1.Gluing.monotone_piecewise line 56
4. lemma OAI.PlanarL1.Gluing.lipschitz_piecewise line 74
5. def OAI.PlanarL1.Gluing.VerticalBound line 128

   Source documentation

   The upper-bound invariant on a set of heights, stated on differences because individual half-line indicators need not be integrable.

   def VerticalBound (μ : Measure Ω) (f : ℝ → Ω → ℝ) (S : Set ℝ) : Prop :=
   …

6. lemma OAI.PlanarL1.Gluing.difference_triangle line 132
7. lemma OAI.PlanarL1.Gluing.verticalBound_piecewise line 150
8. structure OAI.PlanarL1.Columns.Model.SetPatch line 205

   Source documentation

   Local update data on closed full-column pieces. Cross-domain switches must be unchanged, as ensured by the strict frontier margins in the source.

   structure SetPatch (A : SetSystem M Ω μ) where
   …

   Mentions: OAI.PlanarL1.Columns.Model.SetSystem

9. def OAI.PlanarL1.Columns.Model.SetPatch.patchedActivity line 222
10. lemma OAI.PlanarL1.Columns.Model.SetPatch.indicator_eq line 242
11. lemma OAI.PlanarL1.Columns.Model.SetPatch.verticalBound line 249
12. def OAI.PlanarL1.Columns.Model.SetPatch.apply line 266
13. lemma OAI.PlanarL1.Columns.Model.SetPatch.unchanged line 276
14. lemma OAI.PlanarL1.Columns.Model.SetPatch.inside line 280
15. lemma OAI.PlanarL1.Threshold.active_verticalBound line 294
16. def OAI.PlanarL1.Threshold.chartPatch line 307

    Source documentation

    A literal common-label scalar chart replacement yields local patch data. P already contains the source κ and comparison-orientation factors.

    noncomputable def chartPatch {n : ℕ} {M : Columns.Model n}
        (A : M.SetSystem Ω μ) (Z : Variables Ω μ) (D : Fin n → Set ℝ)
        (hD : ∀ i, IsClosed (D i)) (P : Fin n → ℝ → ℝ)
        (hP : ∀ i, LipschitzOnWith 1 (P i) (D i))
        (hb : ∀ ω i H, H ∈ frontier (D i) →
          (active Z H (P i H) ω ↔ (A.activity ω).active i H))
        (hs : ∀ i j H, H ∈ M.heights i j → H ∈ D i → H ∈ D j → P i H = P j H)
        (hc : ∀ ω i j H, H ∈ M.heights i j → H ∈ D i → H ∉ D j →
          (active Z H (P i H) ω ↔ (A.activity ω).active i H)) : Columns.Model.SetPatch A where
    …

    Mentions: OAI.PlanarL1.Columns.Model, OAI.PlanarL1.Threshold.Variables, OAI.PlanarL1.Threshold.active, OAI.PlanarL1.Columns.Model.SetPatch

17. lemma OAI.PlanarL1.Columns.Model.Activity.indicator_mono line 338
18. def OAI.PlanarL1.Columns.Model.SetSystem.balancedUpdate line 348

    Source documentation

    Balanced changes of one-point marginals preserve the exact vertical bound once genuine nestedness has been established. This avoids an unjustified finite-boundary assumption on chart regions.

    noncomputable def SetSystem.balancedUpdate (S : SetSystem M Ω μ) (A : Ω → Activity M)
        (hm : ∀ i H, MeasurableSet {ω | (A ω).active i H})
        (hi : ∀ i H, Integrable (fun ω => (A ω).indicator i H-(S.activity ω).indicator i H) μ)
        (hz : ∀ i H, (∫ ω, (A ω).indicator i H-(S.activity ω).indicator i H ∂μ)=0) :
        SetSystem M Ω μ := by
    …

    Mentions: OAI.PlanarL1.Columns.Model.SetSystem, OAI.PlanarL1.Columns.Model.Activity

19. def OAI.PlanarL1.Columns.Model.SetPatch.rebase line 407

    Source documentation

    A patch can be installed after other patches which have not changed its closed domain. Its actual activity and all clipping data are retained.

    def rebase (P : SetPatch A) (B : SetSystem M Ω μ)
        (hB : ∀ ω i H, H ∈ P.domain i → ((B.activity ω).active i H ↔ (A.activity ω).active i H)) :
        SetPatch B where
    …

    Mentions: OAI.PlanarL1.Columns.Model.SetPatch, OAI.PlanarL1.Columns.Model.SetSystem

20. def OAI.PlanarL1.Columns.Model.SetPatch.UnchangedOverlap line 421
21. def OAI.PlanarL1.Columns.Model.SetPatch.selectActive line 428

    Source documentation

    The deterministic tie rule chooses the first closed cell containing a point. On all main-cell overlaps every proposal is the original activity.

    noncomputable def selectActive : List (SetPatch A) → Ω → Fin n → ℝ → Prop
      | [],ω,i,H => (A.activity ω).active i H
      | P::L,ω,i,H => if H ∈ P.domain i then P.active ω i H else selectActive L ω i H

    Mentions: OAI.PlanarL1.Columns.Model.SetPatch

22. lemma OAI.PlanarL1.Columns.Model.SetPatch.selectActive_old line 432
23. lemma OAI.PlanarL1.Columns.Model.SetPatch.exists_batch line 443
24. def OAI.PlanarL1.Columns.Model.SetPatch.batch line 460
25. lemma OAI.PlanarL1.Columns.Model.SetPatch.batch_active line 463
26. lemma OAI.PlanarL1.Columns.Model.SetPatch.selectActive_choice line 467
27. lemma OAI.PlanarL1.Columns.Model.SetPatch.batch_movement line 489

    Source documentation

    Simultaneous disjoint main clipping has the one-patch movement bound, not the sum over cells. Covers all points, not just the listed vertices.

    lemma batch_movement (L : List (SetPatch A)) (hL : L.Pairwise UnchangedOverlap)
        {b : ℝ} (hb : 0 ≤ b)
        (hp : ∀ P ∈ L, ∀ i H, (∫ ω, |(P.apply.activity ω).indicator i H-(A.activity ω).indicator i H| ∂μ) ≤ b)
        (i : Fin n) (H : ℝ) :
        (∫ ω, |((batch L hL).activity ω).indicator i H-(A.activity ω).indicator i H| ∂μ) ≤ b := by
    …

    Mentions: OAI.PlanarL1.Columns.Model.SetPatch, OAI.PlanarL1.Columns.Model.SetPatch.UnchangedOverlap, OAI.PlanarL1.Columns.Model.SetPatch.batch

28. lemma OAI.PlanarL1.Columns.Model.SetPatch.batch_movement_integrable line 508
29. lemma OAI.PlanarL1.Columns.Model.SetPatch.selectActive_inside line 536
30. lemma OAI.PlanarL1.Columns.Model.SetPatch.batch_inside line 551
31. lemma OAI.PlanarL1.Columns.Model.SetPatch.batch_old line 557