PathCoefficient.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The dominant-path coefficient from complementary masses

For the path child in §9 the coefficient is l^(1-α/p) * r^μ, where l=nₐ/n and r=nₐ/mₐ. Its defect from one and its variation retain the relative path drop.

def OAI.LipschitzHilbert.pathCoefficient line 20
theorem OAI.LipschitzHilbert.pathCoefficient_pos line 22
theorem OAI.LipschitzHilbert.pathCoefficient_le_one line 27

theorem OAI.LipschitzHilbert.pathCoefficient_defect line 38

Source documentation

Both mass fractions lie above 1-u, so two exponents in [0,1] give a coefficient defect at most 2u.

theorem pathCoefficient_defect {a b l r u : ℝ}
    (ha : a ≤ 1) (hb : b ≤ 1) (hl0 : 0 ≤ l) (hl1 : l ≤ 1)
    (hr0 : 0 ≤ r) (hr1 : r ≤ 1) (hl : 1 - l ≤ u) (hr : 1 - r ≤ u) :
    1 - pathCoefficient a b l r ≤ 2 * u := by
…

Mentions: OAI.LipschitzHilbert.pathCoefficient

theorem OAI.LipschitzHilbert.exp_nonpositive_lipschitz line 50
Source documentation
Exponentiation is one-Lipschitz on the nonpositive real half-line.
```
theorem exp_nonpositive_lipschitz {x y : ℝ} (hx : x ≤ 0) (hy : y ≤ 0) :
    |Real.exp x - Real.exp y| ≤ |x - y| := by
…
```
theorem OAI.LipschitzHilbert.positive_unit_interval_motion line 59

theorem OAI.LipschitzHilbert.pathCoefficient_motion line 67

Source documentation

Variation of the coefficient is controlled by the two complementary-mass logarithm variations, with the exact exponent weights.

theorem pathCoefficient_motion {a b l r l' r' : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b)
    (hl0 : 0 < l) (hl1 : l ≤ 1) (hr0 : 0 < r) (hr1 : r ≤ 1)
    (hl'0 : 0 < l') (hl'1 : l' ≤ 1) (hr'0 : 0 < r') (hr'1 : r' ≤ 1) :
    |pathCoefficient a b l' r' - pathCoefficient a b l r| ≤
      a * |Real.log l' - Real.log l| + b * |Real.log r' - Real.log r| := by
…

Mentions: OAI.LipschitzHilbert.pathCoefficient

theorem OAI.LipschitzHilbert.pathCoefficient_from_complementary_masses line 89

Source documentation

The actual shared child mass and its two complementary masses imply all coefficient hypotheses used by the dominant prediction comparison.

theorem pathCoefficient_from_complementary_masses
    {a b n B D n' B' D' ε u : ℝ}
    (ha0 : 0 ≤ a) (ha1 : a ≤ 1) (hb0 : 0 ≤ b) (hb1 : b ≤ 1)
    (hn : 0 < n) (hB : 0 ≤ B) (hD : 0 ≤ D)
    (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1 / 2)
    (hnmove : |n' - n| ≤ ε * n) (hBmove : |B' - B| ≤ ε * B)
    (hDmove : |D' - D| ≤ ε * D)
    (hBdrop : 1 - n / (n + B) ≤ u) (hDdrop : 1 - n / (n + D) ≤ u) :
    let C := pathCoefficient a b (n / (n + B)) (n / (n + D))
…

Mentions: OAI.LipschitzHilbert.pathCoefficient