PlanePotential2.lean`

43 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.SignedDisk.PlanePotential.kernel_column_lp line 26

lemma OAI.SignedDisk.PlanePotential.potential_domination line 61

Source documentation

No pointwise integrability assertion for the singular kernel is needed in this domination: the Bochner integral is bounded by the nonnegative integral.

lemma potential_domination {L : ℂ → ℂ} (hL : Measurable L) {b : ℂ → ℂ}
    (hb : Integrable b) :
    ENNReal.ofReal |∫ y, ⟪L y,b y⟫| ≤
      ∫⁻ y, ENNReal.ofReal ‖L y‖ ∂volume.withDensity (fun y => ENNReal.ofReal ‖b y‖) := by
…

theorem OAI.SignedDisk.PlanePotential.cancelled_potential_lp line 79
lemma OAI.SignedDisk.PlanePotential.zero_mass_kernel_shift line 115
lemma OAI.SignedDisk.PlanePotential.cancelled_potential_eq line 130

lemma OAI.SignedDisk.PlanePotential.column_scaling line 140

Source documentation

Uniform scaling of the exact p-th power column constant: in dimension two and at p=3/2 its radius dependence is precisely a^(1/2).

lemma column_scaling {K D a : ℝ} (hD : 0 ≤ D) (ha : 0 < a) :
    K^(3/2:ℝ)*(4*Real.pi*(4*a)^(1/2:ℝ)) +
      (D*a)^(3/2:ℝ)*(2*Real.pi/(2*a)) =
      (8*Real.pi*K^(3/2:ℝ)+Real.pi*D^(3/2:ℝ))*a^(1/2:ℝ) := by
…

theorem OAI.SignedDisk.PlanePotential.green_zero_piece_lp line 154
def OAI.SignedDisk.IntrinsicMarks.direction line 182
lemma OAI.SignedDisk.IntrinsicMarks.norm_direction line 186
lemma OAI.SignedDisk.IntrinsicMarks.mass_direction line 192
lemma OAI.SignedDisk.IntrinsicMarks.debt_identity line 197
lemma OAI.SignedDisk.IntrinsicMarks.marked_mass_le line 204
inductive OAI.SignedDisk.IntrinsicMarks.Tree line 217
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
…
```
def OAI.SignedDisk.IntrinsicMarks.vector line 223
def OAI.SignedDisk.IntrinsicMarks.terminalMass line 227
lemma OAI.SignedDisk.IntrinsicMarks.norm_vector_le_terminalMass line 232
def OAI.SignedDisk.IntrinsicMarks.markedCost line 240
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.SignedDisk.IntrinsicMarks.Tree, OAI.SignedDisk.IntrinsicMarks.direction, OAI.SignedDisk.IntrinsicMarks.vector
theorem OAI.SignedDisk.IntrinsicMarks.markedCost_le line 248
def OAI.SignedDisk.IntrinsicMarks.costWithRoot line 283
theorem OAI.SignedDisk.IntrinsicMarks.costWithRoot_le line 289
def OAI.SignedDisk.IntrinsicMarks.survival line 318
Source documentation
The fraction of the child capacity occupied by particles already alive.
```
def survival (t : ι → Tree ι E) : ℝ :=
…
```
Mentions: OAI.SignedDisk.IntrinsicMarks.Tree
lemma OAI.SignedDisk.IntrinsicMarks.survival_nonneg line 321
lemma OAI.SignedDisk.IntrinsicMarks.survival_le_one line 325
lemma OAI.SignedDisk.IntrinsicMarks.survival_capacity line 329

def OAI.SignedDisk.IntrinsicMarks.rootEval line 341

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

def OAI.SignedDisk.IntrinsicMarks.lateEval line 347
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.SignedDisk.IntrinsicMarks.Tree, OAI.SignedDisk.IntrinsicMarks.survival, OAI.SignedDisk.IntrinsicMarks.rootEval
def OAI.SignedDisk.IntrinsicMarks.particleEval line 353
lemma OAI.SignedDisk.IntrinsicMarks.rootEval_nonneg line 356
lemma OAI.SignedDisk.IntrinsicMarks.lateEval_nonneg line 363
lemma OAI.SignedDisk.IntrinsicMarks.particleEval_nonneg line 372
lemma OAI.SignedDisk.IntrinsicMarks.rootEval_const line 375
lemma OAI.SignedDisk.IntrinsicMarks.rootEval_add line 385
lemma OAI.SignedDisk.IntrinsicMarks.rootEval_smul line 391
lemma OAI.SignedDisk.IntrinsicMarks.lateEval_const line 397
lemma OAI.SignedDisk.IntrinsicMarks.particleEval_const line 409
lemma OAI.SignedDisk.IntrinsicMarks.lateEval_add line 414
lemma OAI.SignedDisk.IntrinsicMarks.lateEval_smul line 420
lemma OAI.SignedDisk.IntrinsicMarks.particleEval_add line 426
lemma OAI.SignedDisk.IntrinsicMarks.particleEval_smul line 431
lemma OAI.SignedDisk.IntrinsicMarks.particleEval_mono line 435

def OAI.SignedDisk.IntrinsicMarks.pathCharge line 448

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

def OAI.SignedDisk.IntrinsicMarks.nodeCharge line 454
theorem OAI.SignedDisk.IntrinsicMarks.particle_occupancy line 460
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.SignedDisk.IntrinsicMarks.Tree, OAI.SignedDisk.IntrinsicMarks.particleEval, OAI.SignedDisk.IntrinsicMarks.pathCharge, OAI.SignedDisk.IntrinsicMarks.nodeCharge