[GOAL]
f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α β : Type u₀
e : α ≃ β
x : f α
⊢ map e.symm (map e x) = x
[PROOFSTEP]
convert (congr_fun (EquivFunctor.map_trans' e e.symm) x).symm
[GOAL]
case h.e'_3
f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α β : Type u₀
e : α ≃ β
x : f α
⊢ x = map (e.trans e.symm) x
[PROOFSTEP]
simp
[GOAL]
f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α β : Type u₀
e : α ≃ β
y : f β
⊢ map e (map e.symm y) = y
[PROOFSTEP]
convert (congr_fun (EquivFunctor.map_trans' e.symm e) y).symm
[GOAL]
case h.e'_3
f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α β : Type u₀
e : α ≃ β
y : f β
⊢ y = map (e.symm.trans e) y
[PROOFSTEP]
simp
[GOAL]
f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α✝ β : Type u₀
e : α✝ ≃ β
α : Type u₀
⊢ mapEquiv f (Equiv.refl α) = Equiv.refl (f α)
[PROOFSTEP]
simp [EquivFunctor.mapEquiv]
[GOAL]
f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α✝ β : Type u₀
e : α✝ ≃ β
α : Type u₀
⊢ { toFun := id, invFun := id, left_inv := (_ : LeftInverse id id), right_inv := (_ : Function.RightInverse id id) } =
    Equiv.refl (f α)
[PROOFSTEP]
rfl
[GOAL]
f : Type u₀ → Type u₁
inst✝ : EquivFunctor f
α β : Type u₀
e : α ≃ β
γ : Type u₀
ab : α ≃ β
bc : β ≃ γ
x : f α
⊢ ↑((mapEquiv f ab).trans (mapEquiv f bc)) x = ↑(mapEquiv f (ab.trans bc)) x
[PROOFSTEP]
simp [mapEquiv, map_trans']
[GOAL]
f : Type u₀ → Type u₁
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
α : Type u₀
⊢ (fun {α β} e => Functor.map ↑e) (Equiv.refl α) = id
[PROOFSTEP]
ext
[GOAL]
case h
f : Type u₀ → Type u₁
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
α : Type u₀
x✝ : f α
⊢ (fun {α β} e => Functor.map ↑e) (Equiv.refl α) x✝ = id x✝
[PROOFSTEP]
apply LawfulFunctor.id_map
[GOAL]
f : Type u₀ → Type u₁
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
α β γ : Type u₀
k : α ≃ β
h : β ≃ γ
⊢ (fun {α β} e => Functor.map ↑e) (k.trans h) = (fun {α β} e => Functor.map ↑e) h ∘ (fun {α β} e => Functor.map ↑e) k
[PROOFSTEP]
ext x
[GOAL]
case h
f : Type u₀ → Type u₁
inst✝¹ : Functor f
inst✝ : LawfulFunctor f
α β γ : Type u₀
k : α ≃ β
h : β ≃ γ
x : f α
⊢ (fun {α β} e => Functor.map ↑e) (k.trans h) x =
    ((fun {α β} e => Functor.map ↑e) h ∘ (fun {α β} e => Functor.map ↑e) k) x
[PROOFSTEP]
apply LawfulFunctor.comp_map k h x
[GOAL]
f : Type u₀ → Type u₁
inst✝¹ : Applicative f
inst✝ : LawfulApplicative f
α β : Type u₀
h : ∀ (γ : Type u₀), Injective pure
e₁ e₂ : α ≃ β
H : mapEquiv f e₁ = mapEquiv f e₂
x : α
⊢ pure (↑e₁ x) = pure (↑e₂ x)
[PROOFSTEP]
simpa [EquivFunctor.map] using Equiv.congr_fun H (pure x)


[GOAL]
ι : Type u_1
I J : Box ι
x y : ι → ℝ
⊢ List.TFAE [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper]
[PROOFSTEP]
tfae_have 1 ↔ 2
[GOAL]
case tfae_1_iff_2
ι : Type u_1
I J : Box ι
x y : ι → ℝ
⊢ I ≤ J ↔ ↑I ⊆ ↑J
ι : Type u_1
I J : Box ι
x y : ι → ℝ
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
⊢ List.TFAE [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper]
[PROOFSTEP]
exact Iff.rfl
[GOAL]
ι : Type u_1
I J : Box ι
x y : ι → ℝ
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
⊢ List.TFAE [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper]
[PROOFSTEP]
tfae_have 2 → 3
[GOAL]
case tfae_2_to_3
ι : Type u_1
I J : Box ι
x y : ι → ℝ
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
⊢ ↑I ⊆ ↑J → Icc I.lower I.upper ⊆ Icc J.lower J.upper
[PROOFSTEP]
intro h
[GOAL]
case tfae_2_to_3
ι : Type u_1
I J : Box ι
x y : ι → ℝ
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
h : ↑I ⊆ ↑J
⊢ Icc I.lower I.upper ⊆ Icc J.lower J.upper
[PROOFSTEP]
simpa [coe_eq_pi, closure_pi_set, lower_ne_upper] using closure_mono h
[GOAL]
ι : Type u_1
I J : Box ι
x y : ι → ℝ
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
tfae_2_to_3 : ↑I ⊆ ↑J → Icc I.lower I.upper ⊆ Icc J.lower J.upper
⊢ List.TFAE [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper]
[PROOFSTEP]
tfae_have 3 ↔ 4
[GOAL]
case tfae_3_iff_4
ι : Type u_1
I J : Box ι
x y : ι → ℝ
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
tfae_2_to_3 : ↑I ⊆ ↑J → Icc I.lower I.upper ⊆ Icc J.lower J.upper
⊢ Icc I.lower I.upper ⊆ Icc J.lower J.upper ↔ J.lower ≤ I.lower ∧ I.upper ≤ J.upper
ι : Type u_1
I J : Box ι
x y : ι → ℝ
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
tfae_2_to_3 : ↑I ⊆ ↑J → Icc I.lower I.upper ⊆ Icc J.lower J.upper
tfae_3_iff_4 : Icc I.lower I.upper ⊆ Icc J.lower J.upper ↔ J.lower ≤ I.lower ∧ I.upper ≤ J.upper
⊢ List.TFAE [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper]
[PROOFSTEP]
exact Icc_subset_Icc_iff I.lower_le_upper
[GOAL]
ι : Type u_1
I J : Box ι
x y : ι → ℝ
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
tfae_2_to_3 : ↑I ⊆ ↑J → Icc I.lower I.upper ⊆ Icc J.lower J.upper
tfae_3_iff_4 : Icc I.lower I.upper ⊆ Icc J.lower J.upper ↔ J.lower ≤ I.lower ∧ I.upper ≤ J.upper
⊢ List.TFAE [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper]
[PROOFSTEP]
tfae_have 4 → 2
[GOAL]
case tfae_4_to_2
ι : Type u_1
I J : Box ι
x y : ι → ℝ
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
tfae_2_to_3 : ↑I ⊆ ↑J → Icc I.lower I.upper ⊆ Icc J.lower J.upper
tfae_3_iff_4 : Icc I.lower I.upper ⊆ Icc J.lower J.upper ↔ J.lower ≤ I.lower ∧ I.upper ≤ J.upper
⊢ J.lower ≤ I.lower ∧ I.upper ≤ J.upper → ↑I ⊆ ↑J
ι : Type u_1
I J : Box ι
x y : ι → ℝ
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
tfae_2_to_3 : ↑I ⊆ ↑J → Icc I.lower I.upper ⊆ Icc J.lower J.upper
tfae_3_iff_4 : Icc I.lower I.upper ⊆ Icc J.lower J.upper ↔ J.lower ≤ I.lower ∧ I.upper ≤ J.upper
tfae_4_to_2 : J.lower ≤ I.lower ∧ I.upper ≤ J.upper → ↑I ⊆ ↑J
⊢ List.TFAE [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper]
[PROOFSTEP]
exact fun h x hx i ↦ Ioc_subset_Ioc (h.1 i) (h.2 i) (hx i)
[GOAL]
ι : Type u_1
I J : Box ι
x y : ι → ℝ
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
tfae_2_to_3 : ↑I ⊆ ↑J → Icc I.lower I.upper ⊆ Icc J.lower J.upper
tfae_3_iff_4 : Icc I.lower I.upper ⊆ Icc J.lower J.upper ↔ J.lower ≤ I.lower ∧ I.upper ≤ J.upper
tfae_4_to_2 : J.lower ≤ I.lower ∧ I.upper ≤ J.upper → ↑I ⊆ ↑J
⊢ List.TFAE [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper]
[PROOFSTEP]
tfae_finish
[GOAL]
ι : Type u_1
I J : Box ι
x y : ι → ℝ
⊢ Injective toSet
[PROOFSTEP]
rintro ⟨l₁, u₁, h₁⟩ ⟨l₂, u₂, h₂⟩ h
[GOAL]
case mk.mk
ι : Type u_1
I J : Box ι
x y l₁ u₁ : ι → ℝ
h₁ : ∀ (i : ι), l₁ i < u₁ i
l₂ u₂ : ι → ℝ
h₂ : ∀ (i : ι), l₂ i < u₂ i
h : ↑{ lower := l₁, upper := u₁, lower_lt_upper := h₁ } = ↑{ lower := l₂, upper := u₂, lower_lt_upper := h₂ }
⊢ { lower := l₁, upper := u₁, lower_lt_upper := h₁ } = { lower := l₂, upper := u₂, lower_lt_upper := h₂ }
[PROOFSTEP]
simp only [Subset.antisymm_iff, coe_subset_coe, le_iff_bounds] at h
[GOAL]
case mk.mk
ι : Type u_1
I J : Box ι
x y l₁ u₁ : ι → ℝ
h₁ : ∀ (i : ι), l₁ i < u₁ i
l₂ u₂ : ι → ℝ
h₂ : ∀ (i : ι), l₂ i < u₂ i
h : (l₂ ≤ l₁ ∧ u₁ ≤ u₂) ∧ l₁ ≤ l₂ ∧ u₂ ≤ u₁
⊢ { lower := l₁, upper := u₁, lower_lt_upper := h₁ } = { lower := l₂, upper := u₂, lower_lt_upper := h₂ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_lower
ι : Type u_1
I J : Box ι
x y l₁ u₁ : ι → ℝ
h₁ : ∀ (i : ι), l₁ i < u₁ i
l₂ u₂ : ι → ℝ
h₂ : ∀ (i : ι), l₂ i < u₂ i
h : (l₂ ≤ l₁ ∧ u₁ ≤ u₂) ∧ l₁ ≤ l₂ ∧ u₂ ≤ u₁
⊢ l₁ = l₂
case mk.mk.e_upper
ι : Type u_1
I J : Box ι
x y l₁ u₁ : ι → ℝ
h₁ : ∀ (i : ι), l₁ i < u₁ i
l₂ u₂ : ι → ℝ
h₂ : ∀ (i : ι), l₂ i < u₂ i
h : (l₂ ≤ l₁ ∧ u₁ ≤ u₂) ∧ l₁ ≤ l₂ ∧ u₂ ≤ u₁
⊢ u₁ = u₂
[PROOFSTEP]
exacts [le_antisymm h.2.1 h.1.1, le_antisymm h.1.2 h.2.2]
[GOAL]
ι : Type u_1
I J : Box ι
x y : ι → ℝ
⊢ Option.isSome ⊥ = true ↔ Set.Nonempty ↑⊥
[PROOFSTEP]
erw [Option.isSome]
[GOAL]
ι : Type u_1
I J : Box ι
x y : ι → ℝ
⊢ (match ⊥ with
      | some val => true
      | none => false) =
      true ↔
    Set.Nonempty ↑⊥
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
I✝ J : Box ι
x y : ι → ℝ
I : Box ι
⊢ Option.isSome ↑I = true ↔ Set.Nonempty ↑↑I
[PROOFSTEP]
erw [Option.isSome]
[GOAL]
ι : Type u_1
I✝ J : Box ι
x y : ι → ℝ
I : Box ι
⊢ (match ↑I with
      | some val => true
      | none => false) =
      true ↔
    Set.Nonempty ↑↑I
[PROOFSTEP]
simp [I.nonempty_coe]
[GOAL]
ι : Type u_1
I✝ J : Box ι
x y : ι → ℝ
I : WithBot (Box ι)
⊢ ⋃ (J : Box ι) (_ : ↑J = I), ↑J = ↑I
[PROOFSTEP]
induction I using WithBot.recBotCoe
[GOAL]
case bot
ι : Type u_1
I J : Box ι
x y : ι → ℝ
⊢ ⋃ (J : Box ι) (_ : ↑J = ⊥), ↑J = ↑⊥
[PROOFSTEP]
simp [WithBot.coe_eq_coe]
[GOAL]
case coe
ι : Type u_1
I J : Box ι
x y : ι → ℝ
a✝ : Box ι
⊢ ⋃ (J : Box ι) (_ : ↑J = ↑a✝), ↑J = ↑↑a✝
[PROOFSTEP]
simp [WithBot.coe_eq_coe]
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
I J : WithBot (Box ι)
⊢ ↑I ⊆ ↑J ↔ I ≤ J
[PROOFSTEP]
induction I using WithBot.recBotCoe
[GOAL]
case bot
ι : Type u_1
I J✝ : Box ι
x y : ι → ℝ
J : WithBot (Box ι)
⊢ ↑⊥ ⊆ ↑J ↔ ⊥ ≤ J
[PROOFSTEP]
simp
[GOAL]
case coe
ι : Type u_1
I J✝ : Box ι
x y : ι → ℝ
J : WithBot (Box ι)
a✝ : Box ι
⊢ ↑↑a✝ ⊆ ↑J ↔ ↑a✝ ≤ J
[PROOFSTEP]
induction J using WithBot.recBotCoe
[GOAL]
case coe.bot
ι : Type u_1
I J : Box ι
x y : ι → ℝ
a✝ : Box ι
⊢ ↑↑a✝ ⊆ ↑⊥ ↔ ↑a✝ ≤ ⊥
[PROOFSTEP]
simp [subset_empty_iff]
[GOAL]
case coe.coe
ι : Type u_1
I J : Box ι
x y : ι → ℝ
a✝¹ a✝ : Box ι
⊢ ↑↑a✝¹ ⊆ ↑↑a✝ ↔ ↑a✝¹ ≤ ↑a✝
[PROOFSTEP]
simp [le_def]
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
I J : WithBot (Box ι)
⊢ ↑I = ↑J ↔ I = J
[PROOFSTEP]
simp only [Subset.antisymm_iff, ← le_antisymm_iff, withBotCoe_subset_iff]
[GOAL]
ι : Type u_1
I J : Box ι
x y l u : ι → ℝ
⊢ mk' l u = ⊥ ↔ ∃ i, u i ≤ l i
[PROOFSTEP]
rw [mk']
[GOAL]
ι : Type u_1
I J : Box ι
x y l u : ι → ℝ
⊢ (if h : ∀ (i : ι), l i < u i then ↑{ lower := l, upper := u, lower_lt_upper := h } else ⊥) = ⊥ ↔ ∃ i, u i ≤ l i
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
I J : Box ι
x y l u : ι → ℝ
h : ∀ (i : ι), l i < u i
⊢ ↑{ lower := l, upper := u, lower_lt_upper := h } = ⊥ ↔ ∃ i, u i ≤ l i
[PROOFSTEP]
simpa using h
[GOAL]
case neg
ι : Type u_1
I J : Box ι
x y l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
⊢ ⊥ = ⊥ ↔ ∃ i, u i ≤ l i
[PROOFSTEP]
simpa using h
[GOAL]
ι : Type u_1
I J : Box ι
x y l u : ι → ℝ
⊢ mk' l u = ↑I ↔ l = I.lower ∧ u = I.upper
[PROOFSTEP]
cases' I with lI uI hI
[GOAL]
case mk
ι : Type u_1
J : Box ι
x y l u lI uI : ι → ℝ
hI : ∀ (i : ι), lI i < uI i
⊢ mk' l u = ↑{ lower := lI, upper := uI, lower_lt_upper := hI } ↔
    l = { lower := lI, upper := uI, lower_lt_upper := hI }.lower ∧
      u = { lower := lI, upper := uI, lower_lt_upper := hI }.upper
[PROOFSTEP]
rw [mk']
[GOAL]
case mk
ι : Type u_1
J : Box ι
x y l u lI uI : ι → ℝ
hI : ∀ (i : ι), lI i < uI i
⊢ (if h : ∀ (i : ι), l i < u i then ↑{ lower := l, upper := u, lower_lt_upper := h } else ⊥) =
      ↑{ lower := lI, upper := uI, lower_lt_upper := hI } ↔
    l = { lower := lI, upper := uI, lower_lt_upper := hI }.lower ∧
      u = { lower := lI, upper := uI, lower_lt_upper := hI }.upper
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
J : Box ι
x y l u lI uI : ι → ℝ
hI : ∀ (i : ι), lI i < uI i
h : ∀ (i : ι), l i < u i
⊢ ↑{ lower := l, upper := u, lower_lt_upper := h } = ↑{ lower := lI, upper := uI, lower_lt_upper := hI } ↔
    l = { lower := lI, upper := uI, lower_lt_upper := hI }.lower ∧
      u = { lower := lI, upper := uI, lower_lt_upper := hI }.upper
[PROOFSTEP]
simp [WithBot.coe_eq_coe]
[GOAL]
case neg
ι : Type u_1
J : Box ι
x y l u lI uI : ι → ℝ
hI : ∀ (i : ι), lI i < uI i
h : ¬∀ (i : ι), l i < u i
⊢ ⊥ = ↑{ lower := lI, upper := uI, lower_lt_upper := hI } ↔
    l = { lower := lI, upper := uI, lower_lt_upper := hI }.lower ∧
      u = { lower := lI, upper := uI, lower_lt_upper := hI }.upper
[PROOFSTEP]
suffices l = lI → u ≠ uI by simpa
[GOAL]
ι : Type u_1
J : Box ι
x y l u lI uI : ι → ℝ
hI : ∀ (i : ι), lI i < uI i
h : ¬∀ (i : ι), l i < u i
this : l = lI → u ≠ uI
⊢ ⊥ = ↑{ lower := lI, upper := uI, lower_lt_upper := hI } ↔
    l = { lower := lI, upper := uI, lower_lt_upper := hI }.lower ∧
      u = { lower := lI, upper := uI, lower_lt_upper := hI }.upper
[PROOFSTEP]
simpa
[GOAL]
case neg
ι : Type u_1
J : Box ι
x y l u lI uI : ι → ℝ
hI : ∀ (i : ι), lI i < uI i
h : ¬∀ (i : ι), l i < u i
⊢ l = lI → u ≠ uI
[PROOFSTEP]
rintro rfl rfl
[GOAL]
case neg
ι : Type u_1
J : Box ι
x y l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
hI : ∀ (i : ι), l i < u i
⊢ False
[PROOFSTEP]
exact h hI
[GOAL]
ι : Type u_1
I J : Box ι
x y l u : ι → ℝ
⊢ ↑(mk' l u) = Set.pi univ fun i => Ioc (l i) (u i)
[PROOFSTEP]
rw [mk']
[GOAL]
ι : Type u_1
I J : Box ι
x y l u : ι → ℝ
⊢ ↑(if h : ∀ (i : ι), l i < u i then ↑{ lower := l, upper := u, lower_lt_upper := h } else ⊥) =
    Set.pi univ fun i => Ioc (l i) (u i)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
I J : Box ι
x y l u : ι → ℝ
h : ∀ (i : ι), l i < u i
⊢ ↑↑{ lower := l, upper := u, lower_lt_upper := h } = Set.pi univ fun i => Ioc (l i) (u i)
[PROOFSTEP]
exact coe_eq_pi _
[GOAL]
case neg
ι : Type u_1
I J : Box ι
x y l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
⊢ ↑⊥ = Set.pi univ fun i => Ioc (l i) (u i)
[PROOFSTEP]
rcases not_forall.mp h with ⟨i, hi⟩
[GOAL]
case neg.intro
ι : Type u_1
I J : Box ι
x y l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
i : ι
hi : ¬l i < u i
⊢ ↑⊥ = Set.pi univ fun i => Ioc (l i) (u i)
[PROOFSTEP]
rw [coe_bot, univ_pi_eq_empty]
[GOAL]
case neg.intro
ι : Type u_1
I J : Box ι
x y l u : ι → ℝ
h : ¬∀ (i : ι), l i < u i
i : ι
hi : ¬l i < u i
⊢ Ioc (l ?m.301759) (u ?m.301759) = ∅
ι : Type u_1 I J : Box ι x y l u : ι → ℝ h : ¬∀ (i : ι), l i < u i i : ι hi : ¬l i < u i ⊢ ι
[PROOFSTEP]
exact Ioc_eq_empty hi
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
I J : WithBot (Box ι)
⊢ ↑(I ⊓ J) = ↑I ∩ ↑J
[PROOFSTEP]
induction I using WithBot.recBotCoe
[GOAL]
case bot
ι : Type u_1
I J✝ : Box ι
x y : ι → ℝ
J : WithBot (Box ι)
⊢ ↑(⊥ ⊓ J) = ↑⊥ ∩ ↑J
[PROOFSTEP]
change ∅ = _
[GOAL]
case bot
ι : Type u_1
I J✝ : Box ι
x y : ι → ℝ
J : WithBot (Box ι)
⊢ ∅ = ↑⊥ ∩ ↑J
[PROOFSTEP]
simp
[GOAL]
case coe
ι : Type u_1
I J✝ : Box ι
x y : ι → ℝ
J : WithBot (Box ι)
a✝ : Box ι
⊢ ↑(↑a✝ ⊓ J) = ↑↑a✝ ∩ ↑J
[PROOFSTEP]
induction J using WithBot.recBotCoe
[GOAL]
case coe.bot
ι : Type u_1
I J : Box ι
x y : ι → ℝ
a✝ : Box ι
⊢ ↑(↑a✝ ⊓ ⊥) = ↑↑a✝ ∩ ↑⊥
[PROOFSTEP]
change ∅ = _
[GOAL]
case coe.bot
ι : Type u_1
I J : Box ι
x y : ι → ℝ
a✝ : Box ι
⊢ ∅ = ↑↑a✝ ∩ ↑⊥
[PROOFSTEP]
simp
[GOAL]
case coe.coe
ι : Type u_1
I J : Box ι
x y : ι → ℝ
a✝¹ a✝ : Box ι
⊢ ↑(↑a✝¹ ⊓ ↑a✝) = ↑↑a✝¹ ∩ ↑↑a✝
[PROOFSTEP]
change ((mk' _ _ : WithBot (Box ι)) : Set (ι → ℝ)) = _
[GOAL]
case coe.coe
ι : Type u_1
I J : Box ι
x y : ι → ℝ
a✝¹ a✝ : Box ι
⊢ ↑(mk' (fun i => (a✝¹.lower ⊔ a✝.lower) i) fun i => (a✝¹.upper ⊓ a✝.upper) i) = ↑↑a✝¹ ∩ ↑↑a✝
[PROOFSTEP]
simp only [coe_eq_pi, ← pi_inter_distrib, Ioc_inter_Ioc, Pi.sup_apply, Pi.inf_apply, coe_mk', coe_coe]
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
src✝¹ : SemilatticeSup (WithBot (Box ι)) := WithBot.semilatticeSup
src✝ : Inf (WithBot (Box ι)) := WithBot.inf
I J : WithBot (Box ι)
⊢ I ⊓ J ≤ I
[PROOFSTEP]
rw [← withBotCoe_subset_iff, coe_inf]
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
src✝¹ : SemilatticeSup (WithBot (Box ι)) := WithBot.semilatticeSup
src✝ : Inf (WithBot (Box ι)) := WithBot.inf
I J : WithBot (Box ι)
⊢ ↑I ∩ ↑J ⊆ ↑I
[PROOFSTEP]
exact inter_subset_left _ _
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
src✝¹ : SemilatticeSup (WithBot (Box ι)) := WithBot.semilatticeSup
src✝ : Inf (WithBot (Box ι)) := WithBot.inf
I J : WithBot (Box ι)
⊢ I ⊓ J ≤ J
[PROOFSTEP]
rw [← withBotCoe_subset_iff, coe_inf]
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
src✝¹ : SemilatticeSup (WithBot (Box ι)) := WithBot.semilatticeSup
src✝ : Inf (WithBot (Box ι)) := WithBot.inf
I J : WithBot (Box ι)
⊢ ↑I ∩ ↑J ⊆ ↑J
[PROOFSTEP]
exact inter_subset_right _ _
[GOAL]
ι : Type u_1
I✝ J : Box ι
x y : ι → ℝ
src✝¹ : SemilatticeSup (WithBot (Box ι)) := WithBot.semilatticeSup
src✝ : Inf (WithBot (Box ι)) := WithBot.inf
I J₁ J₂ : WithBot (Box ι)
h₁ : I ≤ J₁
h₂ : I ≤ J₂
⊢ I ≤ J₁ ⊓ J₂
[PROOFSTEP]
simp only [← withBotCoe_subset_iff, coe_inf] at *
[GOAL]
ι : Type u_1
I✝ J : Box ι
x y : ι → ℝ
src✝¹ : SemilatticeSup (WithBot (Box ι)) := WithBot.semilatticeSup
src✝ : Inf (WithBot (Box ι)) := WithBot.inf
I J₁ J₂ : WithBot (Box ι)
h₁ : ↑I ⊆ ↑J₁
h₂ : ↑I ⊆ ↑J₂
⊢ ↑I ⊆ ↑J₁ ∩ ↑J₂
[PROOFSTEP]
exact subset_inter h₁ h₂
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
I J : WithBot (Box ι)
⊢ Disjoint ↑I ↑J ↔ Disjoint I J
[PROOFSTEP]
simp only [disjoint_iff_inf_le, ← withBotCoe_subset_iff, coe_inf]
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
I J : WithBot (Box ι)
⊢ ↑I ⊓ ↑J ≤ ⊥ ↔ ↑I ∩ ↑J ⊆ ↑⊥
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
I J : Box ι
x y : ι → ℝ
⊢ ¬Disjoint ↑I ↑J ↔ Set.Nonempty (↑I ∩ ↑J)
[PROOFSTEP]
rw [disjoint_coe, Set.not_disjoint_iff_nonempty_inter]
[GOAL]
ι : Type u_1
I✝ J : Box ι
x✝ y : ι → ℝ
n : ℕ
I : Box (Fin (n + 1))
i : Fin (n + 1)
x : ℝ
hx : x ∈ Ioc (lower I i) (upper I i)
⊢ MapsTo (Fin.insertNth i x) ↑(face I i) ↑I
[PROOFSTEP]
intro y hy
[GOAL]
ι : Type u_1
I✝ J : Box ι
x✝ y✝ : ι → ℝ
n : ℕ
I : Box (Fin (n + 1))
i : Fin (n + 1)
x : ℝ
hx : x ∈ Ioc (lower I i) (upper I i)
y : Fin n → ℝ
hy : y ∈ ↑(face I i)
⊢ Fin.insertNth i x y ∈ ↑I
[PROOFSTEP]
simp_rw [mem_coe, mem_def, i.forall_iff_succAbove, Fin.insertNth_apply_same, Fin.insertNth_apply_succAbove]
[GOAL]
ι : Type u_1
I✝ J : Box ι
x✝ y✝ : ι → ℝ
n : ℕ
I : Box (Fin (n + 1))
i : Fin (n + 1)
x : ℝ
hx : x ∈ Ioc (lower I i) (upper I i)
y : Fin n → ℝ
hy : y ∈ ↑(face I i)
⊢ x ∈ Ioc (lower I i) (upper I i) ∧ ∀ (j : Fin n), y j ∈ Ioc (lower I (Fin.succAbove i j)) (upper I (Fin.succAbove i j))
[PROOFSTEP]
exact ⟨hx, hy⟩
[GOAL]
ι : Type u_1
I✝ J : Box ι
x y : ι → ℝ
I : Box ι
⊢ ∃ J,
    (∀ (n : ℕ), ↑Box.Icc (↑J n) ⊆ ↑Box.Ioo I) ∧
      Tendsto (lower ∘ ↑J) atTop (𝓝 I.lower) ∧ Tendsto (upper ∘ ↑J) atTop (𝓝 I.upper)
[PROOFSTEP]
choose a b ha_anti hb_mono ha_mem hb_mem hab ha_tendsto hb_tendsto using fun i ↦
  exists_seq_strictAnti_strictMono_tendsto (I.lower_lt_upper i)
[GOAL]
ι : Type u_1
I✝ J : Box ι
x y : ι → ℝ
I : Box ι
a b : ι → ℕ → ℝ
ha_anti : ∀ (i : ι), StrictAnti (a i)
hb_mono : ∀ (i : ι), StrictMono (b i)
ha_mem : ∀ (i : ι) (k : ℕ), a i k ∈ Ioo (lower I i) (upper I i)
hb_mem : ∀ (i : ι) (l : ℕ), b i l ∈ Ioo (lower I i) (upper I i)
hab : ∀ (i : ι) (k l : ℕ), a i k < b i l
ha_tendsto : ∀ (i : ι), Tendsto (a i) atTop (𝓝 (lower I i))
hb_tendsto : ∀ (i : ι), Tendsto (b i) atTop (𝓝 (upper I i))
⊢ ∃ J,
    (∀ (n : ℕ), ↑Box.Icc (↑J n) ⊆ ↑Box.Ioo I) ∧
      Tendsto (lower ∘ ↑J) atTop (𝓝 I.lower) ∧ Tendsto (upper ∘ ↑J) atTop (𝓝 I.upper)
[PROOFSTEP]
exact
  ⟨⟨fun k ↦ ⟨flip a k, flip b k, fun i ↦ hab _ _ _⟩, fun k l hkl ↦
      le_iff_bounds.2 ⟨fun i ↦ (ha_anti i).antitone hkl, fun i ↦ (hb_mono i).monotone hkl⟩⟩,
    fun n x hx i _ ↦ ⟨(ha_mem _ _).1.trans_le (hx.1 _), (hx.2 _).trans_lt (hb_mem _ _).2⟩, tendsto_pi_nhds.2 ha_tendsto,
    tendsto_pi_nhds.2 hb_tendsto⟩
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), upper I i - lower I i = (upper J i - lower J i) / r
⊢ distortion I = distortion J
[PROOFSTEP]
simp only [distortion, nndist_pi_def, Real.nndist_eq', h, map_div₀]
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), upper I i - lower I i = (upper J i - lower J i) / r
⊢ (Finset.sup Finset.univ fun i =>
      (Finset.sup Finset.univ fun b => ↑Real.nnabs (upper J b - lower J b) / ↑Real.nnabs r) /
        (↑Real.nnabs (upper J i - lower J i) / ↑Real.nnabs r)) =
    Finset.sup Finset.univ fun i =>
      (Finset.sup Finset.univ fun b => ↑Real.nnabs (upper J b - lower J b)) / ↑Real.nnabs (upper J i - lower J i)
[PROOFSTEP]
congr 1 with i
[GOAL]
case e_f.h.a
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), upper I i - lower I i = (upper J i - lower J i) / r
i : ι
⊢ ↑((Finset.sup Finset.univ fun b => ↑Real.nnabs (upper J b - lower J b) / ↑Real.nnabs r) /
        (↑Real.nnabs (upper J i - lower J i) / ↑Real.nnabs r)) =
    ↑((Finset.sup Finset.univ fun b => ↑Real.nnabs (upper J b - lower J b)) / ↑Real.nnabs (upper J i - lower J i))
[PROOFSTEP]
have : 0 < r := by
  by_contra hr
  have := div_nonpos_of_nonneg_of_nonpos (sub_nonneg.2 <| J.lower_le_upper i) (not_lt.1 hr)
  rw [← h] at this
  exact this.not_lt (sub_pos.2 <| I.lower_lt_upper i)
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), upper I i - lower I i = (upper J i - lower J i) / r
i : ι
⊢ 0 < r
[PROOFSTEP]
by_contra hr
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), upper I i - lower I i = (upper J i - lower J i) / r
i : ι
hr : ¬0 < r
⊢ False
[PROOFSTEP]
have := div_nonpos_of_nonneg_of_nonpos (sub_nonneg.2 <| J.lower_le_upper i) (not_lt.1 hr)
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), upper I i - lower I i = (upper J i - lower J i) / r
i : ι
hr : ¬0 < r
this : (upper J i - lower J i) / r ≤ 0
⊢ False
[PROOFSTEP]
rw [← h] at this
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), upper I i - lower I i = (upper J i - lower J i) / r
i : ι
hr : ¬0 < r
this : upper I i - lower I i ≤ 0
⊢ False
[PROOFSTEP]
exact this.not_lt (sub_pos.2 <| I.lower_lt_upper i)
[GOAL]
case e_f.h.a
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), upper I i - lower I i = (upper J i - lower J i) / r
i : ι
this : 0 < r
⊢ ↑((Finset.sup Finset.univ fun b => ↑Real.nnabs (upper J b - lower J b) / ↑Real.nnabs r) /
        (↑Real.nnabs (upper J i - lower J i) / ↑Real.nnabs r)) =
    ↑((Finset.sup Finset.univ fun b => ↑Real.nnabs (upper J b - lower J b)) / ↑Real.nnabs (upper J i - lower J i))
[PROOFSTEP]
have hn0 := (map_ne_zero Real.nnabs).2 this.ne'
[GOAL]
case e_f.h.a
ι : Type u_1
I✝ J✝ : Box ι
x y : ι → ℝ
inst✝ : Fintype ι
I J : Box ι
r : ℝ
h : ∀ (i : ι), upper I i - lower I i = (upper J i - lower J i) / r
i : ι
this : 0 < r
hn0 : ↑Real.nnabs r ≠ 0
⊢ ↑((Finset.sup Finset.univ fun b => ↑Real.nnabs (upper J b - lower J b) / ↑Real.nnabs r) /
        (↑Real.nnabs (upper J i - lower J i) / ↑Real.nnabs r)) =
    ↑((Finset.sup Finset.univ fun b => ↑Real.nnabs (upper J b - lower J b)) / ↑Real.nnabs (upper J i - lower J i))
[PROOFSTEP]
simp_rw [NNReal.finset_sup_div, div_div_div_cancel_right _ hn0]
[GOAL]
ι : Type u_1
I✝ J : Box ι
x y : ι → ℝ
inst✝ : Fintype ι
I : Box ι
i : ι
⊢ nndist I.lower I.upper / nndist (lower I i) (upper I i) * nndist (lower I i) (upper I i) ≤
    distortion I * nndist (lower I i) (upper I i)
[PROOFSTEP]
apply mul_le_mul_right'
[GOAL]
case bc
ι : Type u_1
I✝ J : Box ι
x y : ι → ℝ
inst✝ : Fintype ι
I : Box ι
i : ι
⊢ nndist I.lower I.upper / nndist (lower I i) (upper I i) ≤ distortion I
[PROOFSTEP]
apply Finset.le_sup (Finset.mem_univ i)
[GOAL]
ι : Type u_1
I✝ J : Box ι
x y : ι → ℝ
inst✝ : Fintype ι
I : Box ι
i : ι
⊢ dist I.lower I.upper ≤ ↑(distortion I) * (upper I i - lower I i)
[PROOFSTEP]
have A : I.lower i - I.upper i < 0 := sub_neg.2 (I.lower_lt_upper i)
[GOAL]
ι : Type u_1
I✝ J : Box ι
x y : ι → ℝ
inst✝ : Fintype ι
I : Box ι
i : ι
A : lower I i - upper I i < 0
⊢ dist I.lower I.upper ≤ ↑(distortion I) * (upper I i - lower I i)
[PROOFSTEP]
simpa only [← NNReal.coe_le_coe, ← dist_nndist, NNReal.coe_mul, Real.dist_eq, abs_of_neg A, neg_sub] using
  I.nndist_le_distortion_mul i
[GOAL]
ι : Type u_1
I✝ J : Box ι
x✝ y✝ : ι → ℝ
inst✝ : Fintype ι
I : Box ι
i : ι
c : ℝ≥0
h : distortion I ≤ c
this : 0 ≤ ↑c * (upper I i - lower I i)
x : ι → ℝ
hx : x ∈ ↑Box.Icc I
y : ι → ℝ
hy : y ∈ ↑Box.Icc I
⊢ ↑(distortion I) * (upper I i - lower I i) ≤ ↑c * (upper I i - lower I i)
[PROOFSTEP]
gcongr
[GOAL]
case a0
ι : Type u_1
I✝ J : Box ι
x✝ y✝ : ι → ℝ
inst✝ : Fintype ι
I : Box ι
i : ι
c : ℝ≥0
h : distortion I ≤ c
this : 0 ≤ ↑c * (upper I i - lower I i)
x : ι → ℝ
hx : x ∈ ↑Box.Icc I
y : ι → ℝ
hy : y ∈ ↑Box.Icc I
⊢ 0 ≤ upper I i - lower I i
[PROOFSTEP]
exact sub_nonneg.2 (I.lower_le_upper i)


[GOAL]
𝕜 : Type u_1
inst✝⁷ : CommRing 𝕜
V : Type u_2
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module 𝕜 V
inst✝⁴ : MeasurableSpace V
W : Type u_3
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
r : ℂ
⊢ fourierIntegral e μ L (r • f) = r • fourierIntegral e μ L f
[PROOFSTEP]
ext1 w
[GOAL]
case h
𝕜 : Type u_1
inst✝⁷ : CommRing 𝕜
V : Type u_2
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module 𝕜 V
inst✝⁴ : MeasurableSpace V
W : Type u_3
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
r : ℂ
w : W
⊢ fourierIntegral e μ L (r • f) w = (r • fourierIntegral e μ L f) w
[PROOFSTEP]
simp only [Pi.smul_apply, fourierIntegral, ← integral_smul]
[GOAL]
case h
𝕜 : Type u_1
inst✝⁷ : CommRing 𝕜
V : Type u_2
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module 𝕜 V
inst✝⁴ : MeasurableSpace V
W : Type u_3
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
r : ℂ
w : W
⊢ ∫ (v : V), ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • r • f v ∂μ =
    ∫ (a : V), r • ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L a) w))) • f a ∂μ
[PROOFSTEP]
congr
[GOAL]
case h.e_f
𝕜 : Type u_1
inst✝⁷ : CommRing 𝕜
V : Type u_2
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module 𝕜 V
inst✝⁴ : MeasurableSpace V
W : Type u_3
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
r : ℂ
w : W
⊢ (fun v => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • r • f v) = fun a =>
    r • ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L a) w))) • f a
