OAI/Analysis/DiskMaximal/Marks.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IntrinsicMarks.direction line 48
2. lemma OAI.IntrinsicMarks.norm_direction line 52
3. lemma OAI.IntrinsicMarks.mass_direction line 58
4. lemma OAI.IntrinsicMarks.debt_identity line 63
5. lemma OAI.IntrinsicMarks.marked_mass_le line 70
6. inductive OAI.IntrinsicMarks.Tree line 83

   Source documentation

   Finite uniform branching includes each finite positive-refinement path forest by padding absent children with zero vectors. No triangle defect is assumed.

   inductive Tree (ι : Type*) (E : Type*) where
   …

7. def OAI.IntrinsicMarks.vector line 89
8. def OAI.IntrinsicMarks.terminalMass line 93
9. lemma OAI.IntrinsicMarks.norm_vector_le_terminalMass line 98
10. def OAI.IntrinsicMarks.markedCost line 106

    Source documentation

    Only the first crossing from the most recent marked direction is counted; a crossing resets the anchor before descending further.

    def markedCost (e : E) (δ : ℝ) : Tree ι E → E → ℝ
      | .leaf v, n => if δ < ‖direction e v-n‖ then ‖v‖ else 0
      | .branch t, n =>
          let v := ∑ i, vector (t i)
    …

    Mentions: OAI.IntrinsicMarks.Tree, OAI.IntrinsicMarks.direction, OAI.IntrinsicMarks.vector

11. theorem OAI.IntrinsicMarks.markedCost_le line 114
12. def OAI.IntrinsicMarks.costWithRoot line 149
13. theorem OAI.IntrinsicMarks.costWithRoot_le line 155
14. def OAI.IntrinsicMarks.survival line 185

    Source documentation

    The fraction of the child capacity occupied by particles already alive.

    def survival (t : ι → Tree ι E) : ℝ :=
    …

    Mentions: OAI.IntrinsicMarks.Tree

15. lemma OAI.IntrinsicMarks.survival_nonneg line 188
16. lemma OAI.IntrinsicMarks.survival_le_one line 192
17. lemma OAI.IntrinsicMarks.survival_capacity line 196
18. def OAI.IntrinsicMarks.rootEval line 208

    Source documentation

    Explicit finite weighted evaluation on terminal paths, for the population born at the current root. Every branching has its true capacity ratio.

    def rootEval : Tree ι E → (List ι → ℝ) → ℝ
      | .leaf v, F => ‖v‖ * F []
      | .branch t, F => survival t * ∑ i, rootEval (t i) (fun p => F (i::p))
    
    /-- Explicit finite evaluation of populations born strictly below this root.
    The complete prefix is retained, including the part before birth. -/

    Mentions: OAI.IntrinsicMarks.Tree, OAI.IntrinsicMarks.survival

19. def OAI.IntrinsicMarks.lateEval line 214

    Source documentation

    Explicit finite evaluation of populations born strictly below this root. The complete prefix is retained, including the part before birth.

    def lateEval : Tree ι E → (List ι → ℕ → ℝ) → ℝ
      | .leaf _, _ => 0
      | .branch t, F =>
          (1-survival t) * (∑ i, rootEval (t i) (fun p => F (i::p) 1)) +
            ∑ i, lateEval (t i) (fun p b => F (i::p) (b+1))

    Mentions: OAI.IntrinsicMarks.Tree, OAI.IntrinsicMarks.survival, OAI.IntrinsicMarks.rootEval

20. def OAI.IntrinsicMarks.particleEval line 220
21. lemma OAI.IntrinsicMarks.rootEval_nonneg line 223
22. lemma OAI.IntrinsicMarks.lateEval_nonneg line 230
23. lemma OAI.IntrinsicMarks.particleEval_nonneg line 239
24. lemma OAI.IntrinsicMarks.rootEval_const line 242
25. lemma OAI.IntrinsicMarks.rootEval_add line 252
26. lemma OAI.IntrinsicMarks.rootEval_smul line 258
27. lemma OAI.IntrinsicMarks.lateEval_const line 264
28. lemma OAI.IntrinsicMarks.particleEval_const line 276
29. lemma OAI.IntrinsicMarks.lateEval_add line 281
30. lemma OAI.IntrinsicMarks.lateEval_smul line 287
31. lemma OAI.IntrinsicMarks.particleEval_add line 293
32. lemma OAI.IntrinsicMarks.particleEval_smul line 298
33. lemma OAI.IntrinsicMarks.particleEval_mono line 302
34. def OAI.IntrinsicMarks.pathCharge line 315

    Source documentation

    Sum a node charge only at and after the particle's birth.

    def pathCharge (C : List ι → ℝ) : List ι → ℕ → ℝ
      | [], 0 => C []
      | [], _+1 => 0
      | i::p, 0 => C [] + pathCharge (fun q => C (i::q)) p 0
      | i::p, b+1 => pathCharge (fun q => C (i::q)) p b

