OAI/Combinatorics/PlanarL1/Threshold.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PlanarL1.Rebase.shear_strictMono line 12
  2. lemma OAI.PlanarL1.Rebase.shear_surjective line 21
  3. def OAI.PlanarL1.Rebase.shear line 44

    Source documentation

    The branch change of variable H ↦ H+ψ(H) is a genuine increasing bijection on the WHOLE real line, not just on the current chart heights.

    noncomputable def shear (hK : (K:ℝ) < 1) (hψ : LipschitzWith K ψ) : ℝ ≃o ℝ :=
…
  4. lemma OAI.PlanarL1.Rebase.shear_apply line 47
  5. def OAI.PlanarL1.Threshold.half line 57
  6. lemma OAI.PlanarL1.Threshold.measurable_half line 59
  7. lemma OAI.PlanarL1.Threshold.abs_sub_half_of_le line 62
  8. lemma OAI.PlanarL1.Threshold.abs_sub_half line 71
  9. lemma OAI.PlanarL1.Threshold.integrable_abs_sub_half line 78
  10. lemma OAI.PlanarL1.Threshold.integrable_sub_half line 84
  11. lemma OAI.PlanarL1.Threshold.integral_abs_sub_half line 88
  12. lemma OAI.PlanarL1.Threshold.two_sign_abs line 98

    Source documentation

    The elementary two-sign identity behind exact vertical control.

    lemma two_sign_abs (a b : ℝ) : (|a+b|+|a-b|)/2 = max |a| |b| := by
…
  13. def OAI.PlanarL1.Threshold.labelMeasure line 120

    Source documentation

    Lebesgue times a fair sign; its total mass is infinite, as in the source.

    noncomputable def labelMeasure : Measure (Bool × ℝ) :=
…
  14. def OAI.PlanarL1.Threshold.chartValue line 123
  15. lemma OAI.PlanarL1.Threshold.measurable_chartValue line 126
  16. lemma OAI.PlanarL1.Threshold.integrable_chart_difference_count line 132
  17. lemma OAI.PlanarL1.Threshold.integrable_chart_difference line 144
  18. lemma OAI.PlanarL1.Threshold.chart_distance line 149
  19. lemma OAI.PlanarL1.Threshold.chart_vertical line 165
  20. lemma OAI.PlanarL1.Threshold.chart_movement line 169
  21. def OAI.PlanarL1.Threshold.rebase line 173
  22. lemma OAI.PlanarL1.Threshold.measurable_rebase line 176
  23. lemma OAI.PlanarL1.Threshold.rebase_preimage_Ioc line 181
  24. lemma OAI.PlanarL1.Threshold.rebase_preserving line 190

    Source documentation

    Rebasing is measure preserving AFTER averaging the old sign. It does not claim that either conditional change of variable preserves Lebesgue measure.

    lemma rebase_preserving (ep em : ℝ ≃o ℝ) (hmean : ∀ H, ep H+em H = 2*H) :
    MeasurePreserving (rebase ep em) labelMeasure volume := by
…

    Mentions: OAI.PlanarL1.Threshold.rebase, OAI.PlanarL1.Threshold.labelMeasure

  25. lemma OAI.PlanarL1.Threshold.rebase_membership line 212

    Source documentation

    Exact set equality, not merely equality in distribution.

    lemma rebase_membership (ep em : ℝ ≃o ℝ) (H : ℝ) (z : Bool × ℝ) :
    z.2 < (if z.1 then ep else em) H ↔ rebase ep em z < H := by
…

    Mentions: OAI.PlanarL1.Threshold.rebase

  26. lemma OAI.PlanarL1.Threshold.threshold_mono line 227
  27. def OAI.PlanarL1.Threshold.chartActivity line 239
  28. lemma OAI.PlanarL1.Threshold.chartIndicator line 251
  29. def OAI.PlanarL1.Threshold.chartSystem line 255
  30. def OAI.PlanarL1.Threshold.branchRebase line 277

    Source documentation

    Rebasing a genuine strict Lipschitz height branch, with no differentiability assumption. The old sign is averaged; its conditional laws are not asserted Lebesgue preserving.

    noncomputable def branchRebase {K : ℝ≥0} (hK : (K:ℝ) < 1) {ψ : ℝ → ℝ}
    (hψ : LipschitzWith K ψ) : Bool × ℝ → ℝ :=
…
  31. lemma OAI.PlanarL1.Threshold.branchRebase_preserving line 281
  32. lemma OAI.PlanarL1.Threshold.branchRebase_membership line 288
  33. def OAI.PlanarL1.Threshold.fair line 310
  34. instance OAI.PlanarL1.Threshold.fair_probability line 312
  35. lemma OAI.PlanarL1.Threshold.labelMeasure_eq line 317
  36. structure OAI.PlanarL1.Threshold.Variables line 322

    Source documentation

    A chart's actual label variables, not hypothetical independent coordinates. The preservation proof is exactly the joint Lebesgue/fair-sign invariant.

    structure Variables (Ω : Type*) [MeasurableSpace Ω] (μ : Measure Ω) where
…
  37. def OAI.PlanarL1.Threshold.Variables.initial line 329
  38. def OAI.PlanarL1.Threshold.Variables.lift line 332
  39. def OAI.PlanarL1.Threshold.Variables.rebase line 336
  40. lemma OAI.PlanarL1.Threshold.Variables.rebase_membership line 349
  41. lemma OAI.PlanarL1.Threshold.Variables.integrable_difference line 359
  42. lemma OAI.PlanarL1.Threshold.Variables.distance line 364
  43. def OAI.PlanarL1.Threshold.active line 388
  44. lemma OAI.PlanarL1.Threshold.active_indicator line 391
  45. lemma OAI.PlanarL1.Threshold.measurable_active line 394
  46. lemma OAI.PlanarL1.Threshold.active_increasing line 400
  47. lemma OAI.PlanarL1.Threshold.Variables.active_rebase line 420
  48. lemma OAI.PlanarL1.Threshold.half_mono line 440
  49. lemma OAI.PlanarL1.Threshold.integral_sub_half line 446
  50. lemma OAI.PlanarL1.Threshold.integral_chart_difference line 457
  51. lemma OAI.PlanarL1.Threshold.Variables.integral_difference line 472
  52. lemma OAI.PlanarL1.Threshold.threshold_compare line 490
  53. lemma OAI.PlanarL1.Threshold.named_nested line 501

    Source documentation

    A genuine gluing lemma for regions with arbitrarily complicated boundaries. Small distance-tapered changes preserve nesting even though the identifiers may have infinitely many changes along a column. All fields below already include κ. No regularity of the name function is assumed.

    lemma named_nested (name : ℝ → ι) (Z : ι → Variables Ω μ)
    (old newer : ℝ → ℝ) (A : ℝ → Ω → Prop)
    (hA : ∀ ω, Monotone (fun H => A H ω))
    (hrep : ∀ H ω, A H ω ↔ active (Z (name H)) H (old H) ω)
    (hold : ∀ s t, name s=name t → |old s-old t| ≤ |s-t|/2)
    (hnew : ∀ s t, name s=name t → |newer s-newer t| ≤ |s-t|)
    (hd : ∀ s t, name s≠name t → |newer s-old s| ≤ |s-t|/8)
    (ω : Ω) : Monotone (fun H => active (Z (name H)) H (newer H) ω) := by
…

    Mentions: OAI.PlanarL1.Threshold.Variables, OAI.PlanarL1.Threshold.active