HierarchyNormalization.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The normalized child identity

Exact algebra for §8, equation (src-25): the ratio of the parent amount (with the residual omitted) to its child denominator equals the weighted prediction ratio. No estimates or hierarchy hypotheses enter this identity.

theorem OAI.LipschitzHilbert.child_normalization_coefficient line 21
theorem OAI.LipschitzHilbert.normalized_child_sum line 34
theorem OAI.LipschitzHilbert.normalized_vector_power line 50

theorem OAI.LipschitzHilbert.normalized_child_ratio line 57

Source documentation

Equation (src-25), with every scalar power and normalization explicit.

theorem normalized_child_ratio (n : ℝ) (m : ι → ℝ) (A : ι → E) (lambda : ι → ℂ)
    (μ α p : ℝ) (hn : 0 < n) (hm : ∀ i, 0 < m i) (hrelation : p * μ = α - 1) :
    (n + n ^ (α - p) * ‖∑ i, lambda i • A i‖ ^ p) /
      (n + ∑ i, m i ^ (α - p) * ‖A i‖ ^ p) =
    (1 + ‖∑ i, ((((m i / n) ^ (1 - μ) : ℝ) : ℂ) * lambda i) •
      (((m i ^ (μ - 1) : ℝ) : ℂ) • A i)‖ ^ p) /
      (1 + ∑ i, (m i / n) * ‖((m i ^ (μ - 1) : ℝ) : ℂ) • A i‖ ^ p) := by
…