-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem _root_.tendsto_tsum_div_pow_atTop_integral (hF : Continuous F) (hs₁ : IsBounded s)
    (hs₂ : MeasurableSet s) (hs₃ : volume (frontier s) = 0) :
    Tendsto (fun n : ℕ ↦ (∑' x : ↑(s ∩ (n : ℝ)⁻¹ • L), F x) / n ^ card ι)
      atTop (nhds (∫ x in s, F x))

Proof state:
case intro.intro.intro.intro
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ ↑B
ε : ℝ
hε : ε > 0
h₁ : ∃ C, ∀ x ∈ Box.Icc B, ‖s.indicator F x‖ ≤ C
h₂ : ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x
r : NNReal → (ι → ℝ) → ↑(Set.Ioi 0)
hr₁ : ∀ (c : NNReal), IntegrationParams.Riemann.RCond (r c)
hr₂ :
  ∀ (c : NNReal) (π : TaggedPrepartition B),
    IntegrationParams.Riemann.MemBaseSet B c (r c) π →
      π.IsPartition →
        dist (integralSum (s.indicator F) volume.toBoxAdditive.toSMul π)
            (∫ (x : ι → ℝ) in ↑B, s.indicator F x ∂volume) ≤
          ε / 2
⊢ ∃ N,
    ∀ n ≥ N,
      dist ((∑' (x : ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))), F ↑x) / ↑n ^ card ι)
          (∫ (x : ι → ℝ) in s, F x) <
        ε

Tactic:
refine ⟨⌈(r 0 0 : ℝ)⁻¹⌉₊, fun n hn ↦ lt_of_le_of_lt ?_ (half_lt_self_iff.mpr hε)⟩

Result:
case intro.intro.intro.intro
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ ↑B
ε : ℝ
hε : ε > 0
h₁ : ∃ C, ∀ x ∈ Box.Icc B, ‖s.indicator F x‖ ≤ C
h₂ : ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x
r : NNReal → (ι → ℝ) → ↑(Set.Ioi 0)
hr₁ : ∀ (c : NNReal), IntegrationParams.Riemann.RCond (r c)
hr₂ :
  ∀ (c : NNReal) (π : TaggedPrepartition B),
    IntegrationParams.Riemann.MemBaseSet B c (r c) π →
      π.IsPartition →
        dist (integralSum (s.indicator F) volume.toBoxAdditive.toSMul π)
            (∫ (x : ι → ℝ) in ↑B, s.indicator F x ∂volume) ≤
          ε / 2
n : ℕ
hn : n ≥ ⌈(↑(r 0 0))⁻¹⌉₊
⊢ dist ((∑' (x : ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))), F ↑x) / ↑n ^ card ι)
      (∫ (x : ι → ℝ) in s, F x) ≤
    ε / 2

Proof state:
case intro.intro.intro.intro.refine_1
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ ↑B
ε : ℝ
hε : ε > 0
h₁ : ∃ C, ∀ x ∈ Box.Icc B, ‖s.indicator F x‖ ≤ C
h₂ : ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x
r : NNReal → (ι → ℝ) → ↑(Set.Ioi 0)
hr₁ : ∀ (c : NNReal), IntegrationParams.Riemann.RCond (r c)
hr₂ :
  ∀ (c : NNReal) (π : TaggedPrepartition B),
    IntegrationParams.Riemann.MemBaseSet B c (r c) π →
      π.IsPartition →
        dist (integralSum (s.indicator F) volume.toBoxAdditive.toSMul π)
            (∫ (x : ι → ℝ) in ↑B, s.indicator F x ∂volume) ≤
          ε / 2
n : ℕ
hn : n ≥ ⌈(↑(r 0 0))⁻¹⌉₊
this : NeZero n
⊢ (prepartition n B).IsSubordinate (r 0)

Tactic:
rw [show r 0 = fun _ ↦ r 0 0 from funext_iff.mpr (hr₁ 0 rfl)]

Result:
case intro.intro.intro.intro.refine_1
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ ↑B
ε : ℝ
hε : ε > 0
h₁ : ∃ C, ∀ x ∈ Box.Icc B, ‖s.indicator F x‖ ≤ C
h₂ : ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x
r : NNReal → (ι → ℝ) → ↑(Set.Ioi 0)
hr₁ : ∀ (c : NNReal), IntegrationParams.Riemann.RCond (r c)
hr₂ :
  ∀ (c : NNReal) (π : TaggedPrepartition B),
    IntegrationParams.Riemann.MemBaseSet B c (r c) π →
      π.IsPartition →
        dist (integralSum (s.indicator F) volume.toBoxAdditive.toSMul π)
            (∫ (x : ι → ℝ) in ↑B, s.indicator F x ∂volume) ≤
          ε / 2
n : ℕ
hn : n ≥ ⌈(↑(r 0 0))⁻¹⌉₊
this : NeZero n
⊢ (prepartition n B).IsSubordinate fun x => r 0 0

Proof state:
case intro
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ ↑B
ε : ℝ
hε : ε > 0
C₀ : ℝ
h₀ : ∀ x ∈ Box.Icc B, ‖F x‖ ≤ C₀
x : ι → ℝ
hx : x ∈ Box.Icc B
⊢ ‖if x ∈ s then F x else 0‖ ≤ 0 ⊔ C₀

Tactic:
split_ifs with hs

Result:
case pos
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ ↑B
ε : ℝ
hε : ε > 0
C₀ : ℝ
h₀ : ∀ x ∈ Box.Icc B, ‖F x‖ ≤ C₀
x : ι → ℝ
hx : x ∈ Box.Icc B
hs : x ∈ s
⊢ ‖F x‖ ≤ 0 ⊔ C₀

case neg
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ ↑B
ε : ℝ
hε : ε > 0
C₀ : ℝ
h₀ : ∀ x ∈ Box.Icc B, ‖F x‖ ≤ C₀
x : ι → ℝ
hx : x ∈ Box.Icc B
hs : x ∉ s
⊢ ‖0‖ ≤ 0 ⊔ C₀

Proof state:
case intro.intro.intro.intro.refine_3
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ ↑B
ε : ℝ
hε : ε > 0
h₁ : ∃ C, ∀ x ∈ Box.Icc B, ‖s.indicator F x‖ ≤ C
h₂ : ∀ᵐ (x : ι → ℝ), ContinuousAt (s.indicator F) x
r : NNReal → (ι → ℝ) → ↑(Set.Ioi 0)
hr₁ : ∀ (c : NNReal), IntegrationParams.Riemann.RCond (r c)
hr₂ :
  ∀ (c : NNReal) (π : TaggedPrepartition B),
    IntegrationParams.Riemann.MemBaseSet B c (r c) π →
      π.IsPartition →
        dist (integralSum (s.indicator F) volume.toBoxAdditive.toSMul π)
            (∫ (x : ι → ℝ) in ↑B, s.indicator F x ∂volume) ≤
          ε / 2
n : ℕ
hn : n ≥ ⌈(↑(r 0 0))⁻¹⌉₊
this : NeZero n
h : IntegrationParams.Riemann.bDistortion = true
⊢ (prepartition n B).distortion ≤ 0

Tactic:
simp only [IntegrationParams.Riemann, Bool.false_eq_true] at h

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ ↑B
ε : ℝ
hε : ε > 0
⊢ ∃ C, ∀ x ∈ Box.Icc B, ‖s.indicator F x‖ ≤ C

Tactic:
obtain ⟨C₀, h₀⟩ := (Box.isCompact_Icc B).exists_bound_of_continuousOn hF.continuousOn

Result:
case intro
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ ↑B
ε : ℝ
hε : ε > 0
C₀ : ℝ
h₀ : ∀ x ∈ Box.Icc B, ‖F x‖ ≤ C₀
⊢ ∃ C, ∀ x ∈ Box.Icc B, ‖s.indicator F x‖ ≤ C

Proof state:
case intro
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ ↑B
ε : ℝ
hε : ε > 0
C₀ : ℝ
h₀ : ∀ x ∈ Box.Icc B, ‖F x‖ ≤ C₀
x : ι → ℝ
hx : x ∈ Box.Icc B
⊢ ‖s.indicator F x‖ ≤ 0 ⊔ C₀

Tactic:
rw [Set.indicator]

Result:
case intro
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
hF : Continuous F
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ ↑B
ε : ℝ
hε : ε > 0
C₀ : ℝ
h₀ : ∀ x ∈ Box.Icc B, ‖F x‖ ≤ C₀
x : ι → ℝ
hx : x ∈ Box.Icc B
⊢ ‖if x ∈ s then F x else 0‖ ≤ 0 ⊔ C₀