[PROOFSTEP]
funext
[GOAL]
case h.e_f.h
𝕜 : Type u_1
inst✝⁷ : CommRing 𝕜
V : Type u_2
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module 𝕜 V
inst✝⁴ : MeasurableSpace V
W : Type u_3
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
r : ℂ
w : W
x✝ : V
⊢ ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L x✝) w))) • r • f x✝ = r • ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L x✝) w))) • f x✝
[PROOFSTEP]
rw [smul_comm]
[GOAL]
𝕜 : Type u_1
inst✝⁷ : CommRing 𝕜
V : Type u_2
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module 𝕜 V
inst✝⁴ : MeasurableSpace V
W : Type u_3
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
w : W
⊢ ‖fourierIntegral e μ L f w‖ ≤ ∫ (v : V), ‖f v‖ ∂μ
[PROOFSTEP]
refine' (norm_integral_le_integral_norm _).trans (le_of_eq _)
[GOAL]
𝕜 : Type u_1
inst✝⁷ : CommRing 𝕜
V : Type u_2
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module 𝕜 V
inst✝⁴ : MeasurableSpace V
W : Type u_3
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
w : W
⊢ ∫ (a : V), ‖↑(↑e (↑Multiplicative.ofAdd (-↑(↑L a) w))) • f a‖ ∂μ = ∫ (v : V), ‖f v‖ ∂μ
[PROOFSTEP]
simp_rw [norm_smul, Complex.norm_eq_abs, abs_coe_circle, one_mul]
[GOAL]
𝕜 : Type u_1
inst✝⁹ : CommRing 𝕜
V : Type u_2
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module 𝕜 V
inst✝⁶ : MeasurableSpace V
W : Type u_3
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module 𝕜 W
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : MeasurableAdd V
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
inst✝ : Measure.IsAddRightInvariant μ
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
v₀ : V
⊢ fourierIntegral e μ L (f ∘ fun v => v + v₀) = fun w =>
    ↑(↑e (↑Multiplicative.ofAdd (↑(↑L v₀) w))) • fourierIntegral e μ L f w
