LogProfile.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

The finite logarithmic profile

The profile is zero at infinite graph distance. Its exact finite expansion and the factor-three dilation estimate include distances beyond the cutoff.

def OAI.MetricEntropyDuality.LogProfile.gamma line 25
Source documentation
The positive logarithmic increment at level j.
```
def gamma (h j : ℕ) : ℝ :=
…
```
def OAI.MetricEntropyDuality.LogProfile.phi line 29
Source documentation
The actual cutoff profile, with a separate value at infinite distance.
```
def phi (h : ℕ) (d : ℕ∞) : ℝ :=
…
```
theorem OAI.MetricEntropyDuality.LogProfile.log_cutoff_pos line 33
theorem OAI.MetricEntropyDuality.LogProfile.gamma_pos line 38
theorem OAI.MetricEntropyDuality.LogProfile.gamma_nonneg line 45
theorem OAI.MetricEntropyDuality.LogProfile.phi_top line 48
theorem OAI.MetricEntropyDuality.LogProfile.phi_coe line 50
theorem OAI.MetricEntropyDuality.LogProfile.phi_zero line 55
theorem OAI.MetricEntropyDuality.LogProfile.phi_nonneg line 57
theorem OAI.MetricEntropyDuality.LogProfile.phi_le_one line 63
theorem OAI.MetricEntropyDuality.LogProfile.phi_eq_zero_of_le line 72

theorem OAI.MetricEntropyDuality.LogProfile.sum_log_steps line 87

Source documentation

Telescoping a tail also handles an empty tail by the minimum endpoint.

private theorem sum_log_steps (d h : ℕ) :
    (∑ j ∈ Finset.range h,
      if d ≤ j then Real.log ((j : ℝ) + 2) - Real.log ((j : ℝ) + 1) else 0) =
      Real.log ((h : ℝ) + 1) - Real.log (((min d h : ℕ) : ℝ) + 1) := by
…

theorem OAI.MetricEntropyDuality.LogProfile.sum_gamma_tail line 104
theorem OAI.MetricEntropyDuality.LogProfile.phi_eq_sum line 119
Source documentation
Exact expansion into the finite graph-ball indicators.
```
theorem phi_eq_sum {h : ℕ} (hh : 0 < h) (d : ℕ∞) :
    phi h d = ∑ j ∈ Finset.range h, if d ≤ (j : ℕ∞) then gamma h j else 0 := by
…
```
Mentions: OAI.MetricEntropyDuality.LogProfile.phi, OAI.MetricEntropyDuality.LogProfile.gamma
theorem OAI.MetricEntropyDuality.LogProfile.sum_gamma line 138
theorem OAI.MetricEntropyDuality.LogProfile.phi_eq_sum_mul_indicator line 142

theorem OAI.MetricEntropyDuality.LogProfile.dilation line 148

Source documentation

The exact discrete factor-three dilation bound.

theorem dilation {h : ℕ} (hh : 0 < h) (d : ℕ∞) :
    (∑ j ∈ Finset.range h,
      if d ≤ ((3 * j + 2 : ℕ) : ℕ∞) then gamma h j else 0) ≤
      phi h d + Real.log 3 / Real.log ((h : ℝ) + 1) := by
…

Mentions: OAI.MetricEntropyDuality.LogProfile.gamma, OAI.MetricEntropyDuality.LogProfile.phi

theorem OAI.MetricEntropyDuality.LogProfile.dilation_mul_indicator line 183