case h
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : PartialOrder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), ↑eL x ≤ ↑eL y ↔ x ≤ y
he_vol : MeasurePreserving ↑eL
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : Set.Countable s
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ (x : F), x ∈ interior (Set.Icc a b) \ s → ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF : ∀ (x : F), DF x = ∑ i : Fin (n + 1), ↑(f' i x) (↑(ContinuousLinearEquiv.symm eL) (e i))
Hi : IntegrableOn DF (Set.Icc a b)
he_emb : MeasurableEmbedding ↑eL
x : F
⊢ x ∈ ↑eL ⁻¹' Set.Icc (↑eL a) (↑eL b) ↔ x ∈ Set.Icc a b
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : PartialOrder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), ↑eL x ≤ ↑eL y ↔ x ≤ y
he_vol : MeasurePreserving ↑eL
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : Set.Countable s
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ (x : F), x ∈ interior (Set.Icc a b) \ s → ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF : ∀ (x : F), DF x = ∑ i : Fin (n + 1), ↑(f' i x) (↑(ContinuousLinearEquiv.symm eL) (e i))
Hi : IntegrableOn DF (Set.Icc a b)
he_emb : MeasurableEmbedding ↑eL
⊢ ↑eL ⁻¹' Set.Icc (↑eL a) (↑eL b) = Set.Icc a b
ext1 x
no goals
case h
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : PartialOrder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), ↑eL x ≤ ↑eL y ↔ x ≤ y
he_vol : MeasurePreserving ↑eL
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : Set.Countable s
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ (x : F), x ∈ interior (Set.Icc a b) \ s → ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF : ∀ (x : F), DF x = ∑ i : Fin (n + 1), ↑(f' i x) (↑(ContinuousLinearEquiv.symm eL) (e i))
Hi : IntegrableOn DF (Set.Icc a b)
he_emb : MeasurableEmbedding ↑eL
x : F
⊢ x ∈ ↑eL ⁻¹' Set.Icc (↑eL a) (↑eL b) ↔ x ∈ Set.Icc a b
simp only [Set.mem_preimage, Set.mem_Icc, he_ord]
no goals
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : PartialOrder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), ↑eL x ≤ ↑eL y ↔ x ≤ y
he_vol : MeasurePreserving ↑eL
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : Set.Countable s
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ (x : F), x ∈ interior (Set.Icc a b) \ s → ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF : ∀ (x : F), DF x = ∑ i : Fin (n + 1), ↑(f' i x) (↑(ContinuousLinearEquiv.symm eL) (e i))
Hi : IntegrableOn DF (Set.Icc a b)
he_emb : MeasurableEmbedding ↑eL
hIcc : ↑eL ⁻¹' Set.Icc (↑eL a) (↑eL b) = Set.Icc a b
⊢ Set.Icc (↑eL a) (↑eL b) = ↑(ContinuousLinearEquiv.symm eL) ⁻¹' Set.Icc a b
rw [← hIcc, eL.symm_preimage_preimage]
no goals
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : PartialOrder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), ↑eL x ≤ ↑eL y ↔ x ≤ y
he_vol : MeasurePreserving ↑eL
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : Set.Countable s
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ (x : F), x ∈ interior (Set.Icc a b) \ s → ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF : ∀ (x : F), DF x = ∑ i : Fin (n + 1), ↑(f' i x) (↑(ContinuousLinearEquiv.symm eL) (e i))
Hi : IntegrableOn DF (Set.Icc a b)
he_emb : MeasurableEmbedding ↑eL
hIcc : ↑eL ⁻¹' Set.Icc (↑eL a) (↑eL b) = Set.Icc a b
hIcc' : Set.Icc (↑eL a) (↑eL b) = ↑(ContinuousLinearEquiv.symm eL) ⁻¹' Set.Icc a b
⊢ (∫ (x : F) in Set.Icc a b, DF x) =
    ∫ (x : F) in Set.Icc a b, ∑ i : Fin (n + 1), ↑(f' i x) (↑(ContinuousLinearEquiv.symm eL) (e i))
simp only [hDF]
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : PartialOrder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), ↑eL x ≤ ↑eL y ↔ x ≤ y
he_vol : MeasurePreserving ↑eL
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : Set.Countable s
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ (x : F), x ∈ interior (Set.Icc a b) \ s → ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF : ∀ (x : F), DF x = ∑ i : Fin (n + 1), ↑(f' i x) (↑(ContinuousLinearEquiv.symm eL) (e i))
Hi : IntegrableOn DF (Set.Icc a b)
he_emb : MeasurableEmbedding ↑eL
hIcc : ↑eL ⁻¹' Set.Icc (↑eL a) (↑eL b) = Set.Icc a b
hIcc' : Set.Icc (↑eL a) (↑eL b) = ↑(ContinuousLinearEquiv.symm eL) ⁻¹' Set.Icc a b
⊢ (∫ (x : F) in Set.Icc a b, ∑ i : Fin (n + 1), ↑(f' i x) (↑(ContinuousLinearEquiv.symm eL) (e i))) =
    ∫ (x : F) in ↑eL ⁻¹' Set.Icc (↑eL a) (↑eL b),
      ∑ i : Fin (n + 1), ↑(f' i (↑(ContinuousLinearEquiv.symm eL) (↑eL x))) (↑(ContinuousLinearEquiv.symm eL) (e i))
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : PartialOrder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), ↑eL x ≤ ↑eL y ↔ x ≤ y
he_vol : MeasurePreserving ↑eL
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : Set.Countable s
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ (x : F), x ∈ interior (Set.Icc a b) \ s → ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF : ∀ (x : F), DF x = ∑ i : Fin (n + 1), ↑(f' i x) (↑(ContinuousLinearEquiv.symm eL) (e i))
Hi : IntegrableOn DF (Set.Icc a b)
he_emb : MeasurableEmbedding ↑eL
hIcc : ↑eL ⁻¹' Set.Icc (↑eL a) (↑eL b) = Set.Icc a b
hIcc' : Set.Icc (↑eL a) (↑eL b) = ↑(ContinuousLinearEquiv.symm eL) ⁻¹' Set.Icc a b
⊢ (∫ (x : F) in Set.Icc a b, ∑ i : Fin (n + 1), ↑(f' i x) (↑(ContinuousLinearEquiv.symm eL) (e i))) =
    ∫ (x : (fun x => Fin (n + 1) → ℝ) a) in Set.Icc (↑eL a) (↑eL b),
      ∑ i : Fin (n + 1), ↑(f' i (↑(ContinuousLinearEquiv.symm eL) x)) (↑(ContinuousLinearEquiv.symm eL) (e i))
rw [← he_vol.set_integral_preimage_emb he_emb]
no goals
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : PartialOrder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), ↑eL x ≤ ↑eL y ↔ x ≤ y
he_vol : MeasurePreserving ↑eL
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : Set.Countable s
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ (x : F), x ∈ interior (Set.Icc a b) \ s → ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF : ∀ (x : F), DF x = ∑ i : Fin (n + 1), ↑(f' i x) (↑(ContinuousLinearEquiv.symm eL) (e i))
Hi : IntegrableOn DF (Set.Icc a b)
he_emb : MeasurableEmbedding ↑eL
hIcc : ↑eL ⁻¹' Set.Icc (↑eL a) (↑eL b) = Set.Icc a b
hIcc' : Set.Icc (↑eL a) (↑eL b) = ↑(ContinuousLinearEquiv.symm eL) ⁻¹' Set.Icc a b
⊢ (∫ (x : F) in Set.Icc a b, ∑ i : Fin (n + 1), ↑(f' i x) (↑(ContinuousLinearEquiv.symm eL) (e i))) =
    ∫ (x : F) in ↑eL ⁻¹' Set.Icc (↑eL a) (↑eL b),
      ∑ i : Fin (n + 1), ↑(f' i (↑(ContinuousLinearEquiv.symm eL) (↑eL x))) (↑(ContinuousLinearEquiv.symm eL) (e i))
simp only [hIcc, eL.symm_apply_apply]
case refine_1
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : PartialOrder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), ↑eL x ≤ ↑eL y ↔ x ≤ y
he_vol : MeasurePreserving ↑eL
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : Set.Countable s
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ (x : F), x ∈ interior (Set.Icc a b) \ s → ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF : ∀ (x : F), DF x = ∑ i : Fin (n + 1), ↑(f' i x) (↑(ContinuousLinearEquiv.symm eL) (e i))
Hi : IntegrableOn DF (Set.Icc a b)
he_emb : MeasurableEmbedding ↑eL
hIcc : ↑eL ⁻¹' Set.Icc (↑eL a) (↑eL b) = Set.Icc a b
hIcc' : Set.Icc (↑eL a) (↑eL b) = ↑(ContinuousLinearEquiv.symm eL) ⁻¹' Set.Icc a b
⊢ ∀ (i : Fin (n + 1)), ContinuousOn ((fun i x => f i (↑(ContinuousLinearEquiv.symm eL) x)) i) (Set.Icc (↑eL a) (↑eL b))

case refine_2
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : PartialOrder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), ↑eL x ≤ ↑eL y ↔ x ≤ y
he_vol : MeasurePreserving ↑eL
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : Set.Countable s
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ (x : F), x ∈ interior (Set.Icc a b) \ s → ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF : ∀ (x : F), DF x = ∑ i : Fin (n + 1), ↑(f' i x) (↑(ContinuousLinearEquiv.symm eL) (e i))
Hi : IntegrableOn DF (Set.Icc a b)
he_emb : MeasurableEmbedding ↑eL
hIcc : ↑eL ⁻¹' Set.Icc (↑eL a) (↑eL b) = Set.Icc a b
hIcc' : Set.Icc (↑eL a) (↑eL b) = ↑(ContinuousLinearEquiv.symm eL) ⁻¹' Set.Icc a b
⊢ ∀ (x : Fin (n + 1) → ℝ),
    x ∈ (Set.pi Set.univ fun i => Set.Ioo (↑eL a i) (↑eL b i)) \ ↑(ContinuousLinearEquiv.symm eL) ⁻¹' s →
      ∀ (i : Fin (n + 1)),
        HasFDerivAt ((fun i x => f i (↑(ContinuousLinearEquiv.symm eL) x)) i)
          ((fun i x =>
              ContinuousLinearMap.comp (f' i (↑(ContinuousLinearEquiv.symm eL) x)) ↑(ContinuousLinearEquiv.symm eL))
            i x)
          x

case refine_3
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : PartialOrder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), ↑eL x ≤ ↑eL y ↔ x ≤ y
he_vol : MeasurePreserving ↑eL
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : Set.Countable s
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ (x : F), x ∈ interior (Set.Icc a b) \ s → ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF : ∀ (x : F), DF x = ∑ i : Fin (n + 1), ↑(f' i x) (↑(ContinuousLinearEquiv.symm eL) (e i))
Hi : IntegrableOn DF (Set.Icc a b)
he_emb : MeasurableEmbedding ↑eL
hIcc : ↑eL ⁻¹' Set.Icc (↑eL a) (↑eL b) = Set.Icc a b
hIcc' : Set.Icc (↑eL a) (↑eL b) = ↑(ContinuousLinearEquiv.symm eL) ⁻¹' Set.Icc a b
⊢ IntegrableOn
    (fun x =>
      ∑ i : Fin (n + 1),
        ↑((fun i x =>
                ContinuousLinearMap.comp (f' i (↑(ContinuousLinearEquiv.symm eL) x)) ↑(ContinuousLinearEquiv.symm eL))
              i x)
          (e i))
    (Set.Icc (↑eL a) (↑eL b))
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : PartialOrder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), ↑eL x ≤ ↑eL y ↔ x ≤ y
he_vol : MeasurePreserving ↑eL
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : Set.Countable s
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ (x : F), x ∈ interior (Set.Icc a b) \ s → ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF : ∀ (x : F), DF x = ∑ i : Fin (n + 1), ↑(f' i x) (↑(ContinuousLinearEquiv.symm eL) (e i))
Hi : IntegrableOn DF (Set.Icc a b)
he_emb : MeasurableEmbedding ↑eL
hIcc : ↑eL ⁻¹' Set.Icc (↑eL a) (↑eL b) = Set.Icc a b
hIcc' : Set.Icc (↑eL a) (↑eL b) = ↑(ContinuousLinearEquiv.symm eL) ⁻¹' Set.Icc a b
⊢ (∫ (x : (fun x => Fin (n + 1) → ℝ) a) in Set.Icc (↑eL a) (↑eL b),
      ∑ i : Fin (n + 1), ↑(f' i (↑(ContinuousLinearEquiv.symm eL) x)) (↑(ContinuousLinearEquiv.symm eL) (e i))) =
    ∑ i : Fin (n + 1),
      ((∫ (x : Fin n → ℝ) in Set.Icc (↑eL a ∘ ↑(Fin.succAbove i)) (↑eL b ∘ ↑(Fin.succAbove i)),
          f i (↑(ContinuousLinearEquiv.symm eL) (Fin.insertNth i (↑eL b i) x))) -
        ∫ (x : Fin n → ℝ) in Set.Icc (↑eL a ∘ ↑(Fin.succAbove i)) (↑eL b ∘ ↑(Fin.succAbove i)),
          f i (↑(ContinuousLinearEquiv.symm eL) (Fin.insertNth i (↑eL a i) x)))
refine integral_divergence_of_hasFDerivWithinAt_off_countable' (eL a) (eL b)
  ((he_ord _ _).2 hle) (fun i x => f i (eL.symm x))
  (fun i x => f' i (eL.symm x) ∘L (eL.symm : ℝⁿ⁺¹ →L[ℝ] F)) (eL.symm ⁻¹' s)
  (hs.preimage eL.symm.injective) ?_ ?_ ?_
no goals
case refine_1
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : PartialOrder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), ↑eL x ≤ ↑eL y ↔ x ≤ y
he_vol : MeasurePreserving ↑eL
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : Set.Countable s
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ (x : F), x ∈ interior (Set.Icc a b) \ s → ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF : ∀ (x : F), DF x = ∑ i : Fin (n + 1), ↑(f' i x) (↑(ContinuousLinearEquiv.symm eL) (e i))
Hi : IntegrableOn DF (Set.Icc a b)
he_emb : MeasurableEmbedding ↑eL
hIcc : ↑eL ⁻¹' Set.Icc (↑eL a) (↑eL b) = Set.Icc a b
hIcc' : Set.Icc (↑eL a) (↑eL b) = ↑(ContinuousLinearEquiv.symm eL) ⁻¹' Set.Icc a b
⊢ ∀ (i : Fin (n + 1)), ContinuousOn ((fun i x => f i (↑(ContinuousLinearEquiv.symm eL) x)) i) (Set.Icc (↑eL a) (↑eL b))
exact fun i => (Hc i).comp eL.symm.continuousOn hIcc'.subset
case refine_2
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : PartialOrder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), ↑eL x ≤ ↑eL y ↔ x ≤ y
he_vol : MeasurePreserving ↑eL
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : Set.Countable s
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ (x : F), x ∈ interior (Set.Icc a b) \ s → ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF : ∀ (x : F), DF x = ∑ i : Fin (n + 1), ↑(f' i x) (↑(ContinuousLinearEquiv.symm eL) (e i))
Hi : IntegrableOn DF (Set.Icc a b)
he_emb : MeasurableEmbedding ↑eL
hIcc : ↑eL ⁻¹' Set.Icc (↑eL a) (↑eL b) = Set.Icc a b
hIcc' : Set.Icc (↑eL a) (↑eL b) = ↑(ContinuousLinearEquiv.symm eL) ⁻¹' Set.Icc a b
x : Fin (n + 1) → ℝ
hx : x ∈ (Set.pi Set.univ fun i => Set.Ioo (↑eL a i) (↑eL b i)) \ ↑(ContinuousLinearEquiv.symm eL) ⁻¹' s
i : Fin (n + 1)
⊢ ↑(ContinuousLinearEquiv.symm eL) x ∈ interior (Set.Icc a b)
case refine_2
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : PartialOrder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), ↑eL x ≤ ↑eL y ↔ x ≤ y
he_vol : MeasurePreserving ↑eL
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : Set.Countable s
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ (x : F), x ∈ interior (Set.Icc a b) \ s → ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF : ∀ (x : F), DF x = ∑ i : Fin (n + 1), ↑(f' i x) (↑(ContinuousLinearEquiv.symm eL) (e i))
Hi : IntegrableOn DF (Set.Icc a b)
he_emb : MeasurableEmbedding ↑eL
hIcc : ↑eL ⁻¹' Set.Icc (↑eL a) (↑eL b) = Set.Icc a b
hIcc' : Set.Icc (↑eL a) (↑eL b) = ↑(ContinuousLinearEquiv.symm eL) ⁻¹' Set.Icc a b
⊢ ∀ (x : Fin (n + 1) → ℝ),
    x ∈ (Set.pi Set.univ fun i => Set.Ioo (↑eL a i) (↑eL b i)) \ ↑(ContinuousLinearEquiv.symm eL) ⁻¹' s →
      ∀ (i : Fin (n + 1)),
        HasFDerivAt ((fun i x => f i (↑(ContinuousLinearEquiv.symm eL) x)) i)
          ((fun i x =>
              ContinuousLinearMap.comp (f' i (↑(ContinuousLinearEquiv.symm eL) x)) ↑(ContinuousLinearEquiv.symm eL))
            i x)
          x
refine' fun x hx i => (Hd (eL.symm x) ⟨_, hx.2⟩ i).comp x eL.symm.hasFDerivAt
case refine_2
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : PartialOrder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), ↑eL x ≤ ↑eL y ↔ x ≤ y
he_vol : MeasurePreserving ↑eL
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : Set.Countable s
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ (x : F), x ∈ interior (Set.Icc a b) \ s → ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF : ∀ (x : F), DF x = ∑ i : Fin (n + 1), ↑(f' i x) (↑(ContinuousLinearEquiv.symm eL) (e i))
Hi : IntegrableOn DF (Set.Icc a b)
he_emb : MeasurableEmbedding ↑eL
hIcc : ↑eL ⁻¹' Set.Icc (↑eL a) (↑eL b) = Set.Icc a b
hIcc' : Set.Icc (↑eL a) (↑eL b) = ↑(ContinuousLinearEquiv.symm eL) ⁻¹' Set.Icc a b
x : Fin (n + 1) → ℝ
hx : x ∈ (Set.pi Set.univ fun i => Set.Ioo (↑eL a i) (↑eL b i)) \ ↑(ContinuousLinearEquiv.symm eL) ⁻¹' s
i : Fin (n + 1)
⊢ ↑(ContinuousLinearEquiv.symm eL) x ∈ interior (↑eL ⁻¹' Set.Icc (↑eL a) (↑eL b))
case refine_2
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : PartialOrder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), ↑eL x ≤ ↑eL y ↔ x ≤ y
he_vol : MeasurePreserving ↑eL
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : Set.Countable s
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ (x : F), x ∈ interior (Set.Icc a b) \ s → ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF : ∀ (x : F), DF x = ∑ i : Fin (n + 1), ↑(f' i x) (↑(ContinuousLinearEquiv.symm eL) (e i))
Hi : IntegrableOn DF (Set.Icc a b)
he_emb : MeasurableEmbedding ↑eL
hIcc : ↑eL ⁻¹' Set.Icc (↑eL a) (↑eL b) = Set.Icc a b
hIcc' : Set.Icc (↑eL a) (↑eL b) = ↑(ContinuousLinearEquiv.symm eL) ⁻¹' Set.Icc a b
x : Fin (n + 1) → ℝ
hx : x ∈ (Set.pi Set.univ fun i => Set.Ioo (↑eL a i) (↑eL b i)) \ ↑(ContinuousLinearEquiv.symm eL) ⁻¹' s
i : Fin (n + 1)
⊢ ↑(ContinuousLinearEquiv.symm eL) x ∈ interior (Set.Icc a b)
rw [← hIcc]
case refine_2
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : PartialOrder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), ↑eL x ≤ ↑eL y ↔ x ≤ y
he_vol : MeasurePreserving ↑eL
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : Set.Countable s
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ (x : F), x ∈ interior (Set.Icc a b) \ s → ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF : ∀ (x : F), DF x = ∑ i : Fin (n + 1), ↑(f' i x) (↑(ContinuousLinearEquiv.symm eL) (e i))
Hi : IntegrableOn DF (Set.Icc a b)
he_emb : MeasurableEmbedding ↑eL
hIcc : ↑eL ⁻¹' Set.Icc (↑eL a) (↑eL b) = Set.Icc a b
hIcc' : Set.Icc (↑eL a) (↑eL b) = ↑(ContinuousLinearEquiv.symm eL) ⁻¹' Set.Icc a b
x : Fin (n + 1) → ℝ
hx : x ∈ (Set.pi Set.univ fun i => Set.Ioo (↑eL a i) (↑eL b i)) \ ↑(ContinuousLinearEquiv.symm eL) ⁻¹' s
i : Fin (n + 1)
⊢ ↑(ContinuousLinearEquiv.symm eL) x ∈ ↑eL ⁻¹' interior (Set.Icc (↑eL a) (↑eL b))
case refine_2
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : PartialOrder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), ↑eL x ≤ ↑eL y ↔ x ≤ y
he_vol : MeasurePreserving ↑eL
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : Set.Countable s
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ (x : F), x ∈ interior (Set.Icc a b) \ s → ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF : ∀ (x : F), DF x = ∑ i : Fin (n + 1), ↑(f' i x) (↑(ContinuousLinearEquiv.symm eL) (e i))
Hi : IntegrableOn DF (Set.Icc a b)
he_emb : MeasurableEmbedding ↑eL
hIcc : ↑eL ⁻¹' Set.Icc (↑eL a) (↑eL b) = Set.Icc a b
hIcc' : Set.Icc (↑eL a) (↑eL b) = ↑(ContinuousLinearEquiv.symm eL) ⁻¹' Set.Icc a b
x : Fin (n + 1) → ℝ
hx : x ∈ (Set.pi Set.univ fun i => Set.Ioo (↑eL a i) (↑eL b i)) \ ↑(ContinuousLinearEquiv.symm eL) ⁻¹' s
i : Fin (n + 1)
⊢ ↑(ContinuousLinearEquiv.symm eL) x ∈ interior (↑eL ⁻¹' Set.Icc (↑eL a) (↑eL b))
refine' preimage_interior_subset_interior_preimage eL.continuous _
no goals
case refine_2
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : PartialOrder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), ↑eL x ≤ ↑eL y ↔ x ≤ y
he_vol : MeasurePreserving ↑eL
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : Set.Countable s
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ (x : F), x ∈ interior (Set.Icc a b) \ s → ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF : ∀ (x : F), DF x = ∑ i : Fin (n + 1), ↑(f' i x) (↑(ContinuousLinearEquiv.symm eL) (e i))
Hi : IntegrableOn DF (Set.Icc a b)
he_emb : MeasurableEmbedding ↑eL
hIcc : ↑eL ⁻¹' Set.Icc (↑eL a) (↑eL b) = Set.Icc a b
hIcc' : Set.Icc (↑eL a) (↑eL b) = ↑(ContinuousLinearEquiv.symm eL) ⁻¹' Set.Icc a b
x : Fin (n + 1) → ℝ
hx : x ∈ (Set.pi Set.univ fun i => Set.Ioo (↑eL a i) (↑eL b i)) \ ↑(ContinuousLinearEquiv.symm eL) ⁻¹' s
i : Fin (n + 1)
⊢ ↑(ContinuousLinearEquiv.symm eL) x ∈ ↑eL ⁻¹' interior (Set.Icc (↑eL a) (↑eL b))
simpa only [Set.mem_preimage, eL.apply_symm_apply, ← pi_univ_Icc,
  interior_pi_set (@finite_univ (Fin _) _), interior_Icc] using hx.1
case refine_3
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : PartialOrder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), ↑eL x ≤ ↑eL y ↔ x ≤ y
he_vol : MeasurePreserving ↑eL
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : Set.Countable s
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ (x : F), x ∈ interior (Set.Icc a b) \ s → ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF : ∀ (x : F), DF x = ∑ i : Fin (n + 1), ↑(f' i x) (↑(ContinuousLinearEquiv.symm eL) (e i))
Hi : IntegrableOn DF (Set.Icc a b)
he_emb : MeasurableEmbedding ↑eL
hIcc : ↑eL ⁻¹' Set.Icc (↑eL a) (↑eL b) = Set.Icc a b
hIcc' : Set.Icc (↑eL a) (↑eL b) = ↑(ContinuousLinearEquiv.symm eL) ⁻¹' Set.Icc a b
⊢ IntegrableOn
    ((fun x =>
        ∑ i : Fin (n + 1),
          ↑((fun i x =>
                  ContinuousLinearMap.comp (f' i (↑(ContinuousLinearEquiv.symm eL) x)) ↑(ContinuousLinearEquiv.symm eL))
                i x)
            (e i)) ∘
      ↑eL)
    (Set.Icc a b)
case refine_3
E : Type u
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
n : ℕ
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : PartialOrder F
inst✝¹ : MeasureSpace F
inst✝ : BorelSpace F
eL : F ≃L[ℝ] Fin (n + 1) → ℝ
he_ord : ∀ (x y : F), ↑eL x ≤ ↑eL y ↔ x ≤ y
he_vol : MeasurePreserving ↑eL
f : Fin (n + 1) → F → E
f' : Fin (n + 1) → F → F →L[ℝ] E
s : Set F
hs : Set.Countable s
a b : F
hle : a ≤ b
Hc : ∀ (i : Fin (n + 1)), ContinuousOn (f i) (Set.Icc a b)
Hd : ∀ (x : F), x ∈ interior (Set.Icc a b) \ s → ∀ (i : Fin (n + 1)), HasFDerivAt (f i) (f' i x) x
DF : F → E
hDF : ∀ (x : F), DF x = ∑ i : Fin (n + 1), ↑(f' i x) (↑(ContinuousLinearEquiv.symm eL) (e i))
Hi : IntegrableOn DF (Set.Icc a b)
he_emb : MeasurableEmbedding ↑eL
hIcc : ↑eL ⁻¹' Set.Icc (↑eL a) (↑eL b) = Set.Icc a b
hIcc' : Set.Icc (↑eL a) (↑eL b) = ↑(ContinuousLinearEquiv.symm eL) ⁻¹' Set.Icc a b
⊢ IntegrableOn
    (fun x =>
      ∑ i : Fin (n + 1),
        ↑((fun i x =>
                ContinuousLinearMap.comp (f' i (↑(ContinuousLinearEquiv.symm eL) x)) ↑(ContinuousLinearEquiv.symm eL))
              i x)
          (e i))
    (Set.Icc (↑eL a) (↑eL b))
rw [← he_vol.integrableOn_comp_preimage he_emb, hIcc]