case h
α : Type u_1
E : Type ?u.8082404
F : Type u_2
G : Type ?u.8082410
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
x : F
⊢ ↑↑(indicatorConstLp 2 hs hμs x) =ᵐ[μ]
    ↑↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp 2 hs hμs 1))
α : Type u_1
E : Type ?u.8082404
F : Type u_2
G : Type ?u.8082410
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
x : F
⊢ indicatorConstLp 2 hs hμs x =
    ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp 2 hs hμs 1)
ext1
case h
α : Type u_1
E : Type ?u.8082404
F : Type u_2
G : Type ?u.8082410
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
x : F
⊢ (Set.indicator s fun x_1 => x) =ᵐ[μ]
    ↑↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp 2 hs hμs 1))
case h
α : Type u_1
E : Type ?u.8082404
F : Type u_2
G : Type ?u.8082410
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
x : F
⊢ ↑↑(indicatorConstLp 2 hs hμs x) =ᵐ[μ]
    ↑↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp 2 hs hμs 1))
refine' indicatorConstLp_coeFn.trans _
case h
α : Type u_1
E : Type ?u.8082404
F : Type u_2
G : Type ?u.8082410
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
x : F
h_compLp :
  ∀ᵐ (a : α) ∂μ,
    ↑↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp 2 hs hμs 1)) a =
      ↑(ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
⊢ (Set.indicator s fun x_1 => x) =ᵐ[μ]
    ↑↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp 2 hs hμs 1))
case h
α : Type u_1
E : Type ?u.8082404
F : Type u_2
G : Type ?u.8082410
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
x : F
⊢ (Set.indicator s fun x_1 => x) =ᵐ[μ]
    ↑↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp 2 hs hμs 1))
have h_compLp :=
  (ContinuousLinearMap.toSpanSingleton ℝ x).coeFn_compLp (indicatorConstLp 2 hs hμs (1 : ℝ))
case h
α : Type u_1
E : Type ?u.8082404
F : Type u_2
G : Type ?u.8082410
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
x : F
h_compLp :
  (fun a =>
      ↑↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp 2 hs hμs 1)) a) =ᵐ[μ]
    fun a => ↑(ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
⊢ (Set.indicator s fun x_1 => x) =ᵐ[μ]
    ↑↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp 2 hs hμs 1))
case h
α : Type u_1
E : Type ?u.8082404
F : Type u_2
G : Type ?u.8082410
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
x : F
h_compLp :
  ∀ᵐ (a : α) ∂μ,
    ↑↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp 2 hs hμs 1)) a =
      ↑(ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
⊢ (Set.indicator s fun x_1 => x) =ᵐ[μ]
    ↑↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp 2 hs hμs 1))
rw [← EventuallyEq] at h_compLp
case h
α : Type u_1
E : Type ?u.8082404
F : Type u_2
G : Type ?u.8082410
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
x : F
h_compLp :
  (fun a =>
      ↑↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp 2 hs hμs 1)) a) =ᵐ[μ]
    fun a => ↑(ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
⊢ (Set.indicator s fun x_1 => x) =ᵐ[μ] fun a =>
    ↑(ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
case h
α : Type u_1
E : Type ?u.8082404
F : Type u_2
G : Type ?u.8082410
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
x : F
h_compLp :
  (fun a =>
      ↑↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp 2 hs hμs 1)) a) =ᵐ[μ]
    fun a => ↑(ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
⊢ (Set.indicator s fun x_1 => x) =ᵐ[μ]
    ↑↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp 2 hs hμs 1))
