PeriodicMeasure.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem310Support.periodic_mem_nat line 12

Source documentation

Iterating a period-one membership equivalence.

theorem periodic_mem_nat {H : Set ℝ}
    (hH : ∀ x : ℝ, x + 1 ∈ H ↔ x ∈ H) (n : ℕ) (x : ℝ) :
    x + (n : ℝ) ∈ H ↔ x ∈ H := by
…

theorem OAI.Problem310Support.periodic_unit_volume_nat line 22

Source documentation

Integer translates of a unit cell have the same occupied volume.

theorem periodic_unit_volume_nat {H : Set ℝ}
    (hH : ∀ x : ℝ, x + 1 ∈ H ↔ x ∈ H) (n : ℕ) :
    volume (H ∩ Icc (n : ℝ) ((n : ℝ) + 1)) =
      volume (H ∩ Icc (0 : ℝ) 1) := by
…

theorem OAI.Problem310Support.periodic_nat_interval_volume_le line 41

Source documentation

A period-one set occupies at most n times its unit-cell volume in n cells. No measurability assumption is needed for this upper bound.

theorem periodic_nat_interval_volume_le {H : Set ℝ}
    (hH : ∀ x : ℝ, x + 1 ∈ H ↔ x ∈ H) (n : ℕ) :
    volume (H ∩ Icc (0 : ℝ) (n : ℝ)) ≤
      (n : ENNReal) * volume (H ∩ Icc (0 : ℝ) 1) := by
…

theorem OAI.Problem310Support.periodic_dilate_unit_volume_le line 62

Source documentation

Pulling a period-one set back by a positive integer dilation cannot increase the volume occupied inside the unit interval.

theorem periodic_dilate_unit_volume_le {H : Set ℝ}
    (hH : ∀ x : ℝ, x + 1 ∈ H ↔ x ∈ H) {n : ℕ} (hn : 0 < n) :
    volume ({x : ℝ | (n : ℝ) * x ∈ H} ∩ Icc (0 : ℝ) 1) ≤
      volume (H ∩ Icc (0 : ℝ) 1) := by
…

theorem OAI.Problem310Support.periodic_reflect line 84

Source documentation

Reflection preserves period-one membership.

theorem periodic_reflect {H : Set ℝ}
    (hH : ∀ x : ℝ, x + 1 ∈ H ↔ x ∈ H) :
    ∀ x : ℝ, x + 1 ∈ {y : ℝ | -y ∈ H} ↔ x ∈ {y : ℝ | -y ∈ H} := by
…

theorem OAI.Problem310Support.periodic_reflect_unit_volume line 93

Source documentation

Reflection preserves the occupied volume in a unit period.

theorem periodic_reflect_unit_volume {H : Set ℝ}
    (hH : ∀ x : ℝ, x + 1 ∈ H ↔ x ∈ H) :
    volume ({x : ℝ | -x ∈ H} ∩ Icc (0 : ℝ) 1) =
      volume (H ∩ Icc (0 : ℝ) 1) := by
…

theorem OAI.Problem310Support.periodic_neg_dilate_unit_volume_le line 112

Source documentation

The reflected version of the integer-dilation volume estimate.

theorem periodic_neg_dilate_unit_volume_le {H : Set ℝ}
    (hH : ∀ x : ℝ, x + 1 ∈ H ↔ x ∈ H) {n : ℕ} (hn : 0 < n) :
    volume ({x : ℝ | -((n : ℝ) * x) ∈ H} ∩ Icc (0 : ℝ) 1) ≤
      volume (H ∩ Icc (0 : ℝ) 1) := by
…