AngularLossMotion.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Relative motion of nonnegative logarithmic losses. Both the submass and its complement are actual positive sums. Vanishing complements give identically zero loss and need no logarithmic positivity assumption.

theorem OAI.LipschitzHilbert.log_one_add_scaled_le line 16
Source documentation
Concavity of the logarithm controls multiplicative changes in its nonnegative argument, uniformly even at argument zero.
```
theorem log_one_add_scaled_le {c q : ℝ} (hc : 1 ≤ c) (hq : 0 ≤ q) :
    Real.log (1+c*q) ≤ c*Real.log (1+q) := by
…
```
theorem OAI.LipschitzHilbert.positive_le_exp_mul_of_log_motion line 33

theorem OAI.LipschitzHilbert.positive_complement_loss_motion line 43

Source documentation

The loss log((a+b)/a) varies relatively with the positive submass and complement, instead of paying a constant independent of that loss.

theorem positive_complement_loss_motion {a b a' b' delta : ℝ}
    (ha : 0 < a) (hb : 0 < b) (ha' : 0 < a') (hb' : 0 < b')
    (hdelta : 0 ≤ delta)
    (hA : |Real.log a'-Real.log a| ≤ delta)
    (hB : |Real.log b'-Real.log b| ≤ delta) :
    |Real.log ((a'+b')/a')-Real.log ((a+b)/a)| ≤
      (Real.exp (2*delta)-1)*Real.log ((a+b)/a) := by
…

theorem OAI.LipschitzHilbert.finite_submass_loss_motion line 81

Source documentation

A finite submass and its actual set complement give relative loss motion. Empty complements are handled exactly, as zero loss.

theorem finite_submass_loss_motion {ι : Type*} [DecidableEq ι] (C A : Finset ι) (hsub : A ⊆ C)
    (hA : A.Nonempty) (w0 w1 : ι → ℝ)
    (hw0 : ∀ t ∈ C, 0 < w0 t) (hw1 : ∀ t ∈ C, 0 < w1 t)
    {delta : ℝ} (hdelta : 0 ≤ delta)
    (hmass : |Real.log (∑ t ∈ A, w1 t)-Real.log (∑ t ∈ A, w0 t)| ≤ delta)
    (hcomplement : (C\A).Nonempty →
      |Real.log (∑ t ∈ C\A, w1 t)-Real.log (∑ t ∈ C\A, w0 t)| ≤ delta) :
    |Real.log ((∑ t ∈ C, w1 t)/(∑ t ∈ A, w1 t)) -
      Real.log ((∑ t ∈ C, w0 t)/(∑ t ∈ A, w0 t))| ≤
        (Real.exp (2*delta)-1)*Real.log ((∑ t ∈ C, w0 t)/(∑ t ∈ A, w0 t)) := by
…

theorem OAI.LipschitzHilbert.relative_loss_factor_le line 111
Source documentation
On the small-motion range the relative loss factor is linear in that motion, with an absolute constant.
```
theorem relative_loss_factor_le {delta : ℝ} (hdelta : 0 ≤ delta) (hsmall : delta ≤ 1/2) :
    Real.exp (2*delta)-1 ≤ (2*Real.exp 1)*delta := by
…
```

theorem OAI.LipschitzHilbert.AngularGrid.source_relative_loss_motion line 130

Source documentation

At the source mesh scale, the child-to-containing-mass loss has a relative error of order G^(-1/2), including identically zero losses.

theorem source_relative_loss_motion {ι : Type*} (g : AngularGrid) (tops : Finset ι)
    (T : ι → SlopeBox) (w B K D : ℝ) (hw : 0 < w) (hB : 1 ≤ B)
    (hK : 0 < K) (hD : 0 ≤ D) (hwidth : ∀ t ∈ tops, B^2*w ≤ (T t).width)
    (base h i : ℕ) (hhi : h ≤ i) (gap : ℝ) (hgap0 : 0 ≤ gap) (hgap : gap ≤ g.width h)
    (s sR : ℝ) (hs : g.index h s = g.index h sR)
    (child : ℝ) (hchild : 0 < child) (hblock : g.width h ≤ B*child)
    (C A : Finset ι) (hsub : A ⊆ C) (hA : A.Nonempty)
    (hC : C ⊆ g.boundaryTops tops (fun t => (T t).slope)
      (fun t => w/(T t).length) (g.rootWidth/B^2) base i gap s)
    (a : ℝ) (ha : |a| ≤ w/(child*Real.sqrt (g.branching:ℝ))) (z : ℝ × ℝ) :
    let loss := fun x => Real.log ((∑ t ∈ C, (T t).weight K D x)/(∑ t ∈ A, (T t).weight K D x))
…

Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.AngularGrid.width