Density.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

def OAI.FiniteFactor.intervalDensity line 19
Source documentation
Normalized restriction density, relative to the probability base measure.
```
def intervalDensity {X : Type*} (U : Set X) (length : ℝ) : X → ℝ :=
…
```
theorem OAI.FiniteFactor.intervalDensity_integrable line 24
theorem OAI.FiniteFactor.intervalDensity_nonneg line 28
theorem OAI.FiniteFactor.intervalDensity_le line 34
theorem OAI.FiniteFactor.intervalDensity_integral line 40
theorem OAI.FiniteFactor.intervalDensity_sq_integrable line 46
theorem OAI.FiniteFactor.intervalDensity_sq_integral line 55

theorem OAI.FiniteFactor.density_energy_identity line 65

Source documentation

The mass-one identity cancels the linear term exactly.

theorem density_energy_identity {h : X → ℝ} (hh : Integrable h μ)
    (hh2 : Integrable (fun x => h x ^ 2) μ) (hm : ∫ x, h x ∂μ = 1) :
    (∫ x, (h x - 1)^2 ∂μ) = (∫ x, h x ^ 2 ∂μ) - 1 := by
…

theorem OAI.FiniteFactor.intervalDensity_energy line 78

Source documentation

Each normalized interval perturbation has energy exactly 1/length - 1.

theorem intervalDensity_energy {U : Set X} (hU : MeasurableSet U)
    {l : ℝ} (hl : 0 < l) (hm : μ.real U = l) :
    (∫ x, (intervalDensity U l x - 1)^2 ∂μ) = l⁻¹ - 1 := by
…

Mentions: OAI.FiniteFactor.intervalDensity

theorem OAI.FiniteFactor.product_density_sq_integral line 86

Source documentation

Finite independent endpoint selections: the square integral factors exactly.

theorem product_density_sq_integral {ι : Type*} [Fintype ι]
    {E : ι → Type*} [∀ i, MeasurableSpace (E i)]
    (ν : ∀ i, Measure (E i)) [∀ i, SigmaFinite (ν i)]
    (h : ∀ i, E i → ℝ) :
    (∫ x, (∏ i, h i (x i))^2 ∂Measure.pi ν) =
      ∏ i, ∫ x, h i x ^ 2 ∂ν i := by
…

theorem OAI.FiniteFactor.product_energy_le_exp line 97
Source documentation
Finite product estimate used in uniform-product-density; the bound has no dependence on the choice of endpoint orientation.
```
theorem product_energy_le_exp {ι : Type*} [Fintype ι]
    (A e : ι → ℝ) (hA0 : ∀ i, 0 ≤ A i) (hA : ∀ i, A i ≤ 1 + e i) :
    (∏ i, A i) ≤ Real.exp (∑ i, e i) := by
…
```