[PROOFSTEP]
ext1 w
[GOAL]
case h
𝕜 : Type u_1
inst✝⁹ : CommRing 𝕜
V : Type u_2
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module 𝕜 V
inst✝⁶ : MeasurableSpace V
W : Type u_3
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module 𝕜 W
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : MeasurableAdd V
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
inst✝ : Measure.IsAddRightInvariant μ
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
v₀ : V
w : W
⊢ fourierIntegral e μ L (f ∘ fun v => v + v₀) w = ↑(↑e (↑Multiplicative.ofAdd (↑(↑L v₀) w))) • fourierIntegral e μ L f w
[PROOFSTEP]
dsimp only [fourierIntegral, Function.comp_apply]
[GOAL]
case h
𝕜 : Type u_1
inst✝⁹ : CommRing 𝕜
V : Type u_2
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module 𝕜 V
inst✝⁶ : MeasurableSpace V
W : Type u_3
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module 𝕜 W
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : MeasurableAdd V
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
inst✝ : Measure.IsAddRightInvariant μ
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
v₀ : V
w : W
⊢ ∫ (v : V), ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • f (v + v₀) ∂μ =
    ↑(↑e (↑Multiplicative.ofAdd (↑(↑L v₀) w))) • ∫ (v : V), ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • f v ∂μ
