ComplementaryMass.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Relative motion of a mass fraction retains its complementary mass.

theorem OAI.LipschitzHilbert.log_motion_of_lower_bound line 17
Source documentation
The logarithm is Lipschitz on a positive half-line, with the sharp reciprocal lower-bound constant.
```
theorem log_motion_of_lower_bound {x y c : ℝ} (hc : 0 < c)
    (hx : c ≤ x) (hy : c ≤ y) :
    |Real.log x - Real.log y| ≤ |x - y| / c := by
…
```

theorem OAI.LipschitzHilbert.complementary_mass_fraction_motion line 40

Source documentation

Two positive groups of mass moving relatively by at most ε have a fraction error proportional to r*(1-r), including a vanishing complement.

theorem complementary_mass_fraction_motion {A B A' B' ε : ℝ}
    (hA : 0 < A) (hB : 0 ≤ B) (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1 / 2)
    (hAmove : |A' - A| ≤ ε * A) (hBmove : |B' - B| ≤ ε * B) :
    0 < A' ∧ 0 < A' + B' ∧
      |A' / (A' + B') - A / (A + B)| ≤
        4 * ε * (A / (A + B)) * (1 - A / (A + B)) := by
…

theorem OAI.LipschitzHilbert.complementary_mass_log_motion line 83

Source documentation

The logarithmic fraction motion is proportional to the missing mass, even if the complement vanishes. The constant is independent of the masses.

theorem complementary_mass_log_motion {A B A' B' ε : ℝ}
    (hA : 0 < A) (hB : 0 ≤ B) (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1 / 2)
    (hAmove : |A' - A| ≤ ε * A) (hBmove : |B' - B| ≤ ε * B) :
    |Real.log (A' / (A' + B')) - Real.log (A / (A + B))| ≤
      12 * ε * (1 - A / (A + B)) := by
…