AngularPathNormalization.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The equal-coordinate value of the shared analytic family. The endpoint mass cancels exactly and leaves only parent-to-boundary ratios.

theorem OAI.LipschitzHilbert.hierarchyWeight_eq_path_product line 14

Source documentation

The path product in the shared analytic family is the exponential weight used in the full-root variation estimate.

theorem hierarchyWeight_eq_path_product (n b : ℕ → ℝ) (phase : ℕ → ℂ)
    (a : ℝ) (N : ℕ) (hn : 0 < n N)
    (hn' : ∀ j < N, 0 < n (j+1)) (hb : ∀ j < N, 0 < b j) :
    hierarchyWeight n (fun j => Real.log (b j / n (j+1))) phase a N =
      ((n N ^ (-a) : ℝ) : ℂ) * ∏ j ∈ Finset.range N,
        Complex.exp (phase j * (Real.log (n (j+1) / b j) : ℂ)) := by
…

Mentions: OAI.LipschitzHilbert.hierarchyWeight

theorem OAI.LipschitzHilbert.normalized_endpoint_telescope line 41