35. def OAI.IntrinsicMarks.nodeCharge line 321
36. theorem OAI.IntrinsicMarks.particle_occupancy line 327

    Source documentation

    Exact occupancy identity for every node charge. This includes all levels, not only the terminal mass; populations created later are not charged earlier.

    theorem particle_occupancy (t : Tree ι E) (C : List ι → ℝ) :
        particleEval t (pathCharge C) = nodeCharge t C := by
    …

    Mentions: OAI.IntrinsicMarks.Tree, OAI.IntrinsicMarks.particleEval, OAI.IntrinsicMarks.pathCharge, OAI.IntrinsicMarks.nodeCharge

37. def OAI.IntrinsicMarks.validPath line 348
38. lemma OAI.IntrinsicMarks.rootEval_mono_on line 354
39. lemma OAI.IntrinsicMarks.lateEval_mono_on line 363
40. theorem OAI.IntrinsicMarks.particleEval_mono_on line 378

    Source documentation

    Particle monotonicity requires bounds only on genuine terminal paths and legal birth times; the explicit construction has no mass elsewhere.

    theorem particleEval_mono_on (t : Tree ι E) {F G : List ι → ℕ → ℝ}
        (h : ∀ p b, validPath t p → b ≤ p.length → F p b ≤ G p b) :
        particleEval t F ≤ particleEval t G := by
    …

    Mentions: OAI.IntrinsicMarks.Tree, OAI.IntrinsicMarks.validPath, OAI.IntrinsicMarks.particleEval

41. def OAI.IntrinsicMarks.markIndicator line 386

    Source documentation

    Intrinsic marks as an actual function on prefixes, with first-crossing reset. Prefixes outside the tree have zero charge.

    def markIndicator (e : E) (δ : ℝ) : Tree ι E → E → List ι → ℝ
      | .leaf v, n, [] => if δ < ‖direction e v-n‖ then 1 else 0
      | .leaf _, _, _::_ => 0
      | .branch t, n, [] => if δ < ‖direction e (∑ i, vector (t i))-n‖ then 1 else 0
      | .branch t, n, i::p =>
          let v := ∑ j, vector (t j)
    …

    Mentions: OAI.IntrinsicMarks.Tree, OAI.IntrinsicMarks.direction, OAI.IntrinsicMarks.vector

42. def OAI.IntrinsicMarks.rootMarkIndicator line 394
43. lemma OAI.IntrinsicMarks.marked_occupancy line 399
44. lemma OAI.IntrinsicMarks.root_marked_occupancy line 412
45. theorem OAI.IntrinsicMarks.particle_mark_budget line 418
46. theorem OAI.IntrinsicMarks.particle_switch_budget line 427

    Source documentation

    Turning a genuine pathwise switch bound into the global budget uses exact occupancy, rather than a false assumption that every particle is born at a root.

    theorem particle_switch_budget {e : E} (he : ‖e‖ = 1) {δ c : ℝ} (hδ : 0 < δ)
        (t : Tree ι E) (energy : List ι → ℝ) (switches : List ι → ℕ → ℝ)
        (hpath : ∀ p b, validPath t p → b ≤ p.length → switches p b ≤
          1+2*pathCharge (rootMarkIndicator e δ t) p b+c*pathCharge energy p b) :
        particleEval t switches ≤ (3+4/δ^2)*terminalMass t+c*nodeCharge t energy := by
    …

    Mentions: OAI.IntrinsicMarks.Tree, OAI.IntrinsicMarks.validPath, OAI.IntrinsicMarks.pathCharge, OAI.IntrinsicMarks.rootMarkIndicator, OAI.IntrinsicMarks.particleEval, OAI.IntrinsicMarks.terminalMass, OAI.IntrinsicMarks.nodeCharge

