Cube.lean`

49 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem358.cube_eq_coord_box line 8
theorem OAI.Problem358.isCompact_cube line 15
theorem OAI.Problem358.convex_cube line 20
theorem OAI.Problem358.zero_mem_cube line 32
theorem OAI.Problem358.cube_nonempty line 36
theorem OAI.Problem358.ball_zero_subset_cube line 38
theorem OAI.Problem358.zero_mem_interior_cube line 45
theorem OAI.Problem358.interior_cube_nonempty line 49
theorem OAI.Problem358.cube_eq_preimage_pi line 58
theorem OAI.Problem358.volume_cube line 65
Source documentation
The Euclidean cube has its usual Lebesgue volume.
```
theorem volume_cube (d : ℕ) : volume (cube d) = (2 : ℝ≥0∞) ^ d := by
…
```
def OAI.Problem358.intervalUniform line 73
Source documentation
The uniform probability law on one coordinate of the cube.
```
def intervalUniform : Measure ℝ :=
…
```
instance OAI.Problem358.intervalUniform_isProbabilityMeasure line 76

theorem OAI.Problem358.intervalUniform_prod line 82

Source documentation

The two-coordinate law is one quarter of planar area restricted to the square.

theorem intervalUniform_prod :
    intervalUniform.prod intervalUniform =
      (4 : ℝ≥0∞)⁻¹ • volume.restrict
        (Set.Icc (-1 : ℝ) 1 ×ˢ Set.Icc (-1 : ℝ) 1) := by
…

Mentions: OAI.Problem358.intervalUniform

theorem OAI.Problem358.map_ofLp_volume_restrict_cube line 93

Source documentation

Restricting Euclidean volume to the cube becomes the product of interval restrictions.

theorem map_ofLp_volume_restrict_cube (d : ℕ) :
    Measure.map (@WithLp.ofLp 2 (Fin d → ℝ)) (volume.restrict (cube d)) =
      Measure.pi (fun _ : Fin d => volume.restrict (Set.Icc (-1 : ℝ) 1)) := by
…

theorem OAI.Problem358.map_ofLp_uniformMeasure_cube line 102

Source documentation

The normalized cube law is the product of normalized interval laws.

theorem map_ofLp_uniformMeasure_cube (d : ℕ) :
    Measure.map (@WithLp.ofLp 2 (Fin d → ℝ)) (uniformMeasure (cube d)) =
      Measure.pi (fun _ : Fin d => intervalUniform) := by
…

Mentions: OAI.Problem358.intervalUniform

theorem OAI.Problem358.measurePreserving_ofLp_uniformMeasure_cube line 114

Source documentation

Coordinate representation preserves the normalized cube law.

theorem measurePreserving_ofLp_uniformMeasure_cube (d : ℕ) :
    MeasurePreserving (@WithLp.ofLp 2 (Fin d → ℝ)) (uniformMeasure (cube d))
      (Measure.pi (fun _ : Fin d => intervalUniform)) :=
…

Mentions: OAI.Problem358.intervalUniform

theorem OAI.Problem358.measurePreserving_coord_uniformMeasure_cube line 120
Source documentation
Every coordinate of the uniform cube is uniform on [-1,1].
```
theorem measurePreserving_coord_uniformMeasure_cube {d : ℕ} (i : Fin d) :
    MeasurePreserving (fun x : E d => x i) (uniformMeasure (cube d)) intervalUniform :=