[PROOFSTEP]
conv in L _ => rw [← add_sub_cancel v v₀]
[GOAL]
𝕜 : Type u_1
inst✝⁹ : CommRing 𝕜
V : Type u_2
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module 𝕜 V
inst✝⁶ : MeasurableSpace V
W : Type u_3
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module 𝕜 W
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : MeasurableAdd V
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
inst✝ : Measure.IsAddRightInvariant μ
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
v₀ : V
w : W
v : V
| ↑L v
[PROOFSTEP]
rw [← add_sub_cancel v v₀]
[GOAL]
𝕜 : Type u_1
inst✝⁹ : CommRing 𝕜
V : Type u_2
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module 𝕜 V
inst✝⁶ : MeasurableSpace V
W : Type u_3
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module 𝕜 W
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : MeasurableAdd V
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
inst✝ : Measure.IsAddRightInvariant μ
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
v₀ : V
w : W
v : V
| ↑L v
[PROOFSTEP]
rw [← add_sub_cancel v v₀]
[GOAL]
𝕜 : Type u_1
inst✝⁹ : CommRing 𝕜
V : Type u_2
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module 𝕜 V
inst✝⁶ : MeasurableSpace V
W : Type u_3
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module 𝕜 W
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : MeasurableAdd V
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
inst✝ : Measure.IsAddRightInvariant μ
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
v₀ : V
w : W
v : V
| ↑L v
[PROOFSTEP]
rw [← add_sub_cancel v v₀]
[GOAL]
case h
𝕜 : Type u_1
inst✝⁹ : CommRing 𝕜
V : Type u_2
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module 𝕜 V
inst✝⁶ : MeasurableSpace V
W : Type u_3
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module 𝕜 W
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : MeasurableAdd V
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
inst✝ : Measure.IsAddRightInvariant μ
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
v₀ : V
w : W
⊢ ∫ (v : V), ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L (v + v₀ - v₀)) w))) • f (v + v₀) ∂μ =
    ↑(↑e (↑Multiplicative.ofAdd (↑(↑L v₀) w))) • ∫ (v : V), ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • f v ∂μ