47. structure OAI.SignedAssembly.RowJet line 448
48. inductive OAI.SignedAssembly.JetTree line 453
49. def OAI.SignedAssembly.mean line 457
50. def OAI.SignedAssembly.flux line 461
51. def OAI.SignedAssembly.pathFlux line 467

    Source documentation

    Product-rule expansion over all terminal label histories. The carried mass and its derivative are updated by the exact Leibniz rule.

    def pathFlux : JetTree ι E → ℝ → E → ℝ
      | .leaf v, _, G => ⟪G,v⟫
      | .branch row _ _ t, q, G =>
          ∑ i, pathFlux (t i) (q*row.law i) (q • row.grad i+row.law i • G)

    Mentions: OAI.SignedAssembly.JetTree

52. lemma OAI.SignedAssembly.pathFlux_eq line 472
53. lemma OAI.SignedAssembly.terminal_flux line 482
54. def OAI.SignedAssembly.TerminalBound line 486

    Source documentation

    Every terminal continuation is within B of the same closed-prefix value.

    def TerminalBound : JetTree ι E → E → ℝ → Prop
      | .leaf v, c, B => ‖v-c‖ ≤ B
      | .branch _ _ _ t, c, B => ∀ i, TerminalBound (t i) c B

    Mentions: OAI.SignedAssembly.JetTree

55. lemma OAI.SignedAssembly.mean_bound line 490
56. lemma OAI.SignedAssembly.prefix_cancellation line 509

    Source documentation

    This is the exact zero-row-sum cancellation. No unsigned path-potential bound is used and the parent prefix may be arbitrarily large.

    lemma prefix_cancellation (row : RowJet ι E) (v : ι → E) (c : E) :
        (∑ i, ⟪row.grad i,v i⟫) = ∑ i, ⟪row.grad i,v i-c⟫ := by
    …

    Mentions: OAI.SignedAssembly.RowJet

57. lemma OAI.SignedAssembly.row_flux_bound line 513
58. def OAI.SignedAssembly.Controlled line 523
59. def OAI.SignedAssembly.cost line 527
60. theorem OAI.SignedAssembly.signed_flux_bound line 533

    Source documentation

    Full finite-history signed flux estimate, with all stochastic prefix weights kept. The node bound is the tail oscillation, not the old envelope.

    theorem signed_flux_bound (t : JetTree ι E) (ht : Controlled t) :
        |pathFlux t 1 0| ≤ cost t := by
    …

    Mentions: OAI.SignedAssembly.JetTree, OAI.SignedAssembly.Controlled, OAI.SignedAssembly.pathFlux, OAI.SignedAssembly.cost

61. lemma OAI.PlanePotential.potential_norm_lintegral line 556
62. lemma OAI.PlanePotential.potential_integrable_of_density line 570
63. theorem OAI.PlanePotential.kernel_potential_ae_integrable line 580

    Source documentation

    Finiteness of the genuine singular integrals, obtained from the column estimate itself. This justifies insertion of the finite vector decomposition.

    theorem kernel_potential_ae_integrable (μ : Measure ℂ) [SFinite μ]
        {K : ℂ × ℂ → ℂ} (hK : Measurable K) {b : ℂ → ℂ} (hb : Integrable b)
        {C : ℝ≥0∞} (hC : C < ⊤)
        (hcol : ∀ᵐ y ∂volume.withDensity (fun y => ENNReal.ofReal ‖b y‖),
          (∫⁻ x, (ENNReal.ofReal ‖K (x,y)‖)^(3/2:ℝ) ∂μ) ≤ C) :
        ∀ᵐ x ∂μ, Integrable (fun y => ⟪K (x,y),b y⟫) := by
    …

64. lemma OAI.PlanePotential.green_root_column line 606
65. lemma OAI.PlanePotential.green_ae_integrable line 620
66. lemma OAI.PlanePotential.green_root_lp line 634
67. lemma OAI.PlanePotential.eLpNorm_three_halves_bound line 668
68. lemma OAI.PlanePotential.potential_aestronglyMeasurable line 678
69. lemma OAI.PlanePotential.potential_memLp_of_bound line 685
70. theorem OAI.PlanePotential.exists_kernel_cutoff line 698

    Source documentation

    A genuine fixed smooth probability cutoff. Its finite size and Lipschitz constants depend on no input, no dyadic level and no number of scales.

    theorem exists_kernel_cutoff : ∃ (ψ : ℂ → ℝ) (B L : ℝ),
        0 ≤ B ∧ 0 ≤ L ∧ ContDiff ℝ ∞ ψ ∧ HasCompactSupport ψ ∧
        (∫ x, ψ x) = 1 ∧ (∀ x, ψ x ≠ 0 → ‖x‖ ≤ 1) ∧
        (∀ x, |ψ x| ≤ B) ∧ (∀ x y, |ψ x-ψ y| ≤ L*‖x-y‖) := by
    …