…
```
Mentions: OAI.Problem358.intervalUniform

theorem OAI.Problem358.measurePreserving_coordPair_uniformMeasure_cube line 126

Source documentation

Two distinct coordinates of the uniform cube have the product interval law.

theorem measurePreserving_coordPair_uniformMeasure_cube {d : ℕ} (i j : Fin d)
    (hij : i ≠ j) :
    MeasurePreserving (fun x : E d => (x i, x j)) (uniformMeasure (cube d))
      (intervalUniform.prod intervalUniform) := by
…

Mentions: OAI.Problem358.intervalUniform

theorem OAI.Problem358.integral_coordPair_uniformMeasure_cube line 145

Source documentation

Integration of a function of two coordinates reduces to a two-dimensional product law.

theorem integral_coordPair_uniformMeasure_cube {d : ℕ} (i j : Fin d)
    (hij : i ≠ j) (f : ℝ × ℝ → ℝ)
    (hf : AEStronglyMeasurable f (intervalUniform.prod intervalUniform)) :
    (∫ x, f (x i, x j) ∂uniformMeasure (cube d)) =
      ∫ p, f p ∂intervalUniform.prod intervalUniform := by
…

Mentions: OAI.Problem358.intervalUniform

theorem OAI.Problem358.lintegral_coordPair_uniformMeasure_cube line 155

Source documentation

The analogous nonnegative integral identity needs only measurability.

theorem lintegral_coordPair_uniformMeasure_cube {d : ℕ} (i j : Fin d)
    (hij : i ≠ j) (f : ℝ × ℝ → ℝ≥0∞) (hf : Measurable f) :
    (∫⁻ x, f (x i, x j) ∂uniformMeasure (cube d)) =
      ∫⁻ p, f p ∂intervalUniform.prod intervalUniform :=
…

Mentions: OAI.Problem358.intervalUniform

theorem OAI.Problem358.uniformMeasure_cube_coordPair_preimage line 162

Source documentation

A planar event depending on two distinct coordinates has one quarter its square area.

theorem uniformMeasure_cube_coordPair_preimage {d : ℕ} (i j : Fin d)
    (hij : i ≠ j) (s : Set (ℝ × ℝ)) (hs : MeasurableSet s) :
    uniformMeasure (cube d) ((fun x : E d => (x i, x j)) ⁻¹' s) =
      (4 : ℝ≥0∞)⁻¹ * volume
        (s ∩ (Set.Icc (-1 : ℝ) 1 ×ˢ Set.Icc (-1 : ℝ) 1)) := by
…

def OAI.Problem358.planarStrip line 182
Source documentation
A central strip in the square, written in slice coordinates.
```
def planarStrip (a b : ℝ) : Set (ℝ × ℝ) :=
…
```
lemma OAI.Problem358.measurableSet_planarStrip line 185
lemma OAI.Problem358.volume_planarStrip_eq_lintegral line 189
lemma OAI.Problem358.integral_strip_width line 211
lemma OAI.Problem358.volume_planarStrip line 225
lemma OAI.Problem358.volume_symmDiff_centeredIntervals line 237
lemma OAI.Problem358.integral_abs_unitInterval line 253
lemma OAI.Problem358.volume_planarStrip_symmDiff line 271
lemma OAI.Problem358.planarStrip_subset_square line 313
def OAI.Problem358.planarRightStrip line 322
Source documentation
The positive outer cell of a planar affine strip, with null ties omitted.
```
def planarRightStrip (a b : ℝ) : Set (ℝ × ℝ) :=
…
```
def OAI.Problem358.planarLeftStrip line 326
Source documentation
The negative outer cell of a planar affine strip, with null ties omitted.
```
def planarLeftStrip (a b : ℝ) : Set (ℝ × ℝ) :=
…
```
lemma OAI.Problem358.measurableSet_planarRightStrip line 329
lemma OAI.Problem358.measurableSet_planarLeftStrip line 333
lemma OAI.Problem358.volume_planarRightStrip_eq_lintegral line 337
lemma OAI.Problem358.volume_planarLeftStrip_eq_lintegral line 356
lemma OAI.Problem358.integral_affine_unitInterval line 377
lemma OAI.Problem358.integral_outerStrip_width line 383
lemma OAI.Problem358.lintegral_outerStrip_width line 390
lemma OAI.Problem358.volume_planarRightStrip line 402
lemma OAI.Problem358.volume_planarLeftStrip line 406
lemma OAI.Problem358.planarRightStrip_subset_square line 410
lemma OAI.Problem358.planarLeftStrip_subset_square line 418
lemma OAI.Problem358.central_inter_square line 426
lemma OAI.Problem358.quarter_mul_ofReal line 436

theorem OAI.Problem358.uniformMeasure_cube_centralCell line 445

Source documentation

The closed tilted central cell has normalized cube mass a.

theorem uniformMeasure_cube_centralCell {d : ℕ} (i j : Fin d) (hij : i ≠ j)
    (a b : ℝ) (hb : 0 ≤ b) (hba : b ≤ a) (hab : a + b ≤ 1) :
    uniformMeasure (cube d) {x : E d | |x i| ≤ a + b * x j} =
      ENNReal.ofReal a := by
…

theorem OAI.Problem358.uniformMeasure_cube_centralCell_symmDiff line 458

Source documentation

Moving the central-cell boundary changes cube mass by b/2.

theorem uniformMeasure_cube_centralCell_symmDiff {d : ℕ} (i j : Fin d) (hij : i ≠ j)
    (a b : ℝ) (hb : 0 ≤ b) (hba : b ≤ a) (hab : a + b ≤ 1) :
    uniformMeasure (cube d)
      (symmDiff {x : E d | |x i| ≤ a} {x : E d | |x i| ≤ a + b * x j}) =
      ENNReal.ofReal (b / 2) := by
…

theorem OAI.Problem358.uniformMeasure_cube_rightCell line 480

Source documentation

The positive outer cell of a tilted slab has mass (1-a)/2.

theorem uniformMeasure_cube_rightCell {d : ℕ} (i j : Fin d) (hij : i ≠ j)
    (a b : ℝ) (hb : 0 ≤ b) (hba : b ≤ a) (hab : a + b ≤ 1) :
    uniformMeasure (cube d) {x : E d | a + b * x j < x i} =
      ENNReal.ofReal ((1 - a) / 2) := by
…

theorem OAI.Problem358.uniformMeasure_cube_leftCell line 500

Source documentation

The negative outer cell of a tilted slab has mass (1-a)/2.

theorem uniformMeasure_cube_leftCell {d : ℕ} (i j : Fin d) (hij : i ≠ j)
    (a b : ℝ) (hb : 0 ≤ b) (hba : b ≤ a) (hab : a + b ≤ 1) :
    uniformMeasure (cube d) {x : E d | x i < -(a + b * x j)} =
      ENNReal.ofReal ((1 - a) / 2) := by
…