[PROOFSTEP]
rw [integral_add_right_eq_self fun v : V => e[-L (v - v₀) w] • f v]
[GOAL]
case h
𝕜 : Type u_1
inst✝⁹ : CommRing 𝕜
V : Type u_2
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module 𝕜 V
inst✝⁶ : MeasurableSpace V
W : Type u_3
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module 𝕜 W
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : MeasurableAdd V
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
inst✝ : Measure.IsAddRightInvariant μ
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
v₀ : V
w : W
⊢ ∫ (x : V), ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L (x - v₀)) w))) • f x ∂μ =
    ↑(↑e (↑Multiplicative.ofAdd (↑(↑L v₀) w))) • ∫ (v : V), ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • f v ∂μ
[PROOFSTEP]
dsimp only
[GOAL]
case h
𝕜 : Type u_1
inst✝⁹ : CommRing 𝕜
V : Type u_2
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module 𝕜 V
inst✝⁶ : MeasurableSpace V
W : Type u_3
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module 𝕜 W
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : MeasurableAdd V
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
inst✝ : Measure.IsAddRightInvariant μ
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
v₀ : V
w : W
⊢ ∫ (x : V), ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L (x - v₀)) w))) • f x ∂μ =
    ↑(↑e (↑Multiplicative.ofAdd (↑(↑L v₀) w))) • ∫ (v : V), ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • f v ∂μ
[PROOFSTEP]
rw [← integral_smul]
[GOAL]
case h
𝕜 : Type u_1
inst✝⁹ : CommRing 𝕜
V : Type u_2
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module 𝕜 V
inst✝⁶ : MeasurableSpace V
W : Type u_3
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module 𝕜 W
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : MeasurableAdd V
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
inst✝ : Measure.IsAddRightInvariant μ
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
v₀ : V
w : W
⊢ ∫ (x : V), ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L (x - v₀)) w))) • f x ∂μ =
    ∫ (a : V), ↑(↑e (↑Multiplicative.ofAdd (↑(↑L v₀) w))) • ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L a) w))) • f a ∂μ
[PROOFSTEP]
congr 1 with v
[GOAL]
case h.e_f.h
𝕜 : Type u_1
inst✝⁹ : CommRing 𝕜
V : Type u_2
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module 𝕜 V
inst✝⁶ : MeasurableSpace V
W : Type u_3
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module 𝕜 W
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : MeasurableAdd V
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
inst✝ : Measure.IsAddRightInvariant μ
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
v₀ : V
w : W
v : V
⊢ ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L (v - v₀)) w))) • f v =
    ↑(↑e (↑Multiplicative.ofAdd (↑(↑L v₀) w))) • ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • f v
[PROOFSTEP]
rw [← smul_assoc, smul_eq_mul, ← Submonoid.coe_mul, ← e.map_mul, ← ofAdd_add, ← LinearMap.neg_apply, ← sub_eq_add_neg, ←
  LinearMap.sub_apply, LinearMap.map_sub, neg_sub]
[GOAL]
𝕜 : Type u_1
inst✝¹² : CommRing 𝕜
V : Type u_2
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module 𝕜 V
inst✝⁹ : MeasurableSpace V
W : Type u_3
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module 𝕜 W
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : TopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
w : W
⊢ Integrable f ↔ Integrable fun v => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • f v
[PROOFSTEP]
have aux : ∀ {g : V → E} (_ : Integrable g μ) (x : W), Integrable (fun v : V => e[-L v x] • g v) μ :=
  by
  intro g hg x
  have c : Continuous fun v => e[-L v x] :=
    by
    refine' (continuous_induced_rng.mp he).comp (continuous_ofAdd.comp (Continuous.neg _))
    exact hL.comp (continuous_prod_mk.mpr ⟨continuous_id, continuous_const⟩)
  rw [← integrable_norm_iff (c.aestronglyMeasurable.smul hg.1)]
  convert hg.norm using 2
  rw [norm_smul, Complex.norm_eq_abs, abs_coe_circle, one_mul]
    -- then use it for both directions
[GOAL]
𝕜 : Type u_1
inst✝¹² : CommRing 𝕜
V : Type u_2
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module 𝕜 V
inst✝⁹ : MeasurableSpace V
W : Type u_3
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module 𝕜 W
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : TopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
w : W
⊢ ∀ {g : V → E}, Integrable g → ∀ (x : W), Integrable fun v => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) x))) • g v
[PROOFSTEP]
intro g hg x
[GOAL]
𝕜 : Type u_1
inst✝¹² : CommRing 𝕜
V : Type u_2
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module 𝕜 V
inst✝⁹ : MeasurableSpace V
W : Type u_3
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module 𝕜 W
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : TopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
w : W
g : V → E
hg : Integrable g
x : W
⊢ Integrable fun v => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) x))) • g v
[PROOFSTEP]
have c : Continuous fun v => e[-L v x] :=
  by
  refine' (continuous_induced_rng.mp he).comp (continuous_ofAdd.comp (Continuous.neg _))
  exact hL.comp (continuous_prod_mk.mpr ⟨continuous_id, continuous_const⟩)
[GOAL]
𝕜 : Type u_1
inst✝¹² : CommRing 𝕜
V : Type u_2
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module 𝕜 V
inst✝⁹ : MeasurableSpace V
W : Type u_3
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module 𝕜 W
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : TopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
w : W
g : V → E
hg : Integrable g
x : W
⊢ Continuous fun v => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) x)))
[PROOFSTEP]
refine' (continuous_induced_rng.mp he).comp (continuous_ofAdd.comp (Continuous.neg _))
[GOAL]
𝕜 : Type u_1
inst✝¹² : CommRing 𝕜
V : Type u_2
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module 𝕜 V
inst✝⁹ : MeasurableSpace V
W : Type u_3
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module 𝕜 W
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : TopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
w : W
g : V → E
hg : Integrable g
x : W
⊢ Continuous fun v => ↑(↑L v) x
[PROOFSTEP]
exact hL.comp (continuous_prod_mk.mpr ⟨continuous_id, continuous_const⟩)
[GOAL]
𝕜 : Type u_1
inst✝¹² : CommRing 𝕜
V : Type u_2
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module 𝕜 V
inst✝⁹ : MeasurableSpace V
W : Type u_3
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module 𝕜 W
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : TopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
w : W
g : V → E
hg : Integrable g
x : W
c : Continuous fun v => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) x)))
⊢ Integrable fun v => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) x))) • g v
[PROOFSTEP]
rw [← integrable_norm_iff (c.aestronglyMeasurable.smul hg.1)]
[GOAL]
𝕜 : Type u_1
inst✝¹² : CommRing 𝕜
V : Type u_2
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module 𝕜 V
inst✝⁹ : MeasurableSpace V
W : Type u_3
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module 𝕜 W
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : TopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
w : W
g : V → E
hg : Integrable g
x : W
c : Continuous fun v => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) x)))
⊢ Integrable fun a => ‖↑(↑e (↑Multiplicative.ofAdd (-↑(↑L a) x))) • g a‖
[PROOFSTEP]
convert hg.norm using 2
[GOAL]
case h.e'_5.h
𝕜 : Type u_1
inst✝¹² : CommRing 𝕜
V : Type u_2
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module 𝕜 V
inst✝⁹ : MeasurableSpace V
W : Type u_3
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module 𝕜 W
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : TopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
w : W
g : V → E
hg : Integrable g
x : W
c : Continuous fun v => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) x)))
x✝ : V
⊢ ‖↑(↑e (↑Multiplicative.ofAdd (-↑(↑L x✝) x))) • g x✝‖ = ‖g x✝‖
[PROOFSTEP]
rw [norm_smul, Complex.norm_eq_abs, abs_coe_circle, one_mul]
  -- then use it for both directions
[GOAL]
𝕜 : Type u_1
inst✝¹² : CommRing 𝕜
V : Type u_2
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module 𝕜 V
inst✝⁹ : MeasurableSpace V
W : Type u_3
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module 𝕜 W
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : TopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
w : W
aux : ∀ {g : V → E}, Integrable g → ∀ (x : W), Integrable fun v => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) x))) • g v
⊢ Integrable f ↔ Integrable fun v => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • f v
[PROOFSTEP]
refine' ⟨fun hf => aux hf w, fun hf => _⟩
[GOAL]
𝕜 : Type u_1
inst✝¹² : CommRing 𝕜
V : Type u_2
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module 𝕜 V
inst✝⁹ : MeasurableSpace V
W : Type u_3
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module 𝕜 W
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : TopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
w : W
aux : ∀ {g : V → E}, Integrable g → ∀ (x : W), Integrable fun v => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) x))) • g v
hf : Integrable fun v => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • f v
⊢ Integrable f
[PROOFSTEP]
convert aux hf (-w)
[GOAL]
case h.e'_5.h
𝕜 : Type u_1
inst✝¹² : CommRing 𝕜
V : Type u_2
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module 𝕜 V
inst✝⁹ : MeasurableSpace V
W : Type u_3
inst✝⁸ : AddCommGroup W
inst✝⁷ : Module 𝕜 W
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : TopologicalRing 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : BorelSpace V
inst✝ : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
w : W
aux : ∀ {g : V → E}, Integrable g → ∀ (x : W), Integrable fun v => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) x))) • g v
hf : Integrable fun v => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • f v
x✝ : V
⊢ f x✝ = ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L x✝) (-w)))) • ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L x✝) w))) • f x✝
[PROOFSTEP]
rw [← smul_assoc, smul_eq_mul, ← Submonoid.coe_mul, ← MonoidHom.map_mul, ← ofAdd_add, LinearMap.map_neg, neg_neg, ←
  sub_eq_add_neg, sub_self, ofAdd_zero, MonoidHom.map_one, Submonoid.coe_one, one_smul]
