[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J I : Box ι
⊢ ∀ (J : Box ι), J ∈ Finset.map (Box.splitCenterBoxEmb I) Finset.univ → J ≤ I
[PROOFSTEP]
simp [I.splitCenterBox_le]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J I : Box ι
⊢ Set.Pairwise (↑(Finset.map (Box.splitCenterBoxEmb I) Finset.univ)) (Disjoint on Box.toSet)
[PROOFSTEP]
rw [Finset.coe_map, Finset.coe_univ, image_univ]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J I : Box ι
⊢ Set.Pairwise (range ↑(Box.splitCenterBoxEmb I)) (Disjoint on Box.toSet)
[PROOFSTEP]
rintro _ ⟨s, rfl⟩ _ ⟨t, rfl⟩ Hne
[GOAL]
case intro.intro
ι : Type u_1
inst✝ : Fintype ι
I✝ J I : Box ι
s t : Set ι
Hne : ↑(Box.splitCenterBoxEmb I) s ≠ ↑(Box.splitCenterBoxEmb I) t
⊢ (Disjoint on Box.toSet) (↑(Box.splitCenterBoxEmb I) s) (↑(Box.splitCenterBoxEmb I) t)
[PROOFSTEP]
exact I.disjoint_splitCenterBox (mt (congr_arg _) Hne)
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
⊢ J ∈ splitCenter I ↔ ∃ s, Box.splitCenterBox I s = J
[PROOFSTEP]
simp [splitCenter]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J I : Box ι
x : ι → ℝ
hx : x ∈ I
⊢ ∃ J, J ∈ splitCenter I ∧ x ∈ J
[PROOFSTEP]
simp [hx]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J : Box ι
p : Box ι → Prop
I : Box ι
H_ind : ∀ (J : Box ι), J ≤ I → (∀ (J' : Box ι), J' ∈ splitCenter J → p J') → p J
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
⊢ p I
[PROOFSTEP]
refine' subbox_induction_on' I (fun J hle hs => H_ind J hle fun J' h' => _) H_nhds
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_ind : ∀ (J : Box ι), J ≤ I → (∀ (J' : Box ι), J' ∈ splitCenter J → p J') → p J
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : Box ι
hle : J ≤ I
hs : ∀ (s : Set ι), p (splitCenterBox J s)
J' : Box ι
h' : J' ∈ splitCenter J
⊢ p J'
[PROOFSTEP]
rcases mem_splitCenter.1 h' with ⟨s, rfl⟩
[GOAL]
case intro
ι : Type u_1
inst✝ : Fintype ι
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_ind : ∀ (J : Box ι), J ≤ I → (∀ (J' : Box ι), J' ∈ splitCenter J → p J') → p J
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : Box ι
hle : J ≤ I
hs : ∀ (s : Set ι), p (splitCenterBox J s)
s : Set ι
h' : splitCenterBox J s ∈ splitCenter J
⊢ p (splitCenterBox J s)
[PROOFSTEP]
exact hs s
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
⊢ ∃ π,
    TaggedPrepartition.IsPartition π ∧
      IsHenstock π ∧
        IsSubordinate π r ∧
          (∀ (J : Box ι), J ∈ π → ∃ m, ∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) ∧
            TaggedPrepartition.distortion π = distortion I
[PROOFSTEP]
refine' subbox_induction_on I (fun J _ hJ => _) fun z _ => _
[GOAL]
case refine'_1
ι : Type u_1
inst✝ : Fintype ι
I✝ J✝ I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
J : Box ι
x✝ : J ≤ I
hJ :
  ∀ (J' : Box ι),
    J' ∈ splitCenter J →
      ∃ π,
        TaggedPrepartition.IsPartition π ∧
          IsHenstock π ∧
            IsSubordinate π r ∧
              (∀ (J : Box ι), J ∈ π → ∃ m, ∀ (i : ι), upper J i - lower J i = (upper J' i - lower J' i) / 2 ^ m) ∧
                TaggedPrepartition.distortion π = distortion J'
⊢ ∃ π,
    TaggedPrepartition.IsPartition π ∧
      IsHenstock π ∧
        IsSubordinate π r ∧
          (∀ (J_1 : Box ι), J_1 ∈ π → ∃ m, ∀ (i : ι), upper J_1 i - lower J_1 i = (upper J i - lower J i) / 2 ^ m) ∧
            TaggedPrepartition.distortion π = distortion J
[PROOFSTEP]
choose! πi hP hHen hr Hn _ using hJ
[GOAL]
case refine'_1
ι : Type u_1
inst✝ : Fintype ι
I✝ J✝ I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
J : Box ι
x✝ : J ≤ I
πi : (J' : Box ι) → TaggedPrepartition J'
hP : ∀ (J' : Box ι), J' ∈ splitCenter J → TaggedPrepartition.IsPartition (πi J')
hHen : ∀ (J' : Box ι), J' ∈ splitCenter J → IsHenstock (πi J')
hr : ∀ (J' : Box ι), J' ∈ splitCenter J → IsSubordinate (πi J') r
Hn :
  ∀ (J' : Box ι),
    J' ∈ splitCenter J →
      ∀ (J : Box ι), J ∈ πi J' → ∃ m, ∀ (i : ι), upper J i - lower J i = (upper J' i - lower J' i) / 2 ^ m
✝ : ∀ (J' : Box ι), J' ∈ splitCenter J → TaggedPrepartition.distortion (πi J') = distortion J'
⊢ ∃ π,
    TaggedPrepartition.IsPartition π ∧
      IsHenstock π ∧
        IsSubordinate π r ∧
          (∀ (J_1 : Box ι), J_1 ∈ π → ∃ m, ∀ (i : ι), upper J_1 i - lower J_1 i = (upper J i - lower J i) / 2 ^ m) ∧
            TaggedPrepartition.distortion π = distortion J
[PROOFSTEP]
choose! n hn using Hn
[GOAL]
case refine'_1
ι : Type u_1
inst✝ : Fintype ι
I✝ J✝ I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
J : Box ι
x✝ : J ≤ I
πi : (J' : Box ι) → TaggedPrepartition J'
hP : ∀ (J' : Box ι), J' ∈ splitCenter J → TaggedPrepartition.IsPartition (πi J')
hHen : ∀ (J' : Box ι), J' ∈ splitCenter J → IsHenstock (πi J')
hr : ∀ (J' : Box ι), J' ∈ splitCenter J → IsSubordinate (πi J') r
✝ : ∀ (J' : Box ι), J' ∈ splitCenter J → TaggedPrepartition.distortion (πi J') = distortion J'
n : Box ι → Box ι → ℕ
hn :
  ∀ (J' : Box ι),
    J' ∈ splitCenter J →
      ∀ (J : Box ι), J ∈ πi J' → ∀ (i : ι), upper J i - lower J i = (upper J' i - lower J' i) / 2 ^ n J' J
⊢ ∃ π,
    TaggedPrepartition.IsPartition π ∧
      IsHenstock π ∧
        IsSubordinate π r ∧
          (∀ (J_1 : Box ι), J_1 ∈ π → ∃ m, ∀ (i : ι), upper J_1 i - lower J_1 i = (upper J i - lower J i) / 2 ^ m) ∧
            TaggedPrepartition.distortion π = distortion J
[PROOFSTEP]
have hP : ((splitCenter J).biUnionTagged πi).IsPartition := (isPartition_splitCenter _).biUnionTagged hP
[GOAL]
case refine'_1
ι : Type u_1
inst✝ : Fintype ι
I✝ J✝ I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
J : Box ι
x✝ : J ≤ I
πi : (J' : Box ι) → TaggedPrepartition J'
hP✝ : ∀ (J' : Box ι), J' ∈ splitCenter J → TaggedPrepartition.IsPartition (πi J')
hHen : ∀ (J' : Box ι), J' ∈ splitCenter J → IsHenstock (πi J')
hr : ∀ (J' : Box ι), J' ∈ splitCenter J → IsSubordinate (πi J') r
✝ : ∀ (J' : Box ι), J' ∈ splitCenter J → TaggedPrepartition.distortion (πi J') = distortion J'
n : Box ι → Box ι → ℕ
hn :
  ∀ (J' : Box ι),
    J' ∈ splitCenter J →
      ∀ (J : Box ι), J ∈ πi J' → ∀ (i : ι), upper J i - lower J i = (upper J' i - lower J' i) / 2 ^ n J' J
hP : TaggedPrepartition.IsPartition (biUnionTagged (splitCenter J) πi)
⊢ ∃ π,
    TaggedPrepartition.IsPartition π ∧
      IsHenstock π ∧
        IsSubordinate π r ∧
          (∀ (J_1 : Box ι), J_1 ∈ π → ∃ m, ∀ (i : ι), upper J_1 i - lower J_1 i = (upper J i - lower J i) / 2 ^ m) ∧
            TaggedPrepartition.distortion π = distortion J
[PROOFSTEP]
have hsub :
  ∀ J' ∈ (splitCenter J).biUnionTagged πi,
    ∃ n : ℕ, ∀ i, (J' : _).upper i - J'.lower i = (J.upper i - J.lower i) / 2 ^ n :=
  by
  intro J' hJ'
  rcases(splitCenter J).mem_biUnionTagged.1 hJ' with ⟨J₁, h₁, h₂⟩
  refine' ⟨n J₁ J' + 1, fun i => _⟩
  simp only [hn J₁ h₁ J' h₂, upper_sub_lower_of_mem_splitCenter h₁, pow_succ, div_div]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J✝ I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
J : Box ι
x✝ : J ≤ I
πi : (J' : Box ι) → TaggedPrepartition J'
hP✝ : ∀ (J' : Box ι), J' ∈ splitCenter J → TaggedPrepartition.IsPartition (πi J')
hHen : ∀ (J' : Box ι), J' ∈ splitCenter J → IsHenstock (πi J')
hr : ∀ (J' : Box ι), J' ∈ splitCenter J → IsSubordinate (πi J') r
✝ : ∀ (J' : Box ι), J' ∈ splitCenter J → TaggedPrepartition.distortion (πi J') = distortion J'
n : Box ι → Box ι → ℕ
hn :
  ∀ (J' : Box ι),
    J' ∈ splitCenter J →
      ∀ (J : Box ι), J ∈ πi J' → ∀ (i : ι), upper J i - lower J i = (upper J' i - lower J' i) / 2 ^ n J' J
hP : TaggedPrepartition.IsPartition (biUnionTagged (splitCenter J) πi)
⊢ ∀ (J' : Box ι),
    J' ∈ biUnionTagged (splitCenter J) πi → ∃ n, ∀ (i : ι), upper J' i - lower J' i = (upper J i - lower J i) / 2 ^ n
[PROOFSTEP]
intro J' hJ'
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J✝ I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
J : Box ι
x✝ : J ≤ I
πi : (J' : Box ι) → TaggedPrepartition J'
hP✝ : ∀ (J' : Box ι), J' ∈ splitCenter J → TaggedPrepartition.IsPartition (πi J')
hHen : ∀ (J' : Box ι), J' ∈ splitCenter J → IsHenstock (πi J')
hr : ∀ (J' : Box ι), J' ∈ splitCenter J → IsSubordinate (πi J') r
✝ : ∀ (J' : Box ι), J' ∈ splitCenter J → TaggedPrepartition.distortion (πi J') = distortion J'
n : Box ι → Box ι → ℕ
hn :
  ∀ (J' : Box ι),
    J' ∈ splitCenter J →
      ∀ (J : Box ι), J ∈ πi J' → ∀ (i : ι), upper J i - lower J i = (upper J' i - lower J' i) / 2 ^ n J' J
hP : TaggedPrepartition.IsPartition (biUnionTagged (splitCenter J) πi)
J' : Box ι
hJ' : J' ∈ biUnionTagged (splitCenter J) πi
⊢ ∃ n, ∀ (i : ι), upper J' i - lower J' i = (upper J i - lower J i) / 2 ^ n
[PROOFSTEP]
rcases(splitCenter J).mem_biUnionTagged.1 hJ' with ⟨J₁, h₁, h₂⟩
[GOAL]
case intro.intro
ι : Type u_1
inst✝ : Fintype ι
I✝ J✝ I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
J : Box ι
x✝ : J ≤ I
πi : (J' : Box ι) → TaggedPrepartition J'
hP✝ : ∀ (J' : Box ι), J' ∈ splitCenter J → TaggedPrepartition.IsPartition (πi J')
hHen : ∀ (J' : Box ι), J' ∈ splitCenter J → IsHenstock (πi J')
hr : ∀ (J' : Box ι), J' ∈ splitCenter J → IsSubordinate (πi J') r
✝ : ∀ (J' : Box ι), J' ∈ splitCenter J → TaggedPrepartition.distortion (πi J') = distortion J'
n : Box ι → Box ι → ℕ
hn :
  ∀ (J' : Box ι),
    J' ∈ splitCenter J →
      ∀ (J : Box ι), J ∈ πi J' → ∀ (i : ι), upper J i - lower J i = (upper J' i - lower J' i) / 2 ^ n J' J
hP : TaggedPrepartition.IsPartition (biUnionTagged (splitCenter J) πi)
J' : Box ι
hJ' : J' ∈ biUnionTagged (splitCenter J) πi
J₁ : Box ι
h₁ : J₁ ∈ splitCenter J
h₂ : J' ∈ πi J₁
⊢ ∃ n, ∀ (i : ι), upper J' i - lower J' i = (upper J i - lower J i) / 2 ^ n
[PROOFSTEP]
refine' ⟨n J₁ J' + 1, fun i => _⟩
[GOAL]
case intro.intro
ι : Type u_1
inst✝ : Fintype ι
I✝ J✝ I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
J : Box ι
x✝ : J ≤ I
πi : (J' : Box ι) → TaggedPrepartition J'
hP✝ : ∀ (J' : Box ι), J' ∈ splitCenter J → TaggedPrepartition.IsPartition (πi J')
hHen : ∀ (J' : Box ι), J' ∈ splitCenter J → IsHenstock (πi J')
hr : ∀ (J' : Box ι), J' ∈ splitCenter J → IsSubordinate (πi J') r
✝ : ∀ (J' : Box ι), J' ∈ splitCenter J → TaggedPrepartition.distortion (πi J') = distortion J'
n : Box ι → Box ι → ℕ
hn :
  ∀ (J' : Box ι),
    J' ∈ splitCenter J →
      ∀ (J : Box ι), J ∈ πi J' → ∀ (i : ι), upper J i - lower J i = (upper J' i - lower J' i) / 2 ^ n J' J
hP : TaggedPrepartition.IsPartition (biUnionTagged (splitCenter J) πi)
J' : Box ι
hJ' : J' ∈ biUnionTagged (splitCenter J) πi
J₁ : Box ι
h₁ : J₁ ∈ splitCenter J
h₂ : J' ∈ πi J₁
i : ι
⊢ upper J' i - lower J' i = (upper J i - lower J i) / 2 ^ (n J₁ J' + 1)
[PROOFSTEP]
simp only [hn J₁ h₁ J' h₂, upper_sub_lower_of_mem_splitCenter h₁, pow_succ, div_div]
[GOAL]
case refine'_1
ι : Type u_1
inst✝ : Fintype ι
I✝ J✝ I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
J : Box ι
x✝ : J ≤ I
πi : (J' : Box ι) → TaggedPrepartition J'
hP✝ : ∀ (J' : Box ι), J' ∈ splitCenter J → TaggedPrepartition.IsPartition (πi J')
hHen : ∀ (J' : Box ι), J' ∈ splitCenter J → IsHenstock (πi J')
hr : ∀ (J' : Box ι), J' ∈ splitCenter J → IsSubordinate (πi J') r
✝ : ∀ (J' : Box ι), J' ∈ splitCenter J → TaggedPrepartition.distortion (πi J') = distortion J'
n : Box ι → Box ι → ℕ
hn :
  ∀ (J' : Box ι),
    J' ∈ splitCenter J →
      ∀ (J : Box ι), J ∈ πi J' → ∀ (i : ι), upper J i - lower J i = (upper J' i - lower J' i) / 2 ^ n J' J
hP : TaggedPrepartition.IsPartition (biUnionTagged (splitCenter J) πi)
hsub :
  ∀ (J' : Box ι),
    J' ∈ biUnionTagged (splitCenter J) πi → ∃ n, ∀ (i : ι), upper J' i - lower J' i = (upper J i - lower J i) / 2 ^ n
⊢ ∃ π,
    TaggedPrepartition.IsPartition π ∧
      IsHenstock π ∧
        IsSubordinate π r ∧
          (∀ (J_1 : Box ι), J_1 ∈ π → ∃ m, ∀ (i : ι), upper J_1 i - lower J_1 i = (upper J i - lower J i) / 2 ^ m) ∧
            TaggedPrepartition.distortion π = distortion J
[PROOFSTEP]
refine' ⟨_, hP, isHenstock_biUnionTagged.2 hHen, isSubordinate_biUnionTagged.2 hr, hsub, _⟩
[GOAL]
case refine'_1
ι : Type u_1
inst✝ : Fintype ι
I✝ J✝ I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
J : Box ι
x✝ : J ≤ I
πi : (J' : Box ι) → TaggedPrepartition J'
hP✝ : ∀ (J' : Box ι), J' ∈ splitCenter J → TaggedPrepartition.IsPartition (πi J')
hHen : ∀ (J' : Box ι), J' ∈ splitCenter J → IsHenstock (πi J')
hr : ∀ (J' : Box ι), J' ∈ splitCenter J → IsSubordinate (πi J') r
✝ : ∀ (J' : Box ι), J' ∈ splitCenter J → TaggedPrepartition.distortion (πi J') = distortion J'
n : Box ι → Box ι → ℕ
hn :
  ∀ (J' : Box ι),
    J' ∈ splitCenter J →
      ∀ (J : Box ι), J ∈ πi J' → ∀ (i : ι), upper J i - lower J i = (upper J' i - lower J' i) / 2 ^ n J' J
hP : TaggedPrepartition.IsPartition (biUnionTagged (splitCenter J) πi)
hsub :
  ∀ (J' : Box ι),
    J' ∈ biUnionTagged (splitCenter J) πi → ∃ n, ∀ (i : ι), upper J' i - lower J' i = (upper J i - lower J i) / 2 ^ n
⊢ TaggedPrepartition.distortion (biUnionTagged (splitCenter J) πi) = distortion J
[PROOFSTEP]
refine' TaggedPrepartition.distortion_of_const _ hP.nonempty_boxes fun J' h' => _
[GOAL]
case refine'_1
ι : Type u_1
inst✝ : Fintype ι
I✝ J✝ I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
J : Box ι
x✝ : J ≤ I
πi : (J' : Box ι) → TaggedPrepartition J'
hP✝ : ∀ (J' : Box ι), J' ∈ splitCenter J → TaggedPrepartition.IsPartition (πi J')
hHen : ∀ (J' : Box ι), J' ∈ splitCenter J → IsHenstock (πi J')
hr : ∀ (J' : Box ι), J' ∈ splitCenter J → IsSubordinate (πi J') r
✝ : ∀ (J' : Box ι), J' ∈ splitCenter J → TaggedPrepartition.distortion (πi J') = distortion J'
n : Box ι → Box ι → ℕ
hn :
  ∀ (J' : Box ι),
    J' ∈ splitCenter J →
      ∀ (J : Box ι), J ∈ πi J' → ∀ (i : ι), upper J i - lower J i = (upper J' i - lower J' i) / 2 ^ n J' J
hP : TaggedPrepartition.IsPartition (biUnionTagged (splitCenter J) πi)
hsub :
  ∀ (J' : Box ι),
    J' ∈ biUnionTagged (splitCenter J) πi → ∃ n, ∀ (i : ι), upper J' i - lower J' i = (upper J i - lower J i) / 2 ^ n
J' : Box ι
h' : J' ∈ biUnionTagged (splitCenter J) πi
⊢ distortion J' = distortion J
[PROOFSTEP]
rcases hsub J' h' with ⟨n, hn⟩
[GOAL]
case refine'_1.intro
ι : Type u_1
inst✝ : Fintype ι
I✝ J✝ I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
J : Box ι
x✝ : J ≤ I
πi : (J' : Box ι) → TaggedPrepartition J'
hP✝ : ∀ (J' : Box ι), J' ∈ splitCenter J → TaggedPrepartition.IsPartition (πi J')
hHen : ∀ (J' : Box ι), J' ∈ splitCenter J → IsHenstock (πi J')
hr : ∀ (J' : Box ι), J' ∈ splitCenter J → IsSubordinate (πi J') r
✝ : ∀ (J' : Box ι), J' ∈ splitCenter J → TaggedPrepartition.distortion (πi J') = distortion J'
n✝ : Box ι → Box ι → ℕ
hn✝ :
  ∀ (J' : Box ι),
    J' ∈ splitCenter J →
      ∀ (J : Box ι), J ∈ πi J' → ∀ (i : ι), upper J i - lower J i = (upper J' i - lower J' i) / 2 ^ n✝ J' J
hP : TaggedPrepartition.IsPartition (biUnionTagged (splitCenter J) πi)
hsub :
  ∀ (J' : Box ι),
    J' ∈ biUnionTagged (splitCenter J) πi → ∃ n, ∀ (i : ι), upper J' i - lower J' i = (upper J i - lower J i) / 2 ^ n
J' : Box ι
h' : J' ∈ biUnionTagged (splitCenter J) πi
n : ℕ
hn : ∀ (i : ι), upper J' i - lower J' i = (upper J i - lower J i) / 2 ^ n
⊢ distortion J' = distortion J
[PROOFSTEP]
exact Box.distortion_eq_of_sub_eq_div hn
[GOAL]
case refine'_2
ι : Type u_1
inst✝ : Fintype ι
I✝ J I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
z : ι → ℝ
x✝ : z ∈ ↑Box.Icc I
⊢ ∃ U,
    U ∈ 𝓝[↑Box.Icc I] z ∧
      ∀ (J : Box ι),
        J ≤ I →
          ∀ (m : ℕ),
            z ∈ ↑Box.Icc J →
              ↑Box.Icc J ⊆ U →
                (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) →
                  ∃ π,
                    TaggedPrepartition.IsPartition π ∧
                      IsHenstock π ∧
                        IsSubordinate π r ∧
                          (∀ (J_1 : Box ι),
                              J_1 ∈ π → ∃ m, ∀ (i : ι), upper J_1 i - lower J_1 i = (upper J i - lower J i) / 2 ^ m) ∧
                            TaggedPrepartition.distortion π = distortion J
[PROOFSTEP]
refine' ⟨Box.Icc I ∩ closedBall z (r z), inter_mem_nhdsWithin _ (closedBall_mem_nhds _ (r z).coe_prop), _⟩
[GOAL]
case refine'_2
ι : Type u_1
inst✝ : Fintype ι
I✝ J I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
z : ι → ℝ
x✝ : z ∈ ↑Box.Icc I
⊢ ∀ (J : Box ι),
    J ≤ I →
      ∀ (m : ℕ),
        z ∈ ↑Box.Icc J →
          ↑Box.Icc J ⊆ ↑Box.Icc I ∩ closedBall z ↑(r z) →
            (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) →
              ∃ π,
                TaggedPrepartition.IsPartition π ∧
                  IsHenstock π ∧
                    IsSubordinate π r ∧
                      (∀ (J_1 : Box ι),
                          J_1 ∈ π → ∃ m, ∀ (i : ι), upper J_1 i - lower J_1 i = (upper J i - lower J i) / 2 ^ m) ∧
                        TaggedPrepartition.distortion π = distortion J
[PROOFSTEP]
intro J _ n Hmem HIcc Hsub
[GOAL]
case refine'_2
ι : Type u_1
inst✝ : Fintype ι
I✝ J✝ I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
z : ι → ℝ
x✝ : z ∈ ↑Box.Icc I
J : Box ι
a✝ : J ≤ I
n : ℕ
Hmem : z ∈ ↑Box.Icc J
HIcc : ↑Box.Icc J ⊆ ↑Box.Icc I ∩ closedBall z ↑(r z)
Hsub : ∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ n
⊢ ∃ π,
    TaggedPrepartition.IsPartition π ∧
      IsHenstock π ∧
        IsSubordinate π r ∧
          (∀ (J_1 : Box ι), J_1 ∈ π → ∃ m, ∀ (i : ι), upper J_1 i - lower J_1 i = (upper J i - lower J i) / 2 ^ m) ∧
            TaggedPrepartition.distortion π = distortion J
[PROOFSTEP]
rw [Set.subset_inter_iff] at HIcc
[GOAL]
case refine'_2
ι : Type u_1
inst✝ : Fintype ι
I✝ J✝ I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
z : ι → ℝ
x✝ : z ∈ ↑Box.Icc I
J : Box ι
a✝ : J ≤ I
n : ℕ
Hmem : z ∈ ↑Box.Icc J
HIcc : ↑Box.Icc J ⊆ ↑Box.Icc I ∧ ↑Box.Icc J ⊆ closedBall z ↑(r z)
Hsub : ∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ n
⊢ ∃ π,
    TaggedPrepartition.IsPartition π ∧
      IsHenstock π ∧
        IsSubordinate π r ∧
          (∀ (J_1 : Box ι), J_1 ∈ π → ∃ m, ∀ (i : ι), upper J_1 i - lower J_1 i = (upper J i - lower J i) / 2 ^ m) ∧
            TaggedPrepartition.distortion π = distortion J
[PROOFSTEP]
refine'
  ⟨single _ _ le_rfl _ Hmem, isPartition_single _, isHenstock_single _, (isSubordinate_single _ _).2 HIcc.2, _,
    distortion_single _ _⟩
[GOAL]
case refine'_2
ι : Type u_1
inst✝ : Fintype ι
I✝ J✝ I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
z : ι → ℝ
x✝ : z ∈ ↑Box.Icc I
J : Box ι
a✝ : J ≤ I
n : ℕ
Hmem : z ∈ ↑Box.Icc J
HIcc : ↑Box.Icc J ⊆ ↑Box.Icc I ∧ ↑Box.Icc J ⊆ closedBall z ↑(r z)
Hsub : ∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ n
⊢ ∀ (J_1 : Box ι),
    J_1 ∈ TaggedPrepartition.single J J (_ : J ≤ J) z Hmem →
      ∃ m, ∀ (i : ι), upper J_1 i - lower J_1 i = (upper J i - lower J i) / 2 ^ m
[PROOFSTEP]
simp only [TaggedPrepartition.mem_single, forall_eq]
[GOAL]
case refine'_2
ι : Type u_1
inst✝ : Fintype ι
I✝ J✝ I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
z : ι → ℝ
x✝ : z ∈ ↑Box.Icc I
J : Box ι
a✝ : J ≤ I
n : ℕ
Hmem : z ∈ ↑Box.Icc J
HIcc : ↑Box.Icc J ⊆ ↑Box.Icc I ∧ ↑Box.Icc J ⊆ closedBall z ↑(r z)
Hsub : ∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ n
⊢ ∃ m, ∀ (i : ι), upper J i - lower J i = (upper J i - lower J i) / 2 ^ m
[PROOFSTEP]
refine' ⟨0, fun i => _⟩
[GOAL]
case refine'_2
ι : Type u_1
inst✝ : Fintype ι
I✝ J✝ I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
z : ι → ℝ
x✝ : z ∈ ↑Box.Icc I
J : Box ι
a✝ : J ≤ I
n : ℕ
Hmem : z ∈ ↑Box.Icc J
HIcc : ↑Box.Icc J ⊆ ↑Box.Icc I ∧ ↑Box.Icc J ⊆ closedBall z ↑(r z)
Hsub : ∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ n
i : ι
⊢ upper J i - lower J i = (upper J i - lower J i) / 2 ^ 0
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J I : Box ι
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : Prepartition I
⊢ ∃ π',
    π'.toPrepartition ≤ π ∧
      IsHenstock π' ∧
        IsSubordinate π' r ∧
          TaggedPrepartition.distortion π' = distortion π ∧ TaggedPrepartition.iUnion π' = Prepartition.iUnion π
[PROOFSTEP]
have := fun J => Box.exists_taggedPartition_isHenstock_isSubordinate_homothetic J r
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J I : Box ι
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : Prepartition I
this :
  ∀ (J : Box ι),
    ∃ π,
      TaggedPrepartition.IsPartition π ∧
        IsHenstock π ∧
          IsSubordinate π r ∧
            (∀ (J_1 : Box ι),
                J_1 ∈ π → ∃ m, ∀ (i : ι), Box.upper J_1 i - Box.lower J_1 i = (Box.upper J i - Box.lower J i) / 2 ^ m) ∧
              TaggedPrepartition.distortion π = Box.distortion J
⊢ ∃ π',
    π'.toPrepartition ≤ π ∧
      IsHenstock π' ∧
        IsSubordinate π' r ∧
          TaggedPrepartition.distortion π' = distortion π ∧ TaggedPrepartition.iUnion π' = Prepartition.iUnion π
[PROOFSTEP]
choose! πi πip πiH πir _ πid using this
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J I : Box ι
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
πip : ∀ (J : Box ι), TaggedPrepartition.IsPartition (πi J)
πiH : ∀ (J : Box ι), IsHenstock (πi J)
πir : ∀ (J : Box ι), IsSubordinate (πi J) r
h✝ :
  ∀ (J J_1 : Box ι),
    J_1 ∈ πi J → ∃ m, ∀ (i : ι), Box.upper J_1 i - Box.lower J_1 i = (Box.upper J i - Box.lower J i) / 2 ^ m
πid : ∀ (J : Box ι), TaggedPrepartition.distortion (πi J) = Box.distortion J
⊢ ∃ π',
    π'.toPrepartition ≤ π ∧
      IsHenstock π' ∧
        IsSubordinate π' r ∧
          TaggedPrepartition.distortion π' = distortion π ∧ TaggedPrepartition.iUnion π' = Prepartition.iUnion π
[PROOFSTEP]
refine'
  ⟨π.biUnionTagged πi, biUnion_le _ _, isHenstock_biUnionTagged.2 fun J _ => πiH J,
    isSubordinate_biUnionTagged.2 fun J _ => πir J, _, π.iUnion_biUnion_partition fun J _ => πip J⟩
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J I : Box ι
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
πip : ∀ (J : Box ι), TaggedPrepartition.IsPartition (πi J)
πiH : ∀ (J : Box ι), IsHenstock (πi J)
πir : ∀ (J : Box ι), IsSubordinate (πi J) r
h✝ :
  ∀ (J J_1 : Box ι),
    J_1 ∈ πi J → ∃ m, ∀ (i : ι), Box.upper J_1 i - Box.lower J_1 i = (Box.upper J i - Box.lower J i) / 2 ^ m
πid : ∀ (J : Box ι), TaggedPrepartition.distortion (πi J) = Box.distortion J
⊢ TaggedPrepartition.distortion (biUnionTagged π πi) = distortion π
[PROOFSTEP]
rw [distortion_biUnionTagged]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I✝ J I : Box ι
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
πip : ∀ (J : Box ι), TaggedPrepartition.IsPartition (πi J)
πiH : ∀ (J : Box ι), IsHenstock (πi J)
πir : ∀ (J : Box ι), IsSubordinate (πi J) r
h✝ :
  ∀ (J J_1 : Box ι),
    J_1 ∈ πi J → ∃ m, ∀ (i : ι), Box.upper J_1 i - Box.lower J_1 i = (Box.upper J i - Box.lower J i) / 2 ^ m
πid : ∀ (J : Box ι), TaggedPrepartition.distortion (πi J) = Box.distortion J
⊢ (sup π.boxes fun J => TaggedPrepartition.distortion (πi J)) = distortion π
[PROOFSTEP]
exact sup_congr rfl fun J _ => πid J
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I J : Box ι
π₁ : TaggedPrepartition I
π₂ : Prepartition I
hU : Prepartition.iUnion π₂ = ↑I \ iUnion π₁
r : (ι → ℝ) → ↑(Ioi 0)
⊢ distortion (unionComplToSubordinate π₁ π₂ hU r) = max (distortion π₁) (Prepartition.distortion π₂)
[PROOFSTEP]
simp [unionComplToSubordinate]


[GOAL]
ι : Type u_1
I✝ J I : Box ι
s : Set ι
i : ι
⊢ Set.piecewise s (fun i => (lower I i + upper I i) / 2) I.lower i <
    Set.piecewise s I.upper (fun i => (lower I i + upper I i) / 2) i
[PROOFSTEP]
dsimp only [Set.piecewise]
[GOAL]
ι : Type u_1
I✝ J I : Box ι
s : Set ι
i : ι
⊢ (if i ∈ s then (lower I i + upper I i) / 2 else lower I i) < if i ∈ s then upper I i else (lower I i + upper I i) / 2
[PROOFSTEP]
split_ifs
[GOAL]
case pos
ι : Type u_1
I✝ J I : Box ι
s : Set ι
i : ι
h✝ : i ∈ s
⊢ (lower I i + upper I i) / 2 < upper I i
[PROOFSTEP]
simp only [left_lt_add_div_two, add_div_two_lt_right, I.lower_lt_upper]
[GOAL]
case neg
ι : Type u_1
I✝ J I : Box ι
s : Set ι
i : ι
h✝ : ¬i ∈ s
⊢ lower I i < (lower I i + upper I i) / 2
[PROOFSTEP]
simp only [left_lt_add_div_two, add_div_two_lt_right, I.lower_lt_upper]
[GOAL]
ι : Type u_1
I J : Box ι
s : Set ι
y : ι → ℝ
⊢ y ∈ splitCenterBox I s ↔ y ∈ I ∧ ∀ (i : ι), (lower I i + upper I i) / 2 < y i ↔ i ∈ s
[PROOFSTEP]
simp only [splitCenterBox, mem_def, ← forall_and]
[GOAL]
ι : Type u_1
I J : Box ι
s : Set ι
y : ι → ℝ
⊢ (∀ (i : ι),
      y i ∈
        Set.Ioc (Set.piecewise s (fun i => (lower I i + upper I i) / 2) I.lower i)
          (Set.piecewise s I.upper (fun i => (lower I i + upper I i) / 2) i)) ↔
    ∀ (x : ι), y x ∈ Set.Ioc (lower I x) (upper I x) ∧ ((lower I x + upper I x) / 2 < y x ↔ x ∈ s)
[PROOFSTEP]
refine' forall_congr' fun i ↦ _
[GOAL]
ι : Type u_1
I J : Box ι
s : Set ι
y : ι → ℝ
i : ι
⊢ y i ∈
      Set.Ioc (Set.piecewise s (fun i => (lower I i + upper I i) / 2) I.lower i)
        (Set.piecewise s I.upper (fun i => (lower I i + upper I i) / 2) i) ↔
    y i ∈ Set.Ioc (lower I i) (upper I i) ∧ ((lower I i + upper I i) / 2 < y i ↔ i ∈ s)
[PROOFSTEP]
dsimp only [Set.piecewise]
[GOAL]
ι : Type u_1
I J : Box ι
s : Set ι
y : ι → ℝ
i : ι
⊢ y i ∈
      Set.Ioc (if i ∈ s then (lower I i + upper I i) / 2 else lower I i)
        (if i ∈ s then upper I i else (lower I i + upper I i) / 2) ↔
    y i ∈ Set.Ioc (lower I i) (upper I i) ∧ ((lower I i + upper I i) / 2 < y i ↔ i ∈ s)
[PROOFSTEP]
split_ifs with hs
[GOAL]
case pos
ι : Type u_1
I J : Box ι
s : Set ι
y : ι → ℝ
i : ι
hs : i ∈ s
⊢ y i ∈ Set.Ioc ((lower I i + upper I i) / 2) (upper I i) ↔
    y i ∈ Set.Ioc (lower I i) (upper I i) ∧ ((lower I i + upper I i) / 2 < y i ↔ i ∈ s)
[PROOFSTEP]
simp only [hs, iff_true_iff, iff_false_iff, not_lt]
[GOAL]
case neg
ι : Type u_1
I J : Box ι
s : Set ι
y : ι → ℝ
i : ι
hs : ¬i ∈ s
⊢ y i ∈ Set.Ioc (lower I i) ((lower I i + upper I i) / 2) ↔
    y i ∈ Set.Ioc (lower I i) (upper I i) ∧ ((lower I i + upper I i) / 2 < y i ↔ i ∈ s)
[PROOFSTEP]
simp only [hs, iff_true_iff, iff_false_iff, not_lt]
[GOAL]
case pos
ι : Type u_1
I J : Box ι
s : Set ι
y : ι → ℝ
i : ι
hs : i ∈ s
⊢ y i ∈ Set.Ioc ((lower I i + upper I i) / 2) (upper I i) ↔
    y i ∈ Set.Ioc (lower I i) (upper I i) ∧ (lower I i + upper I i) / 2 < y i
case neg
ι : Type u_1
I J : Box ι
s : Set ι
y : ι → ℝ
i : ι
hs : ¬i ∈ s
⊢ y i ∈ Set.Ioc (lower I i) ((lower I i + upper I i) / 2) ↔
    y i ∈ Set.Ioc (lower I i) (upper I i) ∧ y i ≤ (lower I i + upper I i) / 2
[PROOFSTEP]
exacts [⟨fun H ↦ ⟨⟨(left_lt_add_div_two.2 (I.lower_lt_upper i)).trans H.1, H.2⟩, H.1⟩, fun H ↦ ⟨H.2, H.1.2⟩⟩,
  ⟨fun H ↦ ⟨⟨H.1, H.2.trans (add_div_two_lt_right.2 (I.lower_lt_upper i)).le⟩, H.2⟩, fun H ↦ ⟨H.1.1, H.2⟩⟩]
[GOAL]
ι : Type u_1
I✝ J I : Box ι
s t : Set ι
h : s ≠ t
⊢ Disjoint ↑(splitCenterBox I s) ↑(splitCenterBox I t)
[PROOFSTEP]
rw [disjoint_iff_inf_le]
[GOAL]
ι : Type u_1
I✝ J I : Box ι
s t : Set ι
h : s ≠ t
⊢ ↑(splitCenterBox I s) ⊓ ↑(splitCenterBox I t) ≤ ⊥
[PROOFSTEP]
rintro y ⟨hs, ht⟩
[GOAL]
case intro
ι : Type u_1
I✝ J I : Box ι
s t : Set ι
h : s ≠ t
y : ι → ℝ
hs : y ∈ ↑(splitCenterBox I s)
ht : y ∈ ↑(splitCenterBox I t)
⊢ y ∈ ⊥
[PROOFSTEP]
apply h
[GOAL]
case intro
ι : Type u_1
I✝ J I : Box ι
s t : Set ι
h : s ≠ t
y : ι → ℝ
hs : y ∈ ↑(splitCenterBox I s)
ht : y ∈ ↑(splitCenterBox I t)
⊢ s = t
[PROOFSTEP]
ext i
[GOAL]
case intro.h
ι : Type u_1
I✝ J I : Box ι
s t : Set ι
h : s ≠ t
y : ι → ℝ
hs : y ∈ ↑(splitCenterBox I s)
ht : y ∈ ↑(splitCenterBox I t)
i : ι
⊢ i ∈ s ↔ i ∈ t
[PROOFSTEP]
rw [mem_coe, mem_splitCenterBox] at hs ht
[GOAL]
case intro.h
ι : Type u_1
I✝ J I : Box ι
s t : Set ι
h : s ≠ t
y : ι → ℝ
hs : y ∈ I ∧ ∀ (i : ι), (lower I i + upper I i) / 2 < y i ↔ i ∈ s
ht : y ∈ I ∧ ∀ (i : ι), (lower I i + upper I i) / 2 < y i ↔ i ∈ t
i : ι
⊢ i ∈ s ↔ i ∈ t
[PROOFSTEP]
rw [← hs.2, ← ht.2]
[GOAL]
ι : Type u_1
I✝ J I : Box ι
⊢ ⋃ (s : Set ι), ↑(splitCenterBox I s) = ↑I
[PROOFSTEP]
ext x
[GOAL]
case h
ι : Type u_1
I✝ J I : Box ι
x : ι → ℝ
⊢ x ∈ ⋃ (s : Set ι), ↑(splitCenterBox I s) ↔ x ∈ ↑I
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
I✝ J I : Box ι
s : Set ι
i : ι
⊢ upper (splitCenterBox I s) i - lower (splitCenterBox I s) i = (upper I i - lower I i) / 2
[PROOFSTEP]
by_cases i ∈ s
[GOAL]
ι : Type u_1
I✝ J I : Box ι
s : Set ι
i : ι
⊢ upper (splitCenterBox I s) i - lower (splitCenterBox I s) i = (upper I i - lower I i) / 2
[PROOFSTEP]
by_cases i ∈ s
[GOAL]
case pos
ι : Type u_1
I✝ J I : Box ι
s : Set ι
i : ι
h : i ∈ s
⊢ upper (splitCenterBox I s) i - lower (splitCenterBox I s) i = (upper I i - lower I i) / 2
[PROOFSTEP]
field_simp [splitCenterBox]
[GOAL]
case neg
ι : Type u_1
I✝ J I : Box ι
s : Set ι
i : ι
h : ¬i ∈ s
⊢ upper (splitCenterBox I s) i - lower (splitCenterBox I s) i = (upper I i - lower I i) / 2
[PROOFSTEP]
field_simp [splitCenterBox]
[GOAL]
case pos
ι : Type u_1
I✝ J I : Box ι
s : Set ι
i : ι
h : i ∈ s
⊢ upper I i * 2 - (lower I i + upper I i) = upper I i - lower I i
[PROOFSTEP]
field_simp [mul_two, two_mul]
[GOAL]
case neg
ι : Type u_1
I✝ J I : Box ι
s : Set ι
i : ι
h : ¬i ∈ s
⊢ lower I i + upper I i - 2 * lower I i = upper I i - lower I i
[PROOFSTEP]
field_simp [mul_two, two_mul]
[GOAL]
ι : Type u_1
I✝ J : Box ι
p : Box ι → Prop
I : Box ι
H_ind : ∀ (J : Box ι), J ≤ I → (∀ (s : Set ι), p (splitCenterBox J s)) → p J
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
⊢ p I
[PROOFSTEP]
by_contra hpI
[GOAL]
ι : Type u_1
I✝ J : Box ι
p : Box ι → Prop
I : Box ι
H_ind : ∀ (J : Box ι), J ≤ I → (∀ (s : Set ι), p (splitCenterBox J s)) → p J
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
⊢ False
[PROOFSTEP]
replace H_ind := fun J hJ ↦ not_imp_not.2 (H_ind J hJ)
[GOAL]
ι : Type u_1
I✝ J : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
H_ind : ∀ (J : Box ι), J ≤ I → ¬p J → ¬∀ (s : Set ι), p (splitCenterBox J s)
⊢ False
[PROOFSTEP]
simp only [exists_imp, not_forall] at H_ind
[GOAL]
ι : Type u_1
I✝ J : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
H_ind : ∀ (J : Box ι), J ≤ I → ¬p J → ∃ x, ¬p (splitCenterBox J x)
⊢ False
[PROOFSTEP]
choose! s hs using H_ind
[GOAL]
ι : Type u_1
I✝ J : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ (J : Box ι), J ≤ I → ¬p J → ¬p (splitCenterBox J (s J))
⊢ False
[PROOFSTEP]
set J : ℕ → Box ι := fun m ↦ (fun J ↦ splitCenterBox J (s J))^[m] I
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ (J : Box ι), J ≤ I → ¬p J → ¬p (splitCenterBox J (s J))
J : ℕ → Box ι := fun m => (fun J => splitCenterBox J (s J))^[m] I
⊢ False
[PROOFSTEP]
have J_succ : ∀ m, J (m + 1) = splitCenterBox (J m) (s <| J m) := fun m ↦
  iterate_succ_apply' _ _
    _
      -- Now we prove some properties of `J`
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ (J : Box ι), J ≤ I → ¬p J → ¬p (splitCenterBox J (s J))
J : ℕ → Box ι := fun m => (fun J => splitCenterBox J (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = splitCenterBox (J m) (s (J m))
⊢ False
[PROOFSTEP]
have hJmono : Antitone J := antitone_nat_of_succ_le fun n ↦ by simpa [J_succ] using splitCenterBox_le _ _
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ (J : Box ι), J ≤ I → ¬p J → ¬p (splitCenterBox J (s J))
J : ℕ → Box ι := fun m => (fun J => splitCenterBox J (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = splitCenterBox (J m) (s (J m))
n : ℕ
⊢ J (n + 1) ≤ J n
[PROOFSTEP]
simpa [J_succ] using splitCenterBox_le _ _
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ (J : Box ι), J ≤ I → ¬p J → ¬p (splitCenterBox J (s J))
J : ℕ → Box ι := fun m => (fun J => splitCenterBox J (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = splitCenterBox (J m) (s (J m))
hJmono : Antitone J
⊢ False
[PROOFSTEP]
have hJle : ∀ m, J m ≤ I := fun m ↦ hJmono (zero_le m)
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ (J : Box ι), J ≤ I → ¬p J → ¬p (splitCenterBox J (s J))
J : ℕ → Box ι := fun m => (fun J => splitCenterBox J (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = splitCenterBox (J m) (s (J m))
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
⊢ False
[PROOFSTEP]
have hJp : ∀ m, ¬p (J m) := fun m ↦ Nat.recOn m hpI fun m ↦ by simpa only [J_succ] using hs (J m) (hJle m)
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ (J : Box ι), J ≤ I → ¬p J → ¬p (splitCenterBox J (s J))
J : ℕ → Box ι := fun m => (fun J => splitCenterBox J (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = splitCenterBox (J m) (s (J m))
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
m✝ m : ℕ
⊢ ¬p (J m) → ¬p (J (Nat.succ m))
[PROOFSTEP]
simpa only [J_succ] using hs (J m) (hJle m)
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ (J : Box ι), J ≤ I → ¬p J → ¬p (splitCenterBox J (s J))
J : ℕ → Box ι := fun m => (fun J => splitCenterBox J (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = splitCenterBox (J m) (s (J m))
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
⊢ False
[PROOFSTEP]
have hJsub : ∀ m i, (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / 2 ^ m :=
  by
  intro m i
  induction' m with m ihm
  · simp [Nat.zero_eq]
  simp only [pow_succ', J_succ, upper_sub_lower_splitCenterBox, ihm, div_div]
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ (J : Box ι), J ≤ I → ¬p J → ¬p (splitCenterBox J (s J))
J : ℕ → Box ι := fun m => (fun J => splitCenterBox J (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = splitCenterBox (J m) (s (J m))
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
⊢ ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
[PROOFSTEP]
intro m i
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ (J : Box ι), J ≤ I → ¬p J → ¬p (splitCenterBox J (s J))
J : ℕ → Box ι := fun m => (fun J => splitCenterBox J (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = splitCenterBox (J m) (s (J m))
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
m : ℕ
i : ι
⊢ upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
[PROOFSTEP]
induction' m with m ihm
[GOAL]
case zero
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ (J : Box ι), J ≤ I → ¬p J → ¬p (splitCenterBox J (s J))
J : ℕ → Box ι := fun m => (fun J => splitCenterBox J (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = splitCenterBox (J m) (s (J m))
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
i : ι
⊢ upper (J Nat.zero) i - lower (J Nat.zero) i = (upper I i - lower I i) / 2 ^ Nat.zero
[PROOFSTEP]
simp [Nat.zero_eq]
[GOAL]
case succ
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ (J : Box ι), J ≤ I → ¬p J → ¬p (splitCenterBox J (s J))
J : ℕ → Box ι := fun m => (fun J => splitCenterBox J (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = splitCenterBox (J m) (s (J m))
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
i : ι
m : ℕ
ihm : upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
⊢ upper (J (Nat.succ m)) i - lower (J (Nat.succ m)) i = (upper I i - lower I i) / 2 ^ Nat.succ m
[PROOFSTEP]
simp only [pow_succ', J_succ, upper_sub_lower_splitCenterBox, ihm, div_div]
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ (J : Box ι), J ≤ I → ¬p J → ¬p (splitCenterBox J (s J))
J : ℕ → Box ι := fun m => (fun J => splitCenterBox J (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = splitCenterBox (J m) (s (J m))
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
⊢ False
[PROOFSTEP]
have h0 : J 0 = I := rfl
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ (J : Box ι), J ≤ I → ¬p J → ¬p (splitCenterBox J (s J))
J : ℕ → Box ι := fun m => (fun J => splitCenterBox J (s J))^[m] I
J_succ : ∀ (m : ℕ), J (m + 1) = splitCenterBox (J m) (s (J m))
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
⊢ False
[PROOFSTEP]
clear_value J
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
hpI : ¬p I
s : Box ι → Set ι
hs : ∀ (J : Box ι), J ≤ I → ¬p J → ¬p (splitCenterBox J (s J))
J : ℕ → Box ι
J_succ : ∀ (m : ℕ), J (m + 1) = splitCenterBox (J m) (s (J m))
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
⊢ False
[PROOFSTEP]
clear hpI hs J_succ s
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
⊢ False
[PROOFSTEP]
set z : ι → ℝ := ⨆ m, (J m).lower
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
⊢ False
[PROOFSTEP]
have hzJ : ∀ m, z ∈ Box.Icc (J m) :=
  mem_iInter.1
    (ciSup_mem_Inter_Icc_of_antitone_Icc ((@Box.Icc ι).monotone.comp_antitone hJmono) fun m ↦ (J m).lower_le_upper)
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), z ∈ ↑Box.Icc (J m)
⊢ False
[PROOFSTEP]
have hJl_mem : ∀ m, (J m).lower ∈ Box.Icc I := fun m ↦ le_iff_Icc.1 (hJle m) (J m).lower_mem_Icc
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), z ∈ ↑Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ ↑Box.Icc I
⊢ False
[PROOFSTEP]
have hJu_mem : ∀ m, (J m).upper ∈ Box.Icc I := fun m ↦ le_iff_Icc.1 (hJle m) (J m).upper_mem_Icc
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), z ∈ ↑Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ ↑Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ ↑Box.Icc I
⊢ False
[PROOFSTEP]
have hJlz : Tendsto (fun m ↦ (J m).lower) atTop (𝓝 z) :=
  tendsto_atTop_ciSup (antitone_lower.comp hJmono) ⟨I.upper, fun x ⟨m, hm⟩ ↦ hm ▸ (hJl_mem m).2⟩
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), z ∈ ↑Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ ↑Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ ↑Box.Icc I
hJlz : Tendsto (fun m => (J m).lower) atTop (𝓝 z)
⊢ False
[PROOFSTEP]
have hJuz : Tendsto (fun m ↦ (J m).upper) atTop (𝓝 z) :=
  by
  suffices Tendsto (fun m ↦ (J m).upper - (J m).lower) atTop (𝓝 0) by simpa using hJlz.add this
  refine' tendsto_pi_nhds.2 fun i ↦ _
  simpa [hJsub] using tendsto_const_nhds.div_atTop (tendsto_pow_atTop_atTop_of_one_lt _root_.one_lt_two)
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), z ∈ ↑Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ ↑Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ ↑Box.Icc I
hJlz : Tendsto (fun m => (J m).lower) atTop (𝓝 z)
⊢ Tendsto (fun m => (J m).upper) atTop (𝓝 z)
[PROOFSTEP]
suffices Tendsto (fun m ↦ (J m).upper - (J m).lower) atTop (𝓝 0) by simpa using hJlz.add this
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), z ∈ ↑Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ ↑Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ ↑Box.Icc I
hJlz : Tendsto (fun m => (J m).lower) atTop (𝓝 z)
this : Tendsto (fun m => (J m).upper - (J m).lower) atTop (𝓝 0)
⊢ Tendsto (fun m => (J m).upper) atTop (𝓝 z)
[PROOFSTEP]
simpa using hJlz.add this
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), z ∈ ↑Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ ↑Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ ↑Box.Icc I
hJlz : Tendsto (fun m => (J m).lower) atTop (𝓝 z)
⊢ Tendsto (fun m => (J m).upper - (J m).lower) atTop (𝓝 0)
[PROOFSTEP]
refine' tendsto_pi_nhds.2 fun i ↦ _
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), z ∈ ↑Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ ↑Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ ↑Box.Icc I
hJlz : Tendsto (fun m => (J m).lower) atTop (𝓝 z)
i : ι
⊢ Tendsto (fun i_1 => ((J i_1).upper - (J i_1).lower) i) atTop (𝓝 (OfNat.ofNat 0 i))
[PROOFSTEP]
simpa [hJsub] using tendsto_const_nhds.div_atTop (tendsto_pow_atTop_atTop_of_one_lt _root_.one_lt_two)
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), z ∈ ↑Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ ↑Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ ↑Box.Icc I
hJlz : Tendsto (fun m => (J m).lower) atTop (𝓝 z)
hJuz : Tendsto (fun m => (J m).upper) atTop (𝓝 z)
⊢ False
[PROOFSTEP]
replace hJlz : Tendsto (fun m ↦ (J m).lower) atTop (𝓝[Icc I.lower I.upper] z)
[GOAL]
case hJlz
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), z ∈ ↑Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ ↑Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ ↑Box.Icc I
hJlz : Tendsto (fun m => (J m).lower) atTop (𝓝 z)
hJuz : Tendsto (fun m => (J m).upper) atTop (𝓝 z)
⊢ Tendsto (fun m => (J m).lower) atTop (𝓝[Set.Icc I.lower I.upper] z)
[PROOFSTEP]
exact tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hJlz (eventually_of_forall hJl_mem)
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), z ∈ ↑Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ ↑Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ ↑Box.Icc I
hJuz : Tendsto (fun m => (J m).upper) atTop (𝓝 z)
hJlz : Tendsto (fun m => (J m).lower) atTop (𝓝[Set.Icc I.lower I.upper] z)
⊢ False
[PROOFSTEP]
replace hJuz : Tendsto (fun m ↦ (J m).upper) atTop (𝓝[Icc I.lower I.upper] z)
[GOAL]
case hJuz
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), z ∈ ↑Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ ↑Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ ↑Box.Icc I
hJuz : Tendsto (fun m => (J m).upper) atTop (𝓝 z)
hJlz : Tendsto (fun m => (J m).lower) atTop (𝓝[Set.Icc I.lower I.upper] z)
⊢ Tendsto (fun m => (J m).upper) atTop (𝓝[Set.Icc I.lower I.upper] z)
[PROOFSTEP]
exact tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hJuz (eventually_of_forall hJu_mem)
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), z ∈ ↑Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ ↑Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ ↑Box.Icc I
hJlz : Tendsto (fun m => (J m).lower) atTop (𝓝[Set.Icc I.lower I.upper] z)
hJuz : Tendsto (fun m => (J m).upper) atTop (𝓝[Set.Icc I.lower I.upper] z)
⊢ False
[PROOFSTEP]
rcases H_nhds z (h0 ▸ hzJ 0) with ⟨U, hUz, hU⟩
[GOAL]
case intro.intro
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), z ∈ ↑Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ ↑Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ ↑Box.Icc I
hJlz : Tendsto (fun m => (J m).lower) atTop (𝓝[Set.Icc I.lower I.upper] z)
hJuz : Tendsto (fun m => (J m).upper) atTop (𝓝[Set.Icc I.lower I.upper] z)
U : Set (ι → ℝ)
hUz : U ∈ 𝓝[↑Box.Icc I] z
hU :
  ∀ (J : Box ι),
    J ≤ I →
      ∀ (m : ℕ),
        z ∈ ↑Box.Icc J → ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
⊢ False
[PROOFSTEP]
rcases(tendsto_lift'.1 (hJlz.Icc hJuz) U hUz).exists with ⟨m, hUm⟩
[GOAL]
case intro.intro.intro
ι : Type u_1
I✝ J✝ : Box ι
p : Box ι → Prop
I : Box ι
H_nhds :
  ∀ (z : ι → ℝ),
    z ∈ ↑Box.Icc I →
      ∃ U,
        U ∈ 𝓝[↑Box.Icc I] z ∧
          ∀ (J : Box ι),
            J ≤ I →
              ∀ (m : ℕ),
                z ∈ ↑Box.Icc J →
                  ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
J : ℕ → Box ι
hJmono : Antitone J
hJle : ∀ (m : ℕ), J m ≤ I
hJp : ∀ (m : ℕ), ¬p (J m)
hJsub : ∀ (m : ℕ) (i : ι), upper (J m) i - lower (J m) i = (upper I i - lower I i) / 2 ^ m
h0 : J 0 = I
z : ι → ℝ := ⨆ (m : ℕ), (J m).lower
hzJ : ∀ (m : ℕ), z ∈ ↑Box.Icc (J m)
hJl_mem : ∀ (m : ℕ), (J m).lower ∈ ↑Box.Icc I
hJu_mem : ∀ (m : ℕ), (J m).upper ∈ ↑Box.Icc I
hJlz : Tendsto (fun m => (J m).lower) atTop (𝓝[Set.Icc I.lower I.upper] z)
hJuz : Tendsto (fun m => (J m).upper) atTop (𝓝[Set.Icc I.lower I.upper] z)
U : Set (ι → ℝ)
hUz : U ∈ 𝓝[↑Box.Icc I] z
hU :
  ∀ (J : Box ι),
    J ≤ I →
      ∀ (m : ℕ),
        z ∈ ↑Box.Icc J → ↑Box.Icc J ⊆ U → (∀ (i : ι), upper J i - lower J i = (upper I i - lower I i) / 2 ^ m) → p J
m : ℕ
hUm : Set.Icc (J m).lower (J m).upper ∈ 𝒫 U
⊢ False
[PROOFSTEP]
exact hJp m (hU (J m) (hJle m) m (hzJ m) hUm (hJsub m))


[GOAL]
ι : Type u_1
I : Box ι
inst✝ : Countable ι
⊢ MeasurableSet ↑I
[PROOFSTEP]
rw [coe_eq_pi]
[GOAL]
ι : Type u_1
I : Box ι
inst✝ : Countable ι
⊢ MeasurableSet (pi univ fun i => Ioc (lower I i) (upper I i))
[PROOFSTEP]
exact MeasurableSet.univ_pi fun i => measurableSet_Ioc
[GOAL]
ι : Type u_1
I : Box ι
inst✝ : Fintype ι
⊢ ↑I =ᵐ[volume] ↑Box.Icc I
[PROOFSTEP]
rw [coe_eq_pi]
[GOAL]
ι : Type u_1
I : Box ι
inst✝ : Fintype ι
⊢ (pi univ fun i => Ioc (lower I i) (upper I i)) =ᵐ[volume] ↑Box.Icc I
[PROOFSTEP]
exact Measure.univ_pi_Ioc_ae_eq_Icc
[GOAL]
ι : Type u_1
inst✝¹ : Finite ι
I : Box ι
π : Prepartition I
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ ENNReal.toReal (↑↑μ (Prepartition.iUnion π)) = ∑ J in π.boxes, ENNReal.toReal (↑↑μ ↑J)
[PROOFSTEP]
erw [← ENNReal.toReal_sum, π.iUnion_def, measure_biUnion_finset π.pairwiseDisjoint]
[GOAL]
ι : Type u_1
inst✝¹ : Finite ι
I : Box ι
π : Prepartition I
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ ∀ (b : Box ι), b ∈ π.boxes → MeasurableSet ↑b
ι : Type u_1
inst✝¹ : Finite ι
I : Box ι
π : Prepartition I
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
⊢ ∀ (a : Box ι), a ∈ π.boxes → ↑↑μ ↑a ≠ ⊤
[PROOFSTEP]
exacts [fun J _ => J.measurableSet_coe, fun J _ => (J.measure_coe_lt_top μ).ne]
[GOAL]
ι : Type u_1
inst✝¹ : Fintype ι
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
J : Box ι
x✝ : ↑J ≤ ⊤
π : Prepartition J
hπ : Prepartition.IsPartition π
⊢ ∑ Ji in π.boxes, (fun J => ENNReal.toReal (↑↑μ ↑J)) Ji = (fun J => ENNReal.toReal (↑↑μ ↑J)) J
[PROOFSTEP]
rw [← π.measure_iUnion_toReal, hπ.iUnion_eq]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
⊢ ↑(Measure.toBoxAdditive volume) I = ∏ i : ι, (upper I i - lower I i)
[PROOFSTEP]
rw [Measure.toBoxAdditive_apply, coe_eq_pi, Real.volume_pi_Ioc_toReal I.lower_le_upper]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
⊢ ENNReal.toReal (↑↑volume ↑I) = ∏ i : ι, (upper I i - lower I i)
[PROOFSTEP]
rw [coe_eq_pi, Real.volume_pi_Ioc_toReal I.lower_le_upper]
[GOAL]
ι : Type u_1
inst✝ : Fintype ι
n : ℕ
i : Fin (n + 1)
I : Box (Fin (n + 1))
⊢ (∏ j : Fin n, (upper (face I i) j - lower (face I i) j)) * (upper I i - lower I i) =
    ∏ j : Fin (n + 1), (upper I j - lower I j)
[PROOFSTEP]
simp only [face_lower, face_upper, (· ∘ ·), Fin.prod_univ_succAbove _ i, mul_comm]
[GOAL]
ι : Type u_1
inst✝² : Fintype ι
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
I : Box ι
x : E
⊢ ↑(↑BoxAdditiveMap.volume I) x = (∏ j : ι, (upper I j - lower I j)) • x
[PROOFSTEP]
rw [BoxAdditiveMap.volume, toSMul_apply]
[GOAL]
ι : Type u_1
inst✝² : Fintype ι
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
I : Box ι
x : E
⊢ ↑(Measure.toBoxAdditive volume) I • x = (∏ j : ι, (upper I j - lower I j)) • x
[PROOFSTEP]
exact congr_arg₂ (· • ·) I.volume_apply rfl


[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I : Box ι
i : ι
x : ℝ
y : ι → ℝ
⊢ ↑(splitLower I i x) = ↑I ∩ {y | y i ≤ x}
[PROOFSTEP]
rw [splitLower, coe_mk']
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I : Box ι
i : ι
x : ℝ
y : ι → ℝ
⊢ (Set.pi univ fun i_1 => Ioc (lower I i_1) (update I.upper i (min x (upper I i)) i_1)) = ↑I ∩ {y | y i ≤ x}
[PROOFSTEP]
ext y
[GOAL]
case h
ι : Type u_1
M : Type u_2
n : ℕ
I : Box ι
i : ι
x : ℝ
y✝ y : ι → ℝ
⊢ (y ∈ Set.pi univ fun i_1 => Ioc (lower I i_1) (update I.upper i (min x (upper I i)) i_1)) ↔ y ∈ ↑I ∩ {y | y i ≤ x}
[PROOFSTEP]
simp only [mem_univ_pi, mem_Ioc, mem_inter_iff, mem_coe, mem_setOf_eq, forall_and, ← Pi.le_def, le_update_iff,
  le_min_iff, and_assoc, and_forall_ne (p := fun j => y j ≤ upper I j) i, mem_def]
[GOAL]
case h
ι : Type u_1
M : Type u_2
n : ℕ
I : Box ι
i : ι
x : ℝ
y✝ y : ι → ℝ
⊢ ((∀ (x : ι), lower I x < y x) ∧ y i ≤ x ∧ (fun i => y i) ≤ fun i => upper I i) ↔
    (∀ (x : ι), lower I x < y x) ∧ ((fun i => y i) ≤ fun i => upper I i) ∧ y i ≤ x
[PROOFSTEP]
rw [and_comm (a := y i ≤ x), Pi.le_def]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I : Box ι
i : ι
x : ℝ
y : ι → ℝ
⊢ ↑(splitLower I i x) ⊆ ↑↑I
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
i : ι
x : ℝ
⊢ splitLower I i x = ⊥ ↔ x ≤ lower I i
[PROOFSTEP]
rw [splitLower, mk'_eq_bot, exists_update_iff I.upper fun j y => y ≤ I.lower j]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
i : ι
x : ℝ
⊢ (min x (upper I i) ≤ lower I i ∨ ∃ x x_1, upper I x ≤ lower I x) ↔ x ≤ lower I i
[PROOFSTEP]
simp [(I.lower_lt_upper _).not_le]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I : Box ι
i : ι
x : ℝ
y : ι → ℝ
⊢ splitLower I i x = ↑I ↔ upper I i ≤ x
[PROOFSTEP]
simp [splitLower, update_eq_iff]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
inst✝ : DecidableEq ι
i : ι
x : ℝ
h : x ∈ Ioo (lower I i) (upper I i)
h' : optParam (∀ (j : ι), lower I j < update I.upper i x j) (_ : ∀ (x_1 : ι), lower I x_1 < update I.upper i x x_1)
⊢ splitLower I i x = ↑{ lower := I.lower, upper := update I.upper i x, lower_lt_upper := h' }
[PROOFSTEP]
simp only [splitLower, mk'_eq_coe, min_eq_left h.2.le, update]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I : Box ι
i : ι
x : ℝ
y : ι → ℝ
⊢ ↑(splitUpper I i x) = ↑I ∩ {y | x < y i}
[PROOFSTEP]
rw [splitUpper, coe_mk']
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I : Box ι
i : ι
x : ℝ
y : ι → ℝ
⊢ (Set.pi univ fun i_1 => Ioc (update I.lower i (max x (lower I i)) i_1) (upper I i_1)) = ↑I ∩ {y | x < y i}
[PROOFSTEP]
ext y
[GOAL]
case h
ι : Type u_1
M : Type u_2
n : ℕ
I : Box ι
i : ι
x : ℝ
y✝ y : ι → ℝ
⊢ (y ∈ Set.pi univ fun i_1 => Ioc (update I.lower i (max x (lower I i)) i_1) (upper I i_1)) ↔ y ∈ ↑I ∩ {y | x < y i}
[PROOFSTEP]
simp only [mem_univ_pi, mem_Ioc, mem_inter_iff, mem_coe, mem_setOf_eq, forall_and,
  forall_update_iff I.lower fun j z => z < y j, max_lt_iff, and_assoc (a := x < y i),
  and_forall_ne (p := fun j => lower I j < y j) i, mem_def]
[GOAL]
case h
ι : Type u_1
M : Type u_2
n : ℕ
I : Box ι
i : ι
x : ℝ
y✝ y : ι → ℝ
⊢ (x < y i ∧ (∀ (b : ι), lower I b < y b) ∧ ∀ (x : ι), y x ≤ upper I x) ↔
    ((∀ (x : ι), lower I x < y x) ∧ ∀ (x : ι), y x ≤ upper I x) ∧ x < y i
[PROOFSTEP]
exact and_comm
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I : Box ι
i : ι
x : ℝ
y : ι → ℝ
⊢ ↑(splitUpper I i x) ⊆ ↑↑I
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
i : ι
x : ℝ
⊢ splitUpper I i x = ⊥ ↔ upper I i ≤ x
[PROOFSTEP]
rw [splitUpper, mk'_eq_bot, exists_update_iff I.lower fun j y => I.upper j ≤ y]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
i : ι
x : ℝ
⊢ (upper I i ≤ max x (lower I i) ∨ ∃ x x_1, upper I x ≤ lower I x) ↔ upper I i ≤ x
[PROOFSTEP]
simp [(I.lower_lt_upper _).not_le]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I : Box ι
i : ι
x : ℝ
y : ι → ℝ
⊢ splitUpper I i x = ↑I ↔ x ≤ lower I i
[PROOFSTEP]
simp [splitUpper, update_eq_iff]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
inst✝ : DecidableEq ι
i : ι
x : ℝ
h : x ∈ Ioo (lower I i) (upper I i)
h' : optParam (∀ (j : ι), update I.lower i x j < upper I j) (_ : ∀ (x_1 : ι), update I.lower i x x_1 < upper I x_1)
⊢ splitUpper I i x = ↑{ lower := update I.lower i x, upper := I.upper, lower_lt_upper := h' }
[PROOFSTEP]
simp only [splitUpper, mk'_eq_coe, max_eq_left h.1.le, update]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
⊢ Disjoint (splitLower I i x) (splitUpper I i x)
[PROOFSTEP]
rw [← disjoint_withBotCoe, coe_splitLower, coe_splitUpper]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
⊢ Disjoint (↑I ∩ {y | y i ≤ x}) (↑I ∩ {y | x < y i})
[PROOFSTEP]
refine' (Disjoint.inf_left' _ _).inf_right' _
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
⊢ Disjoint {y | y i ≤ x} {y | x < y i}
[PROOFSTEP]
rw [Set.disjoint_left]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
⊢ ∀ ⦃a : ι → ℝ⦄, a ∈ {y | y i ≤ x} → ¬a ∈ {y | x < y i}
[PROOFSTEP]
exact fun y (hle : y i ≤ x) hlt => not_lt_of_le hle hlt
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
⊢ splitLower I i x ≠ splitUpper I i x
[PROOFSTEP]
cases' le_or_lt x (I.lower i) with h
[GOAL]
case inl
ι : Type u_1
M : Type u_2
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
h : x ≤ lower I i
⊢ splitLower I i x ≠ splitUpper I i x
[PROOFSTEP]
rw [splitUpper_eq_self.2 h, splitLower_eq_bot.2 h]
[GOAL]
case inl
ι : Type u_1
M : Type u_2
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
h : x ≤ lower I i
⊢ ⊥ ≠ ↑I
[PROOFSTEP]
exact WithBot.bot_ne_coe
[GOAL]
case inr
ι : Type u_1
M : Type u_2
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
h✝ : lower I i < x
⊢ splitLower I i x ≠ splitUpper I i x
[PROOFSTEP]
refine' (disjoint_splitLower_splitUpper I i x).ne _
[GOAL]
case inr
ι : Type u_1
M : Type u_2
n : ℕ
I✝ : Box ι
i✝ : ι
x✝ : ℝ
y : ι → ℝ
I : Box ι
i : ι
x : ℝ
h✝ : lower I i < x
⊢ splitLower I i x ≠ ⊥
[PROOFSTEP]
rwa [Ne.def, splitLower_eq_bot, not_le]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i✝ : ι
x✝ : ℝ
I : Box ι
i : ι
x : ℝ
⊢ ∀ (J : WithBot (Box ι)), J ∈ {Box.splitLower I i x, Box.splitUpper I i x} → J ≤ ↑I
[PROOFSTEP]
simp only [Finset.mem_insert, Finset.mem_singleton]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i✝ : ι
x✝ : ℝ
I : Box ι
i : ι
x : ℝ
⊢ ∀ (J : WithBot (Box ι)), J = Box.splitLower I i x ∨ J = Box.splitUpper I i x → J ≤ ↑I
[PROOFSTEP]
rintro J (rfl | rfl)
[GOAL]
case inl
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i✝ : ι
x✝ : ℝ
I : Box ι
i : ι
x : ℝ
⊢ Box.splitLower I i x ≤ ↑I
case inr ι : Type u_1 M : Type u_2 n : ℕ I✝ J : Box ι i✝ : ι x✝ : ℝ I : Box ι i : ι x : ℝ ⊢ Box.splitUpper I i x ≤ ↑I
[PROOFSTEP]
exacts [Box.splitLower_le, Box.splitUpper_le]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i✝ : ι
x✝ : ℝ
I : Box ι
i : ι
x : ℝ
⊢ Set.Pairwise (↑{Box.splitLower I i x, Box.splitUpper I i x}) Disjoint
[PROOFSTEP]
simp only [Finset.coe_insert, Finset.coe_singleton, true_and_iff, Set.mem_singleton_iff,
  pairwise_insert_of_symmetric symmetric_disjoint, pairwise_singleton]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i✝ : ι
x✝ : ℝ
I : Box ι
i : ι
x : ℝ
⊢ ∀ (b : WithBot (Box ι)), b = Box.splitUpper I i x → Box.splitLower I i x ≠ b → Disjoint (Box.splitLower I i x) b
[PROOFSTEP]
rintro J rfl -
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i✝ : ι
x✝ : ℝ
I : Box ι
i : ι
x : ℝ
⊢ Disjoint (Box.splitLower I i x) (Box.splitUpper I i x)
[PROOFSTEP]
exact I.disjoint_splitLower_splitUpper i x
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
⊢ J ∈ split I i x ↔ ↑J = Box.splitLower I i x ∨ ↑J = Box.splitUpper I i x
[PROOFSTEP]
simp [split]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
⊢ J ∈ split I i x ↔ ↑J = ↑I ∩ {y | y i ≤ x} ∨ ↑J = ↑I ∩ {y | x < y i}
[PROOFSTEP]
simp [mem_split_iff, ← Box.withBotCoe_inj]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i✝ : ι
x✝ : ℝ
I : Box ι
i : ι
x : ℝ
⊢ Prepartition.iUnion (split I i x) = ↑I
[PROOFSTEP]
simp [split, ← inter_union_distrib_left, ← setOf_or, le_or_lt]
[GOAL]
ι : Type u_1
M✝ : Type u_2
n : ℕ
I✝ J : Box ι
i✝ : ι
x✝ : ℝ
M : Type u_3
inst✝ : AddCommMonoid M
I : Box ι
i : ι
x : ℝ
f : Box ι → M
⊢ ∑ J in (split I i x).boxes, f J = Option.elim' 0 f (Box.splitLower I i x) + Option.elim' 0 f (Box.splitUpper I i x)
[PROOFSTEP]
rw [split, sum_ofWithBot, Finset.sum_pair (I.splitLower_ne_splitUpper i x)]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
h : ¬x ∈ Ioo (Box.lower I i) (Box.upper I i)
⊢ split I i x = ⊤
[PROOFSTEP]
refine' ((isPartitionTop I).eq_of_boxes_subset fun J hJ => _).symm
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
h : ¬x ∈ Ioo (Box.lower I i) (Box.upper I i)
J : Box ι
hJ : J ∈ ⊤.boxes
⊢ J ∈ (split I i x).boxes
[PROOFSTEP]
rcases mem_top.1 hJ with rfl
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
J✝ : Box ι
i : ι
x : ℝ
J : Box ι
h : ¬x ∈ Ioo (Box.lower J i) (Box.upper J i)
hJ : J ∈ ⊤.boxes
⊢ J ∈ (split J i x).boxes
[PROOFSTEP]
clear hJ
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
J✝ : Box ι
i : ι
x : ℝ
J : Box ι
h : ¬x ∈ Ioo (Box.lower J i) (Box.upper J i)
⊢ J ∈ (split J i x).boxes
[PROOFSTEP]
rw [mem_boxes, mem_split_iff]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
J✝ : Box ι
i : ι
x : ℝ
J : Box ι
h : ¬x ∈ Ioo (Box.lower J i) (Box.upper J i)
⊢ ↑J = Box.splitLower J i x ∨ ↑J = Box.splitUpper J i x
[PROOFSTEP]
rw [mem_Ioo, not_and_or, not_lt, not_lt] at h
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
J✝ : Box ι
i : ι
x : ℝ
J : Box ι
h : x ≤ Box.lower J i ∨ Box.upper J i ≤ x
⊢ ↑J = Box.splitLower J i x ∨ ↑J = Box.splitUpper J i x
[PROOFSTEP]
cases h <;> [right; left]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
J✝ : Box ι
i : ι
x : ℝ
J : Box ι
h : x ≤ Box.lower J i ∨ Box.upper J i ≤ x
⊢ ↑J = Box.splitLower J i x ∨ ↑J = Box.splitUpper J i x
[PROOFSTEP]
cases h
[GOAL]
case inl
ι : Type u_1
M : Type u_2
n : ℕ
J✝ : Box ι
i : ι
x : ℝ
J : Box ι
h✝ : x ≤ Box.lower J i
⊢ ↑J = Box.splitLower J i x ∨ ↑J = Box.splitUpper J i x
[PROOFSTEP]
right
[GOAL]
case inr
ι : Type u_1
M : Type u_2
n : ℕ
J✝ : Box ι
i : ι
x : ℝ
J : Box ι
h✝ : Box.upper J i ≤ x
⊢ ↑J = Box.splitLower J i x ∨ ↑J = Box.splitUpper J i x
[PROOFSTEP]
left
[GOAL]
case inl.h
ι : Type u_1
M : Type u_2
n : ℕ
J✝ : Box ι
i : ι
x : ℝ
J : Box ι
h✝ : x ≤ Box.lower J i
⊢ ↑J = Box.splitUpper J i x
[PROOFSTEP]
rwa [eq_comm, Box.splitUpper_eq_self]
[GOAL]
case inr.h
ι : Type u_1
M : Type u_2
n : ℕ
J✝ : Box ι
i : ι
x : ℝ
J : Box ι
h✝ : Box.upper J i ≤ x
⊢ ↑J = Box.splitLower J i x
[PROOFSTEP]
rwa [eq_comm, Box.splitLower_eq_self]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ J
h₃ : y i ≤ x
⊢ ↑J = ↑I ∩ {y | y i ≤ x}
[PROOFSTEP]
refine' (mem_split_iff'.1 h₁).resolve_right fun H => _
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ J
h₃ : y i ≤ x
H : ↑J = ↑I ∩ {y | x < y i}
⊢ False
[PROOFSTEP]
rw [← Box.mem_coe, H] at h₂
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ ↑I ∩ {y | x < y i}
h₃ : y i ≤ x
H : ↑J = ↑I ∩ {y | x < y i}
⊢ False
[PROOFSTEP]
exact h₃.not_lt h₂.2
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ J
h₃ : x < y i
⊢ ↑J = ↑I ∩ {y | x < y i}
[PROOFSTEP]
refine' (mem_split_iff'.1 h₁).resolve_left fun H => _
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ J
h₃ : x < y i
H : ↑J = ↑I ∩ {y | y i ≤ x}
⊢ False
[PROOFSTEP]
rw [← Box.mem_coe, H] at h₂
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
y : ι → ℝ
h₁ : J ∈ split I i x
h₂ : y ∈ ↑I ∩ {y | y i ≤ x}
h₃ : x < y i
H : ↑J = ↑I ∩ {y | y i ≤ x}
⊢ False
[PROOFSTEP]
exact h₃.not_le h₂.2
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i✝ : ι
x✝ : ℝ
h : I ≤ J
i : ι
x : ℝ
⊢ restrict (split J i x) I = split I i x
[PROOFSTEP]
refine' ((isPartitionSplit J i x).restrict h).eq_of_boxes_subset _
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i✝ : ι
x✝ : ℝ
h : I ≤ J
i : ι
x : ℝ
⊢ (restrict (split J i x) I).boxes ⊆ (split I i x).boxes
[PROOFSTEP]
simp only [Finset.subset_iff, mem_boxes, mem_restrict', exists_prop, mem_split_iff']
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i✝ : ι
x✝ : ℝ
h : I ≤ J
i : ι
x : ℝ
⊢ ∀ ⦃x_1 : Box ι⦄,
    (∃ J', (↑J' = ↑J ∩ {y | y i ≤ x} ∨ ↑J' = ↑J ∩ {y | x < y i}) ∧ ↑x_1 = ↑I ∩ ↑J') →
      ↑x_1 = ↑I ∩ {y | y i ≤ x} ∨ ↑x_1 = ↑I ∩ {y | x < y i}
[PROOFSTEP]
have : ∀ s, (I ∩ s : Set (ι → ℝ)) ⊆ J := fun s => (inter_subset_left _ _).trans h
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i✝ : ι
x✝ : ℝ
h : I ≤ J
i : ι
x : ℝ
this : ∀ (s : Set (ι → ℝ)), ↑I ∩ s ⊆ ↑J
⊢ ∀ ⦃x_1 : Box ι⦄,
    (∃ J', (↑J' = ↑J ∩ {y | y i ≤ x} ∨ ↑J' = ↑J ∩ {y | x < y i}) ∧ ↑x_1 = ↑I ∩ ↑J') →
      ↑x_1 = ↑I ∩ {y | y i ≤ x} ∨ ↑x_1 = ↑I ∩ {y | x < y i}
[PROOFSTEP]
rintro J₁ ⟨J₂, H₂ | H₂, H₁⟩ <;> [left; right]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i✝ : ι
x✝ : ℝ
h : I ≤ J
i : ι
x : ℝ
this : ∀ (s : Set (ι → ℝ)), ↑I ∩ s ⊆ ↑J
⊢ ∀ ⦃x_1 : Box ι⦄,
    (∃ J', (↑J' = ↑J ∩ {y | y i ≤ x} ∨ ↑J' = ↑J ∩ {y | x < y i}) ∧ ↑x_1 = ↑I ∩ ↑J') →
      ↑x_1 = ↑I ∩ {y | y i ≤ x} ∨ ↑x_1 = ↑I ∩ {y | x < y i}
[PROOFSTEP]
rintro J₁ ⟨J₂, H₂ | H₂, H₁⟩
[GOAL]
case intro.intro.inl
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i✝ : ι
x✝ : ℝ
h : I ≤ J
i : ι
x : ℝ
this : ∀ (s : Set (ι → ℝ)), ↑I ∩ s ⊆ ↑J
J₁ J₂ : Box ι
H₁ : ↑J₁ = ↑I ∩ ↑J₂
H₂ : ↑J₂ = ↑J ∩ {y | y i ≤ x}
⊢ ↑J₁ = ↑I ∩ {y | y i ≤ x} ∨ ↑J₁ = ↑I ∩ {y | x < y i}
[PROOFSTEP]
left
[GOAL]
case intro.intro.inr
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i✝ : ι
x✝ : ℝ
h : I ≤ J
i : ι
x : ℝ
this : ∀ (s : Set (ι → ℝ)), ↑I ∩ s ⊆ ↑J
J₁ J₂ : Box ι
H₁ : ↑J₁ = ↑I ∩ ↑J₂
H₂ : ↑J₂ = ↑J ∩ {y | x < y i}
⊢ ↑J₁ = ↑I ∩ {y | y i ≤ x} ∨ ↑J₁ = ↑I ∩ {y | x < y i}
[PROOFSTEP]
right
[GOAL]
case intro.intro.inl.h
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i✝ : ι
x✝ : ℝ
h : I ≤ J
i : ι
x : ℝ
this : ∀ (s : Set (ι → ℝ)), ↑I ∩ s ⊆ ↑J
J₁ J₂ : Box ι
H₁ : ↑J₁ = ↑I ∩ ↑J₂
H₂ : ↑J₂ = ↑J ∩ {y | y i ≤ x}
⊢ ↑J₁ = ↑I ∩ {y | y i ≤ x}
[PROOFSTEP]
simp [H₁, H₂, inter_left_comm (I : Set (ι → ℝ)), this]
[GOAL]
case intro.intro.inr.h
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i✝ : ι
x✝ : ℝ
h : I ≤ J
i : ι
x : ℝ
this : ∀ (s : Set (ι → ℝ)), ↑I ∩ s ⊆ ↑J
J₁ J₂ : Box ι
H₁ : ↑J₁ = ↑I ∩ ↑J₂
H₂ : ↑J₂ = ↑J ∩ {y | x < y i}
⊢ ↑J₁ = ↑I ∩ {y | x < y i}
[PROOFSTEP]
simp [H₁, H₂, inter_left_comm (I : Set (ι → ℝ)), this]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i : ι
x : ℝ
I : Box ι
s : Finset (ι × ℝ)
p : ι × ℝ
⊢ splitMany I (insert p s) = splitMany I s ⊓ split I p.fst p.snd
[PROOFSTEP]
rw [splitMany, Finset.inf_insert, inf_comm, splitMany]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i : ι
x : ℝ
I : Box ι
s : Finset (ι × ℝ)
⊢ IsPartition (splitMany I ∅)
[PROOFSTEP]
simp only [splitMany_empty, isPartitionTop]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i : ι
x : ℝ
I : Box ι
s✝ : Finset (ι × ℝ)
a : ι × ℝ
s : Finset (ι × ℝ)
x✝ : ¬a ∈ s
hs : IsPartition (splitMany I s)
⊢ IsPartition (splitMany I (insert a s))
[PROOFSTEP]
simpa only [splitMany_insert, inf_split] using hs.biUnion fun J _ => isPartitionSplit _ _ _
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i : ι
x : ℝ
I : Box ι
π : Prepartition I
s : Finset (ι × ℝ)
⊢ π ⊓ splitMany I s = biUnion π fun J => splitMany J s
[PROOFSTEP]
induction' s using Finset.induction_on with p s _ ihp
[GOAL]
case empty
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i : ι
x : ℝ
I : Box ι
π : Prepartition I
⊢ π ⊓ splitMany I ∅ = biUnion π fun J => splitMany J ∅
[PROOFSTEP]
simp
[GOAL]
case insert
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i : ι
x : ℝ
I : Box ι
π : Prepartition I
p : ι × ℝ
s : Finset (ι × ℝ)
a✝ : ¬p ∈ s
ihp : π ⊓ splitMany I s = biUnion π fun J => splitMany J s
⊢ π ⊓ splitMany I (insert p s) = biUnion π fun J => splitMany J (insert p s)
[PROOFSTEP]
simp_rw [splitMany_insert, ← inf_assoc, ihp, inf_split, biUnion_assoc]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J✝ : Box ι
i : ι
x : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
H : ∀ (i : ι), {(i, Box.lower J i), (i, Box.upper J i)} ⊆ s
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
⊢ Js ≤ J
[PROOFSTEP]
simp only [Finset.insert_subset_iff, Finset.singleton_subset_iff] at H
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J✝ : Box ι
i : ι
x : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
⊢ Js ≤ J
[PROOFSTEP]
rcases Box.not_disjoint_coe_iff_nonempty_inter.mp Hn with ⟨x, hx, hxs⟩
[GOAL]
case intro.intro
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J✝ : Box ι
i : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
⊢ Js ≤ J
[PROOFSTEP]
refine' fun y hy i => ⟨_, _⟩
[GOAL]
case intro.intro.refine'_1
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
⊢ Box.lower J i < y i
[PROOFSTEP]
rcases splitMany_le_split I (H i).1 HJs with ⟨Jl, Hmem : Jl ∈ split I i (J.lower i), Hle⟩
[GOAL]
case intro.intro.refine'_1.intro.intro
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
Jl : Box ι
Hmem : Jl ∈ split I i (Box.lower J i)
Hle : Js ≤ Jl
⊢ Box.lower J i < y i
[PROOFSTEP]
have := Hle hxs
[GOAL]
case intro.intro.refine'_1.intro.intro
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
Jl : Box ι
Hmem : Jl ∈ split I i (Box.lower J i)
Hle : Js ≤ Jl
this : (fun i => x i) ∈ Jl
⊢ Box.lower J i < y i
[PROOFSTEP]
rw [← Box.coe_subset_coe, coe_eq_of_mem_split_of_lt_mem Hmem this (hx i).1] at Hle
[GOAL]
case intro.intro.refine'_1.intro.intro
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
Jl : Box ι
Hmem : Jl ∈ split I i (Box.lower J i)
Hle : ↑Js ⊆ ↑I ∩ {y | Box.lower J i < y i}
this : (fun i => x i) ∈ Jl
⊢ Box.lower J i < y i
[PROOFSTEP]
exact (Hle hy).2
[GOAL]
case intro.intro.refine'_2
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
⊢ y i ≤ Box.upper J i
[PROOFSTEP]
rcases splitMany_le_split I (H i).2 HJs with ⟨Jl, Hmem : Jl ∈ split I i (J.upper i), Hle⟩
[GOAL]
case intro.intro.refine'_2.intro.intro
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
Jl : Box ι
Hmem : Jl ∈ split I i (Box.upper J i)
Hle : Js ≤ Jl
⊢ y i ≤ Box.upper J i
[PROOFSTEP]
have := Hle hxs
[GOAL]
case intro.intro.refine'_2.intro.intro
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
Jl : Box ι
Hmem : Jl ∈ split I i (Box.upper J i)
Hle : Js ≤ Jl
this : (fun i => x i) ∈ Jl
⊢ y i ≤ Box.upper J i
[PROOFSTEP]
rw [← Box.coe_subset_coe, coe_eq_of_mem_split_of_mem_le Hmem this (hx i).2] at Hle
[GOAL]
case intro.intro.refine'_2.intro.intro
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x✝ : ℝ
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, Box.lower J i) ∈ s ∧ (i, Box.upper J i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
Jl : Box ι
Hmem : Jl ∈ split I i (Box.upper J i)
Hle : ↑Js ⊆ ↑I ∩ {y | y i ≤ Box.upper J i}
this : (fun i => x i) ∈ Jl
⊢ y i ≤ Box.upper J i
[PROOFSTEP]
exact (Hle hy).2
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
s : Finset (Box ι)
⊢ ∀ᶠ (t : Finset (ι × ℝ)) in atTop,
    ∀ (I J : Box ι), J ∈ s → ∀ (J' : Box ι), J' ∈ splitMany I t → ¬Disjoint ↑J ↑J' → J' ≤ J
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
s : Finset (Box ι)
val✝ : Fintype ι
⊢ ∀ᶠ (t : Finset (ι × ℝ)) in atTop,
    ∀ (I J : Box ι), J ∈ s → ∀ (J' : Box ι), J' ∈ splitMany I t → ¬Disjoint ↑J ↑J' → J' ≤ J
[PROOFSTEP]
refine'
  eventually_atTop.2
    ⟨s.biUnion fun J => Finset.univ.biUnion fun i => {(i, J.lower i), (i, J.upper i)}, fun t ht I J hJ J' hJ' =>
      not_disjoint_imp_le_of_subset_of_mem_splitMany (fun i => _) hJ'⟩
[GOAL]
case intro
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J✝ : Box ι
i✝ : ι
x : ℝ
inst✝ : Finite ι
s : Finset (Box ι)
val✝ : Fintype ι
t : Finset (ι × ℝ)
ht : t ≥ Finset.biUnion s fun J => Finset.biUnion Finset.univ fun i => {(i, Box.lower J i), (i, Box.upper J i)}
I J : Box ι
hJ : J ∈ s
J' : Box ι
hJ' : J' ∈ splitMany I t
i : ι
⊢ {(i, Box.lower J i), (i, Box.upper J i)} ⊆ t
[PROOFSTEP]
exact fun p hp => ht (Finset.mem_biUnion.2 ⟨J, hJ, Finset.mem_biUnion.2 ⟨i, Finset.mem_univ _, hp⟩⟩)
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
⊢ ∀ᶠ (t : Finset (ι × ℝ)) in atTop, π ⊓ splitMany I t = filter (splitMany I t) fun J => ↑J ⊆ Prepartition.iUnion π
[PROOFSTEP]
refine' (eventually_not_disjoint_imp_le_of_mem_splitMany π.boxes).mono fun t ht => _
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
⊢ π ⊓ splitMany I t = filter (splitMany I t) fun J => ↑J ⊆ Prepartition.iUnion π
[PROOFSTEP]
refine' le_antisymm ((biUnion_le_iff _).2 fun J hJ => _) (le_inf (fun J hJ => _) (filter_le _ _))
[GOAL]
case refine'_1
ι : Type u_1
M : Type u_2
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ π
⊢ restrict (splitMany I t) J ≤ restrict (filter (splitMany I t) fun J => ↑J ⊆ Prepartition.iUnion π) J
[PROOFSTEP]
refine' ofWithBot_mono _
[GOAL]
case refine'_1
ι : Type u_1
M : Type u_2
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ π
⊢ ∀ (J_1 : WithBot (Box ι)),
    J_1 ∈ Finset.image (fun J' => ↑J ⊓ ↑J') (splitMany I t).boxes →
      J_1 ≠ ⊥ →
        ∃ J',
          J' ∈ Finset.image (fun J' => ↑J ⊓ ↑J') (filter (splitMany I t) fun J => ↑J ⊆ Prepartition.iUnion π).boxes ∧
            J_1 ≤ J'
[PROOFSTEP]
simp only [Finset.mem_image, exists_prop, mem_boxes, mem_filter]
[GOAL]
case refine'_1
ι : Type u_1
M : Type u_2
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ π
⊢ ∀ (J_1 : WithBot (Box ι)),
    (∃ a, a ∈ splitMany I t ∧ ↑J ⊓ ↑a = J_1) →
      J_1 ≠ ⊥ → ∃ J', (∃ a, (a ∈ splitMany I t ∧ ↑a ⊆ Prepartition.iUnion π) ∧ ↑J ⊓ ↑a = J') ∧ J_1 ≤ J'
[PROOFSTEP]
rintro _ ⟨J₁, h₁, rfl⟩ hne
[GOAL]
case refine'_1.intro.intro
ι : Type u_1
M : Type u_2
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ π
J₁ : Box ι
h₁ : J₁ ∈ splitMany I t
hne : ↑J ⊓ ↑J₁ ≠ ⊥
⊢ ∃ J', (∃ a, (a ∈ splitMany I t ∧ ↑a ⊆ Prepartition.iUnion π) ∧ ↑J ⊓ ↑a = J') ∧ ↑J ⊓ ↑J₁ ≤ J'
[PROOFSTEP]
refine' ⟨_, ⟨J₁, ⟨h₁, Subset.trans _ (π.subset_iUnion hJ)⟩, rfl⟩, le_rfl⟩
[GOAL]
case refine'_1.intro.intro
ι : Type u_1
M : Type u_2
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ π
J₁ : Box ι
h₁ : J₁ ∈ splitMany I t
hne : ↑J ⊓ ↑J₁ ≠ ⊥
⊢ ↑J₁ ⊆ ↑J
[PROOFSTEP]
exact ht I J hJ J₁ h₁ (mt disjoint_iff.1 hne)
[GOAL]
case refine'_2
ι : Type u_1
M : Type u_2
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ filter (splitMany I t) fun J => ↑J ⊆ Prepartition.iUnion π
⊢ ∃ I', I' ∈ π ∧ J ≤ I'
[PROOFSTEP]
rw [mem_filter] at hJ
[GOAL]
case refine'_2
ι : Type u_1
M : Type u_2
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ splitMany I t ∧ ↑J ⊆ Prepartition.iUnion π
⊢ ∃ I', I' ∈ π ∧ J ≤ I'
[PROOFSTEP]
rcases Set.mem_iUnion₂.1 (hJ.2 J.upper_mem) with ⟨J', hJ', hmem⟩
[GOAL]
case refine'_2.intro.intro
ι : Type u_1
M : Type u_2
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ splitMany I t ∧ ↑J ⊆ Prepartition.iUnion π
J' : Box ι
hJ' : J' ∈ π
hmem : (fun i => Box.upper J i) ∈ ↑J'
⊢ ∃ I', I' ∈ π ∧ J ≤ I'
[PROOFSTEP]
refine' ⟨J', hJ', ht I _ hJ' _ hJ.1 <| Box.not_disjoint_coe_iff_nonempty_inter.2 _⟩
[GOAL]
case refine'_2.intro.intro
ι : Type u_1
M : Type u_2
n : ℕ
I J✝ : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
t : Finset (ι × ℝ)
ht : ∀ (I_1 J : Box ι), J ∈ π.boxes → ∀ (J' : Box ι), J' ∈ splitMany I_1 t → ¬Disjoint ↑J ↑J' → J' ≤ J
J : Box ι
hJ : J ∈ splitMany I t ∧ ↑J ⊆ Prepartition.iUnion π
J' : Box ι
hJ' : J' ∈ π
hmem : (fun i => Box.upper J i) ∈ ↑J'
⊢ Set.Nonempty (↑J' ∩ ↑J)
[PROOFSTEP]
exact ⟨J.upper, hmem, J.upper_mem⟩
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
I : Box ι
π : Prepartition I
h : IsPartition π
⊢ ∃ s, splitMany I s ≤ π
[PROOFSTEP]
refine' (eventually_splitMany_inf_eq_filter π).exists.imp fun s hs => _
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
I : Box ι
π : Prepartition I
h : IsPartition π
s : Finset (ι × ℝ)
hs : π ⊓ splitMany I s = filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π
⊢ splitMany I s ≤ π
[PROOFSTEP]
rwa [h.iUnion_eq, filter_of_true, inf_eq_right] at hs
[GOAL]
case hp
ι : Type u_1
M : Type u_2
n : ℕ
I✝ J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
I : Box ι
π : Prepartition I
h : IsPartition π
s : Finset (ι × ℝ)
hs : π ⊓ splitMany I s = filter (splitMany I s) fun J => ↑J ⊆ ↑I
⊢ ∀ (J : Box ι), J ∈ splitMany I s → ↑J ⊆ ↑I
[PROOFSTEP]
exact fun J hJ => le_of_mem _ hJ
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
⊢ ∃ π', Prepartition.iUnion π' = ↑I \ Prepartition.iUnion π
[PROOFSTEP]
rcases π.eventually_splitMany_inf_eq_filter.exists with ⟨s, hs⟩
[GOAL]
case intro
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
s : Finset (ι × ℝ)
hs : π ⊓ splitMany I s = filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π
⊢ ∃ π', Prepartition.iUnion π' = ↑I \ Prepartition.iUnion π
[PROOFSTEP]
use(splitMany I s).filter fun J => ¬(J : Set (ι → ℝ)) ⊆ π.iUnion
[GOAL]
case h
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
s : Finset (ι × ℝ)
hs : π ⊓ splitMany I s = filter (splitMany I s) fun J => ↑J ⊆ Prepartition.iUnion π
⊢ Prepartition.iUnion (filter (splitMany I s) fun J => ¬↑J ⊆ Prepartition.iUnion π) = ↑I \ Prepartition.iUnion π
[PROOFSTEP]
simp [← hs]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
⊢ compl π₁ = compl π₂
[PROOFSTEP]
dsimp only [compl]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
⊢ Exists.choose (_ : ∃ π', Prepartition.iUnion π' = ↑I \ Prepartition.iUnion π₁) =
    Exists.choose (_ : ∃ π', Prepartition.iUnion π' = ↑I \ Prepartition.iUnion π₂)
[PROOFSTEP]
congr 1
[GOAL]
case e_p
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π₁ π₂ : Prepartition I
h : Prepartition.iUnion π₁ = Prepartition.iUnion π₂
⊢ (fun π' => Prepartition.iUnion π' = ↑I \ Prepartition.iUnion π₁) = fun π' =>
    Prepartition.iUnion π' = ↑I \ Prepartition.iUnion π₂
[PROOFSTEP]
rw [h]
[GOAL]
ι : Type u_1
M : Type u_2
n : ℕ
I J : Box ι
i : ι
x : ℝ
inst✝ : Finite ι
π : Prepartition I
h : IsPartition π
⊢ compl π = ⊥
[PROOFSTEP]
rw [← iUnion_eq_empty, iUnion_compl, h.iUnion_eq, diff_self]


[GOAL]
t : ℝ
⊢ ‖exp (↑t * I)‖ = 1
[PROOFSTEP]
simp only [norm_eq_abs, abs_exp_ofReal_mul_I]
[GOAL]
r₁ r₂ : ℝ
h₀ : 0 ≤ r₁
hr : r₁ < r₂
x : ℝ
h : r₁ < x ∧ x < r₂
⊢ r₁ < ‖↑x‖ ∧ ‖↑x‖ < r₂
[PROOFSTEP]
rwa [norm_eq_abs, abs_ofReal, abs_of_pos (h₀.trans_lt h.1)]
[GOAL]
R : Type u_1
inst✝¹ : NormedField R
inst✝ : NormedAlgebra R ℝ
r : R
x : ℂ
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖
[PROOFSTEP]
rw [← algebraMap_smul ℝ r x, real_smul, norm_mul, norm_eq_abs, abs_ofReal, ← Real.norm_eq_abs, norm_algebraMap']
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z w : ℂ
⊢ dist z w = Real.sqrt ((z.re - w.re) ^ 2 + (z.im - w.im) ^ 2)
[PROOFSTEP]
rw [sq, sq]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z w : ℂ
⊢ dist z w = Real.sqrt ((z.re - w.re) * (z.re - w.re) + (z.im - w.im) * (z.im - w.im))
[PROOFSTEP]
rfl
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z w : ℂ
h : z.re = w.re
⊢ dist z w = dist z.im w.im
[PROOFSTEP]
rw [dist_eq_re_im, h, sub_self, zero_pow two_pos, zero_add, Real.sqrt_sq_eq_abs, Real.dist_eq]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z w : ℂ
h : z.re = w.re
⊢ edist z w = edist z.im w.im
[PROOFSTEP]
rw [edist_nndist, edist_nndist, nndist_of_re_eq h]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z w : ℂ
h : z.im = w.im
⊢ dist z w = dist z.re w.re
[PROOFSTEP]
rw [dist_eq_re_im, h, sub_self, zero_pow two_pos, add_zero, Real.sqrt_sq_eq_abs, Real.dist_eq]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z w : ℂ
h : z.im = w.im
⊢ edist z w = edist z.re w.re
[PROOFSTEP]
rw [edist_nndist, edist_nndist, nndist_of_im_eq h]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
⊢ dist (↑(starRingEnd ℂ) z) z = 2 * |z.im|
[PROOFSTEP]
rw [dist_of_re_eq (conj_re z), conj_im, dist_comm, Real.dist_eq, sub_neg_eq_add, ← two_mul, _root_.abs_mul,
  abs_of_pos (zero_lt_two' ℝ)]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
⊢ ↑(nndist (↑(starRingEnd ℂ) z) z) = ↑(2 * ↑Real.nnabs z.im)
[PROOFSTEP]
rw [← dist_nndist, NNReal.coe_mul, NNReal.coe_two, Real.coe_nnabs, dist_conj_self]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
⊢ dist z (↑(starRingEnd ℂ) z) = 2 * |z.im|
[PROOFSTEP]
rw [dist_comm, dist_conj_self]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
⊢ nndist z (↑(starRingEnd ℂ) z) = 2 * ↑Real.nnabs z.im
[PROOFSTEP]
rw [nndist_comm, nndist_conj_self]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
r : ℚ
⊢ ‖↑r‖ = |↑r|
[PROOFSTEP]
rw [← ofReal_rat_cast]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
r : ℚ
⊢ ‖↑↑r‖ = |↑r|
[PROOFSTEP]
exact norm_real _
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
n : ℤ
hn : 0 ≤ n
⊢ ‖↑n‖ = ↑n
[PROOFSTEP]
rw [norm_int, ← Int.cast_abs, _root_.abs_of_nonneg hn]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
⊢ Continuous ↑normSq
[PROOFSTEP]
simpa [← normSq_eq_abs] using continuous_abs.pow 2
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
n : ℕ
⊢ ↑‖↑n‖₊ = ↑↑n
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
ζ : ℂ
n : ℕ
h : ζ ^ n = 1
hn : n ≠ 0
⊢ ‖ζ‖₊ = 1
[PROOFSTEP]
refine' (@pow_left_inj NNReal _ _ _ _ zero_le' zero_le' hn.bot_lt).mp _
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
ζ : ℂ
n : ℕ
h : ζ ^ n = 1
hn : n ≠ 0
⊢ ‖ζ‖₊ ^ n = 1 ^ n
[PROOFSTEP]
rw [← nnnorm_pow, h, nnnorm_one, one_pow]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
⊢ ‖↑equivRealProd z‖ ≤ ↑abs z
[PROOFSTEP]
simp [Prod.norm_def, abs_re_le_abs, abs_im_le_abs]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
⊢ ‖↑equivRealProd z‖ ≤ 1 * ↑abs z
[PROOFSTEP]
simpa using equivRealProd_apply_le z
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
⊢ LipschitzWith 1 ↑equivRealProd
[PROOFSTEP]
simpa using AddMonoidHomClass.lipschitz_of_bound equivRealProdLm 1 equivRealProd_apply_le'
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
⊢ ‖z‖ ≤ ↑(↑NNReal.sqrt 2) * ‖↑equivRealProdLm z‖
[PROOFSTEP]
simpa only [Real.coe_sqrt, NNReal.coe_ofNat] using abs_le_sqrt_two_mul_max z
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
⊢ Tendsto (↑normSq) (cocompact ℂ) atTop
[PROOFSTEP]
simpa [mul_self_abs] using tendsto_abs_cocompact_atTop.atTop_mul_atTop tendsto_abs_cocompact_atTop
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℂ
⊢ ‖↑reLm x‖ ≤ 1 * ‖x‖
[PROOFSTEP]
simp [abs_re_le_abs]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℂ
⊢ ‖↑imLm x‖ ≤ 1 * ‖x‖
[PROOFSTEP]
simp [abs_im_le_abs]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : E
⊢ restrictScalars ℝ (smulRight 1 x) = smulRight reClm x + I • smulRight imClm x
[PROOFSTEP]
ext ⟨a, b⟩
[GOAL]
case h.mk
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : E
a b : ℝ
⊢ ↑(restrictScalars ℝ (smulRight 1 x)) { re := a, im := b } =
    ↑(smulRight reClm x + I • smulRight imClm x) { re := a, im := b }
[PROOFSTEP]
simp [mk_eq_add_mul_I, mul_smul, smul_comm I b x]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℂ
⊢ restrictScalars ℝ (smulRight 1 x) = x • 1
[PROOFSTEP]
ext1 z
[GOAL]
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x z : ℂ
⊢ ↑(restrictScalars ℝ (smulRight 1 x)) z = ↑(x • 1) z
[PROOFSTEP]
dsimp
[GOAL]
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x z : ℂ
⊢ z * x = x * z
[PROOFSTEP]
apply mul_comm
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z w : ℂ
⊢ dist (↑(starRingEnd ℂ) z) w = dist z (↑(starRingEnd ℂ) w)
[PROOFSTEP]
rw [← dist_conj_conj, conj_conj]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ →+* ℂ
hf : Continuous ↑f
⊢ f = RingHom.id ℂ ∨ f = starRingEnd ℂ
[PROOFSTEP]
simpa only [FunLike.ext_iff] using real_algHom_eq_id_or_conj (AlgHom.mk' f (map_real_smul f hf))
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ →+* ℂ
h : Continuous ↑f
⊢ f = ofReal
[PROOFSTEP]
convert congr_arg AlgHom.toRingHom <| Subsingleton.elim (AlgHom.mk' f <| map_real_smul f h) (Algebra.ofId ℝ ℂ)
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
hz : 0 ≤ z
⊢ z = ↑‖z‖
[PROOFSTEP]
lift z to ℝ using hz.2.symm
[GOAL]
case intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℝ
hz : 0 ≤ ↑z
⊢ ↑z = ↑‖↑z‖
[PROOFSTEP]
rw [norm_eq_abs, abs_ofReal, _root_.abs_of_nonneg (id hz.1 : 0 ≤ z)]
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝ : IsROrC 𝕜
f : α → ℝ
x : ℝ
h : HasSum (fun x => ↑(f x)) ↑x
⊢ HasSum f x
[PROOFSTEP]
simpa only [IsROrC.reClm_apply, IsROrC.ofReal_re] using reClm.hasSum h
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝ : IsROrC 𝕜
f : α → ℝ
h : Summable fun x => ↑(f x)
⊢ Summable f
[PROOFSTEP]
simpa only [IsROrC.reClm_apply, IsROrC.ofReal_re] using reClm.summable h
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝ : IsROrC 𝕜
f : α → ℝ
⊢ ↑(∑' (a : α), f a) = ∑' (a : α), ↑(f a)
[PROOFSTEP]
by_cases h : Summable f
[GOAL]
case pos
α : Type u_1
𝕜 : Type u_2
inst✝ : IsROrC 𝕜
f : α → ℝ
h : Summable f
⊢ ↑(∑' (a : α), f a) = ∑' (a : α), ↑(f a)
[PROOFSTEP]
exact ContinuousLinearMap.map_tsum ofRealClm h
[GOAL]
case neg
α : Type u_1
𝕜 : Type u_2
inst✝ : IsROrC 𝕜
f : α → ℝ
h : ¬Summable f
⊢ ↑(∑' (a : α), f a) = ∑' (a : α), ↑(f a)
[PROOFSTEP]
rw [tsum_eq_zero_of_not_summable h, tsum_eq_zero_of_not_summable ((summable_ofReal _).not.mpr h), ofReal_zero]
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝ : IsROrC 𝕜
f : α → 𝕜
c : 𝕜
⊢ HasSum f c ↔ HasSum (fun x => ↑re (f x)) (↑re c) ∧ HasSum (fun x => ↑im (f x)) (↑im c)
[PROOFSTEP]
refine' ⟨fun h => ⟨hasSum_re _ h, hasSum_im _ h⟩, _⟩
[GOAL]
α : Type u_1
𝕜 : Type u_2
inst✝ : IsROrC 𝕜
f : α → 𝕜
c : 𝕜
⊢ HasSum (fun x => ↑re (f x)) (↑re c) ∧ HasSum (fun x => ↑im (f x)) (↑im c) → HasSum f c
[PROOFSTEP]
rintro ⟨h₁, h₂⟩
[GOAL]
case intro
α : Type u_1
𝕜 : Type u_2
inst✝ : IsROrC 𝕜
f : α → 𝕜
c : 𝕜
h₁ : HasSum (fun x => ↑re (f x)) (↑re c)
h₂ : HasSum (fun x => ↑im (f x)) (↑im c)
⊢ HasSum f c
[PROOFSTEP]
simpa only [re_add_im] using ((hasSum_ofReal 𝕜).mpr h₁).add (((hasSum_ofReal 𝕜).mpr h₂).mul_right I)