refine' EventuallyEq.trans _ h_compLp.symm
case h
α : Type u_1
E : Type ?u.8082404
F : Type u_2
G : Type ?u.8082410
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
x : F
h_compLp :
  (fun a =>
      ↑↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp 2 hs hμs 1)) a) =ᵐ[μ]
    fun a => ↑(ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
y : α
hy : ↑↑(indicatorConstLp 2 hs hμs 1) y = Set.indicator s (fun x => 1) y
⊢ Set.indicator s (fun x_1 => x) y =
    (fun a => ↑(ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)) y
case h
α : Type u_1
E : Type ?u.8082404
F : Type u_2
G : Type ?u.8082410
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
x : F
h_compLp :
  (fun a =>
      ↑↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp 2 hs hμs 1)) a) =ᵐ[μ]
    fun a => ↑(ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
⊢ (Set.indicator s fun x_1 => x) =ᵐ[μ] fun a =>
    ↑(ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
refine' (@indicatorConstLp_coeFn _ _ _ 2 μ _ s hs hμs (1 : ℝ)).mono fun y hy => _
case h
α : Type u_1
E : Type ?u.8082404
F : Type u_2
G : Type ?u.8082410
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
x : F
h_compLp :
  (fun a =>
      ↑↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp 2 hs hμs 1)) a) =ᵐ[μ]
    fun a => ↑(ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
y : α
hy : ↑↑(indicatorConstLp 2 hs hμs 1) y = Set.indicator s (fun x => 1) y
⊢ Set.indicator s (fun x_1 => x) y = ↑(ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) y)
case h
α : Type u_1
E : Type ?u.8082404
F : Type u_2
G : Type ?u.8082410
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
x : F
h_compLp :
  (fun a =>
      ↑↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp 2 hs hμs 1)) a) =ᵐ[μ]
    fun a => ↑(ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
y : α
hy : ↑↑(indicatorConstLp 2 hs hμs 1) y = Set.indicator s (fun x => 1) y
⊢ Set.indicator s (fun x_1 => x) y =
    (fun a => ↑(ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)) y
dsimp only
case h
α : Type u_1
E : Type ?u.8082404
F : Type u_2
G : Type ?u.8082410
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
x : F
h_compLp :
  (fun a =>
      ↑↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp 2 hs hμs 1)) a) =ᵐ[μ]
    fun a => ↑(ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
y : α
hy : ↑↑(indicatorConstLp 2 hs hμs 1) y = Set.indicator s (fun x => 1) y
⊢ Set.indicator s (fun x_1 => x) y = ↑(ContinuousLinearMap.toSpanSingleton ℝ x) (Set.indicator s (fun x => 1) y)
case h
α : Type u_1
E : Type ?u.8082404
F : Type u_2
G : Type ?u.8082410
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
x : F
h_compLp :
  (fun a =>
      ↑↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp 2 hs hμs 1)) a) =ᵐ[μ]
    fun a => ↑(ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
y : α
hy : ↑↑(indicatorConstLp 2 hs hμs 1) y = Set.indicator s (fun x => 1) y
⊢ Set.indicator s (fun x_1 => x) y = ↑(ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) y)
rw [hy]
case h
α : Type u_1
E : Type ?u.8082404
F : Type u_2
G : Type ?u.8082410
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
x : F
h_compLp :
  (fun a =>
      ↑↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp 2 hs hμs 1)) a) =ᵐ[μ]
    fun a => ↑(ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
y : α
hy : ↑↑(indicatorConstLp 2 hs hμs 1) y = Set.indicator s (fun x => 1) y
⊢ Set.indicator s (fun x_1 => x) y = Set.indicator s (fun x => 1) y • x
case h
α : Type u_1
E : Type ?u.8082404
F : Type u_2
G : Type ?u.8082410
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
x : F
h_compLp :
  (fun a =>
      ↑↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp 2 hs hμs 1)) a) =ᵐ[μ]
    fun a => ↑(ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
y : α
hy : ↑↑(indicatorConstLp 2 hs hμs 1) y = Set.indicator s (fun x => 1) y
⊢ Set.indicator s (fun x_1 => x) y = ↑(ContinuousLinearMap.toSpanSingleton ℝ x) (Set.indicator s (fun x => 1) y)
simp_rw [ContinuousLinearMap.toSpanSingleton_apply]
no goals
case h
α : Type u_1
E : Type ?u.8082404
F : Type u_2
G : Type ?u.8082410
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
g : E → F
c : ℝ≥0
s : Set α
inst✝ : NormedSpace ℝ F
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
x : F
h_compLp :
  (fun a =>
      ↑↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp 2 hs hμs 1)) a) =ᵐ[μ]
    fun a => ↑(ContinuousLinearMap.toSpanSingleton ℝ x) (↑↑(indicatorConstLp 2 hs hμs 1) a)
y : α
hy : ↑↑(indicatorConstLp 2 hs hμs 1) y = Set.indicator s (fun x => 1) y
⊢ Set.indicator s (fun x_1 => x) y = Set.indicator s (fun x => 1) y • x
by_cases hy_mem : y ∈ s <;> simp [hy_mem, ContinuousLinearMap.lsmul_apply]