[GOAL]
𝕜 : Type u_1
inst✝¹³ : CommRing 𝕜
V : Type u_2
inst✝¹² : AddCommGroup V
inst✝¹¹ : Module 𝕜 V
inst✝¹⁰ : MeasurableSpace V
W : Type u_3
inst✝⁹ : AddCommGroup W
inst✝⁸ : Module 𝕜 W
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : TopologicalRing 𝕜
inst✝³ : TopologicalSpace V
inst✝² : BorelSpace V
inst✝¹ : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst✝ : CompleteSpace E
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f g : V → E
hf : Integrable f
hg : Integrable g
⊢ fourierIntegral e μ L f + fourierIntegral e μ L g = fourierIntegral e μ L (f + g)
[PROOFSTEP]
ext1 w
[GOAL]
case h
𝕜 : Type u_1
inst✝¹³ : CommRing 𝕜
V : Type u_2
inst✝¹² : AddCommGroup V
inst✝¹¹ : Module 𝕜 V
inst✝¹⁰ : MeasurableSpace V
W : Type u_3
inst✝⁹ : AddCommGroup W
inst✝⁸ : Module 𝕜 W
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : TopologicalRing 𝕜
inst✝³ : TopologicalSpace V
inst✝² : BorelSpace V
inst✝¹ : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst✝ : CompleteSpace E
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f g : V → E
hf : Integrable f
hg : Integrable g
w : W
⊢ (fourierIntegral e μ L f + fourierIntegral e μ L g) w = fourierIntegral e μ L (f + g) w
[PROOFSTEP]
dsimp only [Pi.add_apply, fourierIntegral]
[GOAL]
case h
𝕜 : Type u_1
inst✝¹³ : CommRing 𝕜
V : Type u_2
inst✝¹² : AddCommGroup V
inst✝¹¹ : Module 𝕜 V
inst✝¹⁰ : MeasurableSpace V
W : Type u_3
inst✝⁹ : AddCommGroup W
inst✝⁸ : Module 𝕜 W
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : TopologicalRing 𝕜
inst✝³ : TopologicalSpace V
inst✝² : BorelSpace V
inst✝¹ : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst✝ : CompleteSpace E
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f g : V → E
hf : Integrable f
hg : Integrable g
w : W
⊢ ∫ (v : V), ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • f v ∂μ +
      ∫ (v : V), ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • g v ∂μ =
    ∫ (v : V), ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • (f v + g v) ∂μ
[PROOFSTEP]
simp_rw [smul_add]
[GOAL]
case h
𝕜 : Type u_1
inst✝¹³ : CommRing 𝕜
V : Type u_2
inst✝¹² : AddCommGroup V
inst✝¹¹ : Module 𝕜 V
inst✝¹⁰ : MeasurableSpace V
W : Type u_3
inst✝⁹ : AddCommGroup W
inst✝⁸ : Module 𝕜 W
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : TopologicalRing 𝕜
inst✝³ : TopologicalSpace V
inst✝² : BorelSpace V
inst✝¹ : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst✝ : CompleteSpace E
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f g : V → E
hf : Integrable f
hg : Integrable g
w : W
⊢ ∫ (v : V), ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • f v ∂μ +
      ∫ (v : V), ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • g v ∂μ =
    ∫ (v : V), ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • f v + ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • g v ∂μ
