[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]
