IntrinsicMarks1.lean`

34 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SignedDisk.IntrinsicMarks.validPath line 28
lemma OAI.SignedDisk.IntrinsicMarks.rootEval_mono_on line 34
lemma OAI.SignedDisk.IntrinsicMarks.lateEval_mono_on line 43
theorem OAI.SignedDisk.IntrinsicMarks.particleEval_mono_on line 58
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.SignedDisk.IntrinsicMarks.Tree, OAI.SignedDisk.IntrinsicMarks.validPath, OAI.SignedDisk.IntrinsicMarks.particleEval

def OAI.SignedDisk.IntrinsicMarks.markIndicator line 66

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.SignedDisk.IntrinsicMarks.Tree, OAI.SignedDisk.IntrinsicMarks.direction, OAI.SignedDisk.IntrinsicMarks.vector

def OAI.SignedDisk.IntrinsicMarks.rootMarkIndicator line 74
lemma OAI.SignedDisk.IntrinsicMarks.marked_occupancy line 79
lemma OAI.SignedDisk.IntrinsicMarks.root_marked_occupancy line 92
theorem OAI.SignedDisk.IntrinsicMarks.particle_mark_budget line 98
theorem OAI.SignedDisk.IntrinsicMarks.particle_switch_budget line 107
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.SignedDisk.IntrinsicMarks.Tree, OAI.SignedDisk.IntrinsicMarks.validPath, OAI.SignedDisk.IntrinsicMarks.pathCharge, OAI.SignedDisk.IntrinsicMarks.rootMarkIndicator, OAI.SignedDisk.IntrinsicMarks.particleEval, OAI.SignedDisk.IntrinsicMarks.terminalMass, OAI.SignedDisk.IntrinsicMarks.nodeCharge
structure OAI.SignedDisk.SignedAssembly.RowJet line 128
inductive OAI.SignedDisk.SignedAssembly.JetTree line 133
def OAI.SignedDisk.SignedAssembly.mean line 137
def OAI.SignedDisk.SignedAssembly.flux line 141
def OAI.SignedDisk.SignedAssembly.pathFlux line 147
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.SignedDisk.SignedAssembly.JetTree
lemma OAI.SignedDisk.SignedAssembly.pathFlux_eq line 152
lemma OAI.SignedDisk.SignedAssembly.terminal_flux line 162
def OAI.SignedDisk.SignedAssembly.TerminalBound line 165
lemma OAI.SignedDisk.SignedAssembly.mean_bound line 169
lemma OAI.SignedDisk.SignedAssembly.prefix_cancellation line 188
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.SignedDisk.SignedAssembly.RowJet
lemma OAI.SignedDisk.SignedAssembly.row_flux_bound line 192
def OAI.SignedDisk.SignedAssembly.Controlled line 202
def OAI.SignedDisk.SignedAssembly.cost line 206
theorem OAI.SignedDisk.SignedAssembly.signed_flux_bound line 212
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.SignedDisk.SignedAssembly.JetTree, OAI.SignedDisk.SignedAssembly.Controlled, OAI.SignedDisk.SignedAssembly.pathFlux, OAI.SignedDisk.SignedAssembly.cost
lemma OAI.SignedDisk.PlanePotential.potential_norm_lintegral line 235
lemma OAI.SignedDisk.PlanePotential.potential_integrable_of_density line 249

theorem OAI.SignedDisk.PlanePotential.kernel_potential_ae_integrable line 259

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
…

lemma OAI.SignedDisk.PlanePotential.green_root_column line 285
lemma OAI.SignedDisk.PlanePotential.green_ae_integrable line 299
lemma OAI.SignedDisk.PlanePotential.green_root_lp line 313
lemma OAI.SignedDisk.PlanePotential.eLpNorm_three_halves_bound line 344
lemma OAI.SignedDisk.PlanePotential.potential_aestronglyMeasurable line 354
lemma OAI.SignedDisk.PlanePotential.potential_memLp_of_bound line 361

theorem OAI.SignedDisk.PlanePotential.exists_kernel_cutoff line 374

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
…