[PROOFSTEP]
rw [integral_add]
[GOAL]
case h.hf
𝕜 : Type u_1
inst✝¹³ : CommRing 𝕜
V : Type u_2
inst✝¹² : AddCommGroup V
inst✝¹¹ : Module 𝕜 V
inst✝¹⁰ : MeasurableSpace V
W : Type u_3
inst✝⁹ : AddCommGroup W
inst✝⁸ : Module 𝕜 W
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : TopologicalRing 𝕜
inst✝³ : TopologicalSpace V
inst✝² : BorelSpace V
inst✝¹ : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst✝ : CompleteSpace E
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f g : V → E
hf : Integrable f
hg : Integrable g
w : W
⊢ Integrable fun v => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • f v
[PROOFSTEP]
exact (fourier_integral_convergent_iff he hL w).mp hf
[GOAL]
case h.hg
𝕜 : Type u_1
inst✝¹³ : CommRing 𝕜
V : Type u_2
inst✝¹² : AddCommGroup V
inst✝¹¹ : Module 𝕜 V
inst✝¹⁰ : MeasurableSpace V
W : Type u_3
inst✝⁹ : AddCommGroup W
inst✝⁸ : Module 𝕜 W
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℂ E
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : TopologicalRing 𝕜
inst✝³ : TopologicalSpace V
inst✝² : BorelSpace V
inst✝¹ : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst✝ : CompleteSpace E
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f g : V → E
hf : Integrable f
hg : Integrable g
w : W
⊢ Integrable fun v => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • g v
[PROOFSTEP]
exact (fourier_integral_convergent_iff he hL w).mp hg
[GOAL]
𝕜 : Type u_1
inst✝¹⁴ : CommRing 𝕜
V : Type u_2
inst✝¹³ : AddCommGroup V
inst✝¹² : Module 𝕜 V
inst✝¹¹ : MeasurableSpace V
W : Type u_3
inst✝¹⁰ : AddCommGroup W
inst✝⁹ : Module 𝕜 W
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : TopologicalRing 𝕜
inst✝⁴ : TopologicalSpace V
inst✝³ : BorelSpace V
inst✝² : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst✝¹ : CompleteSpace E
inst✝ : TopologicalSpace.FirstCountableTopology W
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
hf : Integrable f
⊢ Continuous (fourierIntegral e μ L f)
[PROOFSTEP]
apply continuous_of_dominated
[GOAL]
case hF_meas
𝕜 : Type u_1
inst✝¹⁴ : CommRing 𝕜
V : Type u_2
inst✝¹³ : AddCommGroup V
inst✝¹² : Module 𝕜 V
inst✝¹¹ : MeasurableSpace V
W : Type u_3
inst✝¹⁰ : AddCommGroup W
inst✝⁹ : Module 𝕜 W
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : TopologicalRing 𝕜
inst✝⁴ : TopologicalSpace V
inst✝³ : BorelSpace V
inst✝² : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst✝¹ : CompleteSpace E
inst✝ : TopologicalSpace.FirstCountableTopology W
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
hf : Integrable f
⊢ ∀ (x : W), AEStronglyMeasurable (fun a => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L a) x))) • f a) μ
[PROOFSTEP]
exact fun w => ((fourier_integral_convergent_iff he hL w).mp hf).1
[GOAL]
case h_bound
𝕜 : Type u_1
inst✝¹⁴ : CommRing 𝕜
V : Type u_2
inst✝¹³ : AddCommGroup V
inst✝¹² : Module 𝕜 V
inst✝¹¹ : MeasurableSpace V
W : Type u_3
inst✝¹⁰ : AddCommGroup W
inst✝⁹ : Module 𝕜 W
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : TopologicalRing 𝕜
inst✝⁴ : TopologicalSpace V
inst✝³ : BorelSpace V
inst✝² : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst✝¹ : CompleteSpace E
inst✝ : TopologicalSpace.FirstCountableTopology W
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
hf : Integrable f
⊢ ∀ (x : W), ∀ᵐ (a : V) ∂μ, ‖↑(↑e (↑Multiplicative.ofAdd (-↑(↑L a) x))) • f a‖ ≤ ?bound a
[PROOFSTEP]
refine' fun w => ae_of_all _ fun v => _
[GOAL]
case bound
𝕜 : Type u_1
inst✝¹⁴ : CommRing 𝕜
V : Type u_2
inst✝¹³ : AddCommGroup V
inst✝¹² : Module 𝕜 V
inst✝¹¹ : MeasurableSpace V
W : Type u_3
inst✝¹⁰ : AddCommGroup W
inst✝⁹ : Module 𝕜 W
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : TopologicalRing 𝕜
inst✝⁴ : TopologicalSpace V
inst✝³ : BorelSpace V
inst✝² : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst✝¹ : CompleteSpace E
inst✝ : TopologicalSpace.FirstCountableTopology W
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
hf : Integrable f
⊢ V → ℝ
[PROOFSTEP]
exact fun v => ‖f v‖
[GOAL]
case h_bound
𝕜 : Type u_1
inst✝¹⁴ : CommRing 𝕜
V : Type u_2
inst✝¹³ : AddCommGroup V
inst✝¹² : Module 𝕜 V
inst✝¹¹ : MeasurableSpace V
W : Type u_3
inst✝¹⁰ : AddCommGroup W
inst✝⁹ : Module 𝕜 W
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : TopologicalRing 𝕜
inst✝⁴ : TopologicalSpace V
inst✝³ : BorelSpace V
inst✝² : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst✝¹ : CompleteSpace E
inst✝ : TopologicalSpace.FirstCountableTopology W
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
hf : Integrable f
w : W
v : V
⊢ ‖↑(↑e (↑Multiplicative.ofAdd (-↑(↑L v) w))) • f v‖ ≤ ‖f v‖
[PROOFSTEP]
rw [norm_smul, Complex.norm_eq_abs, abs_coe_circle, one_mul]
[GOAL]
case bound_integrable
𝕜 : Type u_1
inst✝¹⁴ : CommRing 𝕜
V : Type u_2
inst✝¹³ : AddCommGroup V
inst✝¹² : Module 𝕜 V
inst✝¹¹ : MeasurableSpace V
W : Type u_3
inst✝¹⁰ : AddCommGroup W
inst✝⁹ : Module 𝕜 W
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : TopologicalRing 𝕜
inst✝⁴ : TopologicalSpace V
inst✝³ : BorelSpace V
inst✝² : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst✝¹ : CompleteSpace E
inst✝ : TopologicalSpace.FirstCountableTopology W
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
hf : Integrable f
⊢ Integrable fun v => ‖f v‖
[PROOFSTEP]
exact hf.norm
[GOAL]
case h_cont
𝕜 : Type u_1
inst✝¹⁴ : CommRing 𝕜
V : Type u_2
inst✝¹³ : AddCommGroup V
inst✝¹² : Module 𝕜 V
inst✝¹¹ : MeasurableSpace V
W : Type u_3
inst✝¹⁰ : AddCommGroup W
inst✝⁹ : Module 𝕜 W
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : TopologicalRing 𝕜
inst✝⁴ : TopologicalSpace V
inst✝³ : BorelSpace V
inst✝² : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst✝¹ : CompleteSpace E
inst✝ : TopologicalSpace.FirstCountableTopology W
he : Continuous ↑e
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
hf : Integrable f
⊢ ∀ᵐ (a : V) ∂μ, Continuous fun x => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L a) x))) • f a
[PROOFSTEP]
rw [continuous_induced_rng] at he
[GOAL]
case h_cont
𝕜 : Type u_1
inst✝¹⁴ : CommRing 𝕜
V : Type u_2
inst✝¹³ : AddCommGroup V
inst✝¹² : Module 𝕜 V
inst✝¹¹ : MeasurableSpace V
W : Type u_3
inst✝¹⁰ : AddCommGroup W
inst✝⁹ : Module 𝕜 W
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : TopologicalRing 𝕜
inst✝⁴ : TopologicalSpace V
inst✝³ : BorelSpace V
inst✝² : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst✝¹ : CompleteSpace E
inst✝ : TopologicalSpace.FirstCountableTopology W
he : Continuous (Subtype.val ∘ ↑e)
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
hf : Integrable f
⊢ ∀ᵐ (a : V) ∂μ, Continuous fun x => ↑(↑e (↑Multiplicative.ofAdd (-↑(↑L a) x))) • f a
[PROOFSTEP]
refine' ae_of_all _ fun v => (he.comp (continuous_ofAdd.comp _)).smul continuous_const
[GOAL]
case h_cont
𝕜 : Type u_1
inst✝¹⁴ : CommRing 𝕜
V : Type u_2
inst✝¹³ : AddCommGroup V
inst✝¹² : Module 𝕜 V
inst✝¹¹ : MeasurableSpace V
W : Type u_3
inst✝¹⁰ : AddCommGroup W
inst✝⁹ : Module 𝕜 W
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℂ E
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : TopologicalRing 𝕜
inst✝⁴ : TopologicalSpace V
inst✝³ : BorelSpace V
inst✝² : TopologicalSpace W
e : Multiplicative 𝕜 →* { x // x ∈ 𝕊 }
μ : Measure V
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
inst✝¹ : CompleteSpace E
inst✝ : TopologicalSpace.FirstCountableTopology W
he : Continuous (Subtype.val ∘ ↑e)
hL : Continuous fun p => ↑(↑L p.fst) p.snd
f : V → E
hf : Integrable f
v : V
⊢ Continuous fun x => -↑(↑L v) x
[PROOFSTEP]
refine' (hL.comp (continuous_prod_mk.mpr ⟨continuous_const, continuous_id⟩)).neg
[GOAL]
⊢ (fun z => ↑expMapCircle (2 * π * ↑Multiplicative.toAdd z)) 1 = 1
[PROOFSTEP]
simp only
[GOAL]
⊢ ↑expMapCircle (2 * π * ↑Multiplicative.toAdd 1) = 1
[PROOFSTEP]
rw [toAdd_one, mul_zero, expMapCircle_zero]
[GOAL]
x y : Multiplicative ℝ
⊢ OneHom.toFun
      { toFun := fun z => ↑expMapCircle (2 * π * ↑Multiplicative.toAdd z),
        map_one' := (_ : (fun z => ↑expMapCircle (2 * π * ↑Multiplicative.toAdd z)) 1 = 1) }
      (x * y) =
    OneHom.toFun
        { toFun := fun z => ↑expMapCircle (2 * π * ↑Multiplicative.toAdd z),
          map_one' := (_ : (fun z => ↑expMapCircle (2 * π * ↑Multiplicative.toAdd z)) 1 = 1) }
        x *
      OneHom.toFun
        { toFun := fun z => ↑expMapCircle (2 * π * ↑Multiplicative.toAdd z),
          map_one' := (_ : (fun z => ↑expMapCircle (2 * π * ↑Multiplicative.toAdd z)) 1 = 1) }
        y
[PROOFSTEP]
simp only
[GOAL]
x y : Multiplicative ℝ
⊢ ↑expMapCircle (2 * π * ↑Multiplicative.toAdd (x * y)) =
    ↑expMapCircle (2 * π * ↑Multiplicative.toAdd x) * ↑expMapCircle (2 * π * ↑Multiplicative.toAdd y)
[PROOFSTEP]
rw [toAdd_mul, mul_add, expMapCircle_add]
[GOAL]
x : ℝ
⊢ ↑(↑fourierChar (↑Multiplicative.ofAdd x)) = Complex.exp (↑(2 * π * x) * Complex.I)
[PROOFSTEP]
rfl
[GOAL]
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
inst✝² : MeasurableSpace V
W : Type u_3
inst✝¹ : AddCommGroup W
inst✝ : Module ℝ W
L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ
μ : Measure V
f : V → E
w : W
⊢ VectorFourier.fourierIntegral fourierChar μ L f w =
    ∫ (v : V), Complex.exp (↑(-2 * π * ↑(↑L v) w) * Complex.I) • f v ∂μ
[PROOFSTEP]
simp_rw [VectorFourier.fourierIntegral, Real.fourierChar_apply, mul_neg, neg_mul]
[GOAL]
E✝ : Type u_1
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedSpace ℂ E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
w : ℝ
⊢ 𝓕 f w = ∫ (v : ℝ), Complex.exp (↑(-2 * π * v * w) * Complex.I) • f v
[PROOFSTEP]
simp_rw [fourierIntegral_def, Real.fourierChar_apply, mul_neg, neg_mul, mul_assoc]


[GOAL]
ι : Type u_1
I J J₁ J₂ : Box ι
π : TaggedPrepartition I
x : ι → ℝ
⊢ x ∈ iUnion π ↔ ∃ J, J ∈ π ∧ x ∈ J
[PROOFSTEP]
convert Set.mem_iUnion₂
[GOAL]
case h.e'_2.h.e'_2.h.a
ι : Type u_1
I J J₁ J₂ : Box ι
π : TaggedPrepartition I
x : ι → ℝ
x✝ : Box ι
⊢ x✝ ∈ π ∧ x ∈ x✝ ↔ ∃ j, x ∈ ↑x✝
[PROOFSTEP]
rw [Box.mem_coe, mem_toPrepartition, exists_prop]
[GOAL]
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
hJ : J ∈ π
J' : Box ι
hJ' : J' ∈ πi J
⊢ TaggedPrepartition.tag (biUnionTagged π πi) J' = TaggedPrepartition.tag (πi J) J'
[PROOFSTEP]
rw [← π.biUnionIndex_of_mem (πi := fun J => (πi J).toPrepartition) hJ hJ']
[GOAL]
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
hJ : J ∈ π
J' : Box ι
hJ' : J' ∈ πi J
⊢ TaggedPrepartition.tag (biUnionTagged π πi) J' =
    TaggedPrepartition.tag (πi (biUnionIndex π (fun J => (πi J).toPrepartition) J')) J'
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
I J : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
⊢ (∀ (J : Box ι), J ∈ biUnionTagged π πi → p (TaggedPrepartition.tag (biUnionTagged π πi) J) J) ↔
    ∀ (J : Box ι), J ∈ π → ∀ (J' : Box ι), J' ∈ πi J → p (TaggedPrepartition.tag (πi J) J') J'
[PROOFSTEP]
simp only [mem_biUnionTagged]
[GOAL]
ι : Type u_1
I J : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
⊢ (∀ (J : Box ι), (∃ J', J' ∈ π ∧ J ∈ πi J') → p (TaggedPrepartition.tag (biUnionTagged π πi) J) J) ↔
    ∀ (J : Box ι), J ∈ π → ∀ (J' : Box ι), J' ∈ πi J → p (TaggedPrepartition.tag (πi J) J') J'
[PROOFSTEP]
refine' ⟨fun H J hJ J' hJ' => _, fun H J' ⟨J, hJ, hJ'⟩ => _⟩
[GOAL]
case refine'_1
ι : Type u_1
I J✝ : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
H : ∀ (J : Box ι), (∃ J', J' ∈ π ∧ J ∈ πi J') → p (TaggedPrepartition.tag (biUnionTagged π πi) J) J
J : Box ι
hJ : J ∈ π
J' : Box ι
hJ' : J' ∈ πi J
⊢ p (TaggedPrepartition.tag (πi J) J') J'
[PROOFSTEP]
rw [← π.tag_biUnionTagged hJ hJ']
[GOAL]
case refine'_1
ι : Type u_1
I J✝ : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
H : ∀ (J : Box ι), (∃ J', J' ∈ π ∧ J ∈ πi J') → p (TaggedPrepartition.tag (biUnionTagged π πi) J) J
J : Box ι
hJ : J ∈ π
J' : Box ι
hJ' : J' ∈ πi J
⊢ p (TaggedPrepartition.tag (biUnionTagged π πi) J') J'
[PROOFSTEP]
exact H J' ⟨J, hJ, hJ'⟩
[GOAL]
case refine'_2
ι : Type u_1
I J✝ : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
H : ∀ (J : Box ι), J ∈ π → ∀ (J' : Box ι), J' ∈ πi J → p (TaggedPrepartition.tag (πi J) J') J'
J' : Box ι
x✝ : ∃ J'_1, J'_1 ∈ π ∧ J' ∈ πi J'_1
J : Box ι
hJ : J ∈ π
hJ' : J' ∈ πi J
⊢ p (TaggedPrepartition.tag (biUnionTagged π πi) J') J'
[PROOFSTEP]
rw [π.tag_biUnionTagged hJ hJ']
[GOAL]
case refine'_2
ι : Type u_1
I J✝ : Box ι
p : (ι → ℝ) → Box ι → Prop
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
H : ∀ (J : Box ι), J ∈ π → ∀ (J' : Box ι), J' ∈ πi J → p (TaggedPrepartition.tag (πi J) J') J'
J' : Box ι
x✝ : ∃ J'_1, J'_1 ∈ π ∧ J' ∈ πi J'_1
J : Box ι
hJ : J ∈ π
hJ' : J' ∈ πi J
⊢ p (TaggedPrepartition.tag (πi J) J') J'
[PROOFSTEP]
exact H J hJ J' hJ'
[GOAL]
ι : Type u_1
I J : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
⊢ J ∈ infPrepartition π₁ π₂.toPrepartition ↔ J ∈ infPrepartition π₂ π₁.toPrepartition
[PROOFSTEP]
simp only [← mem_toPrepartition, infPrepartition_toPrepartition, inf_comm]
[GOAL]
ι : Type u_1
I J : Box ι
π π₁ π₂ : TaggedPrepartition I
x✝ : ι → ℝ
inst✝ : Fintype ι
h : IsHenstock π
x : ι → ℝ
⊢ Finset.card (Finset.filter (fun J => tag π J = x) π.boxes) ≤
    Finset.card (Finset.filter (fun J => x ∈ ↑Box.Icc J) π.boxes)
[PROOFSTEP]
refine' Finset.card_le_of_subset fun J hJ => _
[GOAL]
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x✝ : ι → ℝ
inst✝ : Fintype ι
h : IsHenstock π
x : ι → ℝ
J : Box ι
hJ : J ∈ Finset.filter (fun J => tag π J = x) π.boxes
⊢ J ∈ Finset.filter (fun J => x ∈ ↑Box.Icc J) π.boxes
[PROOFSTEP]
rw [Finset.mem_filter] at hJ ⊢
[GOAL]
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x✝ : ι → ℝ
inst✝ : Fintype ι
h : IsHenstock π
x : ι → ℝ
J : Box ι
hJ : J ∈ π.boxes ∧ tag π J = x
⊢ J ∈ π.boxes ∧ x ∈ ↑Box.Icc J
[PROOFSTEP]
rcases hJ with ⟨hJ, rfl⟩
[GOAL]
case intro
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
inst✝ : Fintype ι
h : IsHenstock π
J : Box ι
hJ : J ∈ π.boxes
⊢ J ∈ π.boxes ∧ tag π J ∈ ↑Box.Icc J
[PROOFSTEP]
exact ⟨hJ, h J hJ⟩
[GOAL]
ι : Type u_1
I J : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
p : (ι → ℝ) → Box ι → Prop
hJ : J ≤ I
h : x ∈ ↑Box.Icc I
⊢ (∀ (J' : Box ι), J' ∈ single I J hJ x h → p (tag (single I J hJ x h) J') J') ↔ p x J
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
I J✝ : Box ι
π π₁✝ π₂✝ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
π₁ π₂ : TaggedPrepartition I
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
⊢ Finset.piecewise π₁.boxes π₁.tag π₂.tag J ∈ ↑Box.Icc I
[PROOFSTEP]
dsimp only [Finset.piecewise]
[GOAL]
ι : Type u_1
I J✝ : Box ι
π π₁✝ π₂✝ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
π₁ π₂ : TaggedPrepartition I
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
⊢ (if J ∈ π₁.boxes then tag π₁ J else tag π₂ J) ∈ ↑Box.Icc I
[PROOFSTEP]
split_ifs
[GOAL]
case pos
ι : Type u_1
I J✝ : Box ι
π π₁✝ π₂✝ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
π₁ π₂ : TaggedPrepartition I
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
h✝ : J ∈ π₁.boxes
⊢ tag π₁ J ∈ ↑Box.Icc I
case neg
ι : Type u_1
I J✝ : Box ι
π π₁✝ π₂✝ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
π₁ π₂ : TaggedPrepartition I
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
h✝ : ¬J ∈ π₁.boxes
⊢ tag π₂ J ∈ ↑Box.Icc I
[PROOFSTEP]
exacts [π₁.tag_mem_Icc J, π₂.tag_mem_Icc J]
[GOAL]
ι : Type u_1
I J : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
inst✝ : Fintype ι
h₁ : IsSubordinate π₁ r
h₂ : IsSubordinate π₂ r
h : Disjoint (iUnion π₁) (iUnion π₂)
⊢ IsSubordinate (TaggedPrepartition.disjUnion π₁ π₂ h) r
[PROOFSTEP]
refine' fun J hJ => (Finset.mem_union.1 hJ).elim (fun hJ => _) fun hJ => _
[GOAL]
case refine'_1
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
inst✝ : Fintype ι
h₁ : IsSubordinate π₁ r
h₂ : IsSubordinate π₂ r
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
hJ✝ : J ∈ TaggedPrepartition.disjUnion π₁ π₂ h
hJ : J ∈ π₁.boxes
⊢ ↑Box.Icc J ⊆
    closedBall (tag (TaggedPrepartition.disjUnion π₁ π₂ h) J) ↑(r (tag (TaggedPrepartition.disjUnion π₁ π₂ h) J))
[PROOFSTEP]
rw [disjUnion_tag_of_mem_left _ hJ]
[GOAL]
case refine'_1
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
inst✝ : Fintype ι
h₁ : IsSubordinate π₁ r
h₂ : IsSubordinate π₂ r
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
hJ✝ : J ∈ TaggedPrepartition.disjUnion π₁ π₂ h
hJ : J ∈ π₁.boxes
⊢ ↑Box.Icc J ⊆ closedBall (tag π₁ J) ↑(r (tag π₁ J))
[PROOFSTEP]
exact h₁ _ hJ
[GOAL]
case refine'_2
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
inst✝ : Fintype ι
h₁ : IsSubordinate π₁ r
h₂ : IsSubordinate π₂ r
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
hJ✝ : J ∈ TaggedPrepartition.disjUnion π₁ π₂ h
hJ : J ∈ π₂.boxes
⊢ ↑Box.Icc J ⊆
    closedBall (tag (TaggedPrepartition.disjUnion π₁ π₂ h) J) ↑(r (tag (TaggedPrepartition.disjUnion π₁ π₂ h) J))
[PROOFSTEP]
rw [disjUnion_tag_of_mem_right _ hJ]
[GOAL]
case refine'_2
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
inst✝ : Fintype ι
h₁ : IsSubordinate π₁ r
h₂ : IsSubordinate π₂ r
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
hJ✝ : J ∈ TaggedPrepartition.disjUnion π₁ π₂ h
hJ : J ∈ π₂.boxes
⊢ ↑Box.Icc J ⊆ closedBall (tag π₂ J) ↑(r (tag π₂ J))
[PROOFSTEP]
exact h₂ _ hJ
[GOAL]
ι : Type u_1
I J : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
h₁ : IsHenstock π₁
h₂ : IsHenstock π₂
h : Disjoint (iUnion π₁) (iUnion π₂)
⊢ IsHenstock (TaggedPrepartition.disjUnion π₁ π₂ h)
[PROOFSTEP]
refine' fun J hJ => (Finset.mem_union.1 hJ).elim (fun hJ => _) fun hJ => _
[GOAL]
case refine'_1
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
h₁ : IsHenstock π₁
h₂ : IsHenstock π₂
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
hJ✝ : J ∈ TaggedPrepartition.disjUnion π₁ π₂ h
hJ : J ∈ π₁.boxes
⊢ tag (TaggedPrepartition.disjUnion π₁ π₂ h) J ∈ ↑Box.Icc J
[PROOFSTEP]
rw [disjUnion_tag_of_mem_left _ hJ]
[GOAL]
case refine'_1
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
h₁ : IsHenstock π₁
h₂ : IsHenstock π₂
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
hJ✝ : J ∈ TaggedPrepartition.disjUnion π₁ π₂ h
hJ : J ∈ π₁.boxes
⊢ tag π₁ J ∈ ↑Box.Icc J
[PROOFSTEP]
exact h₁ _ hJ
[GOAL]
case refine'_2
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
h₁ : IsHenstock π₁
h₂ : IsHenstock π₂
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
hJ✝ : J ∈ TaggedPrepartition.disjUnion π₁ π₂ h
hJ : J ∈ π₂.boxes
⊢ tag (TaggedPrepartition.disjUnion π₁ π₂ h) J ∈ ↑Box.Icc J
[PROOFSTEP]
rw [disjUnion_tag_of_mem_right _ hJ]
[GOAL]
case refine'_2
ι : Type u_1
I J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
h₁ : IsHenstock π₁
h₂ : IsHenstock π₂
h : Disjoint (iUnion π₁) (iUnion π₂)
J : Box ι
hJ✝ : J ∈ TaggedPrepartition.disjUnion π₁ π₂ h
hJ : J ∈ π₂.boxes
⊢ tag π₂ J ∈ ↑Box.Icc J
[PROOFSTEP]
exact h₂ _ hJ
[GOAL]
ι : Type u_1
I✝ J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I✝
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
I J : Box ι
h : I ≤ J
⊢ Injective fun π =>
    {
      toPrepartition :=
        { boxes := π.boxes, le_of_mem' := (_ : ∀ (J' : Box ι), J' ∈ π.boxes → J' ≤ J),
          pairwiseDisjoint := (_ : Set.Pairwise (↑π.boxes) (Disjoint on Box.toSet)) },
      tag := π.tag, tag_mem_Icc := (_ : ∀ (J_1 : Box ι), tag π J_1 ∈ ↑Box.Icc J) }
[PROOFSTEP]
rintro ⟨⟨b₁, h₁le, h₁d⟩, t₁, ht₁⟩ ⟨⟨b₂, h₂le, h₂d⟩, t₂, ht₂⟩ H
[GOAL]
case mk.mk.mk.mk
ι : Type u_1
I✝ J✝ : Box ι
π π₁ π₂ : TaggedPrepartition I✝
x : ι → ℝ
r r₁ r₂ : (ι → ℝ) → ↑(Ioi 0)
I J : Box ι
h : I ≤ J
t₁ : Box ι → ι → ℝ
ht₁ : ∀ (J : Box ι), t₁ J ∈ ↑Box.Icc I
b₁ : Finset (Box ι)
h₁le : ∀ (J : Box ι), J ∈ b₁ → J ≤ I
h₁d : Set.Pairwise (↑b₁) (Disjoint on Box.toSet)
t₂ : Box ι → ι → ℝ
ht₂ : ∀ (J : Box ι), t₂ J ∈ ↑Box.Icc I
b₂ : Finset (Box ι)
h₂le : ∀ (J : Box ι), J ∈ b₂ → J ≤ I
h₂d : Set.Pairwise (↑b₂) (Disjoint on Box.toSet)
H :
  (fun π =>
        {
          toPrepartition :=
            { boxes := π.boxes, le_of_mem' := (_ : ∀ (J' : Box ι), J' ∈ π.boxes → J' ≤ J),
              pairwiseDisjoint := (_ : Set.Pairwise (↑π.boxes) (Disjoint on Box.toSet)) },
          tag := π.tag, tag_mem_Icc := (_ : ∀ (J_1 : Box ι), tag π J_1 ∈ ↑Box.Icc J) })
      { toPrepartition := { boxes := b₁, le_of_mem' := h₁le, pairwiseDisjoint := h₁d }, tag := t₁,
        tag_mem_Icc := ht₁ } =
    (fun π =>
        {
          toPrepartition :=
            { boxes := π.boxes, le_of_mem' := (_ : ∀ (J' : Box ι), J' ∈ π.boxes → J' ≤ J),
              pairwiseDisjoint := (_ : Set.Pairwise (↑π.boxes) (Disjoint on Box.toSet)) },
          tag := π.tag, tag_mem_Icc := (_ : ∀ (J_1 : Box ι), tag π J_1 ∈ ↑Box.Icc J) })
      { toPrepartition := { boxes := b₂, le_of_mem' := h₂le, pairwiseDisjoint := h₂d }, tag := t₂, tag_mem_Icc := ht₂ }
⊢ { toPrepartition := { boxes := b₁, le_of_mem' := h₁le, pairwiseDisjoint := h₁d }, tag := t₁, tag_mem_Icc := ht₁ } =
    { toPrepartition := { boxes := b₂, le_of_mem' := h₂le, pairwiseDisjoint := h₂d }, tag := t₂, tag_mem_Icc := ht₂ }
[PROOFSTEP]
simpa using H