SourceBoundaryEntropy.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The remaining logarithmic boundary loss is linear in the actual top weight after its available eight powers are used. Summation has no factor depending on the number of tops.

theorem OAI.LipschitzHilbert.boundary_weight_entropy_le line 15
Source documentation
A positive bounded weight absorbs the logarithmic ratio to the ambient mass, with a constant independent of the small weight.
```
theorem boundary_weight_entropy_le {h n C : ℝ}
    (hh : 0 < h) (hhn : h ≤ n) (hC : 1 ≤ C) (hhC : h ≤ C) :
    h^8*Real.log (n/h) ≤ C^7*h*(1+Real.log (max 1 n)) := by
…
```
theorem OAI.LipschitzHilbert.boundary_weight_entropy_sum_le line 44
theorem OAI.LipschitzHilbert.SlopeBox.weight_boundary_entropy_le line 60
theorem OAI.LipschitzHilbert.top_weight_boundary_entropy_sum_le line 69

theorem OAI.LipschitzHilbert.top_weight_boundary_entropy_sum_le_log_bound line 82

Source documentation

The common good-set logarithmic mass bound turns the entropy sum into the same linear top mass used by the plane estimates.

theorem top_weight_boundary_entropy_sum_le_log_bound {ι : Type*}
    (tops : Finset ι) (T : ι → SlopeBox) {Kw D H : ℝ}
    (hKw : 0 < Kw) (hD : 0 ≤ D) (z : ℝ×ℝ)
    (hlog : Real.log (max 1 (∑ u ∈ tops, (T u).weight Kw D z)) ≤ H) :
    (∑ t ∈ tops, ((T t).weight Kw D z)^8*
      Real.log ((∑ u ∈ tops, (T u).weight Kw D z)/(T t).weight Kw D z)) ≤
      ((2:ℝ)^D)^7*(1+H)*(∑ t ∈ tops, (T t).weight Kw D z) := by
…

Mentions: OAI.LipschitzHilbert.SlopeBox