-- Mathlib/Analysis/InnerProductSpace/MeanErgodic.lean
theorem ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjection (f : E →L[𝕜] E)
    (hf : ‖f‖ ≤ 1) (x : E) :
    Tendsto (birkhoffAverage 𝕜 f _root_.id · x) atTop
      (𝓝 <| orthogonalProjection (LinearMap.eqLocus f 1) x)

Proof state:
case hg_ker.refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
x : E
hx : x ∈ (LinearMap.range (↑f - 1))ᗮ
⊢ ‖f x‖ ≤ ‖1 x‖

Tactic:
simpa using f.le_of_opNorm_le hf x

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
x : E
⊢ Tendsto (fun x_1 => birkhoffAverage 𝕜 (⇑f) _root_.id x_1 x) atTop
    (𝓝 ↑((orthogonalProjection (LinearMap.eqLocus f 1)) x))

Tactic:
apply (f : E →ₗ[𝕜] E).tendsto_birkhoffAverage_of_ker_subset_closure (f.lipschitz.weaken hf)

Result:
case hg_proj
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
x : E
⊢ ∀ (x : ↥(LinearMap.eqLocus (↑f) 1)), (orthogonalProjection (LinearMap.eqLocus f 1)) ↑x = x

case hg_ker
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
x : E
⊢ ↑(LinearMap.ker (orthogonalProjection (LinearMap.eqLocus f 1))) ⊆ closure ↑(LinearMap.range (↑f - 1))

Proof state:
case hg_ker.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
x : E
hx : x ∈ (LinearMap.range (↑f - 1))ᗮ
this : ∀ (y : E), inner (f y) x = inner y x
⊢ RCLike.re (inner (f x) (1 x)) = ‖1 x‖ ^ 2

Tactic:
simp [this, ← norm_sq_eq_inner]

Result:
no goals

Proof state:
case hg_ker.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
x : E
hx : x ∈ (LinearMap.range (↑f - 1))ᗮ
⊢ RCLike.re (inner (f x) (1 x)) = ‖1 x‖ ^ 2

Tactic:
have : ∀ y, ⟪f y, x⟫ = ⟪y, x⟫ := by
  simpa [Submodule.mem_orthogonal, inner_sub_left, sub_eq_zero] using hx

Result:
case hg_ker.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
x : E
hx : x ∈ (LinearMap.range (↑f - 1))ᗮ
this : ∀ (y : E), inner (f y) x = inner y x
⊢ RCLike.re (inner (f x) (1 x)) = ‖1 x‖ ^ 2

Proof state:
case hg_ker
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
⊢ (LinearMap.eqLocus f 1)ᗮ ≤ (LinearMap.range (↑f - 1))ᗮᗮ

Tactic:
refine Submodule.orthogonal_le fun x hx ↦ eq_of_norm_le_re_inner_eq_norm_sq (𝕜 := 𝕜) ?_ ?_

Result:
case hg_ker.refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
x : E
hx : x ∈ (LinearMap.range (↑f - 1))ᗮ
⊢ ‖f x‖ ≤ ‖1 x‖

case hg_ker.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
x : E
hx : x ∈ (LinearMap.range (↑f - 1))ᗮ
⊢ RCLike.re (inner (f x) (1 x)) = ‖1 x‖ ^ 2

Proof state:
case hg_ker
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
⊢ ↑(LinearMap.ker (orthogonalProjection (LinearMap.eqLocus f 1))) ⊆ closure ↑(LinearMap.range (↑f - 1))

Tactic:
rw [ker_orthogonalProjection, ← Submodule.topologicalClosure_coe, SetLike.coe_subset_coe,
  ← Submodule.orthogonal_orthogonal_eq_closure]

Result:
case hg_ker
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
⊢ (LinearMap.eqLocus f 1)ᗮ ≤ (LinearMap.range (↑f - 1))ᗮᗮ

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
x : E
hx : x ∈ (LinearMap.range (↑f - 1))ᗮ
⊢ ∀ (y : E), inner (f y) x = inner y x

Tactic:
simpa [Submodule.mem_orthogonal, inner_sub_left, sub_eq_zero] using hx

Result:
no goals

Proof state:
case hg_ker
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
x : E
⊢ ↑(LinearMap.ker (orthogonalProjection (LinearMap.eqLocus f 1))) ⊆ closure ↑(LinearMap.range (↑f - 1))

Tactic:
clear x

Result:
case hg_ker
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
⊢ ↑(LinearMap.ker (orthogonalProjection (LinearMap.eqLocus f 1))) ⊆ closure ↑(LinearMap.range (↑f - 1))

Proof state:
case hg_proj
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
x : E
⊢ ∀ (x : ↥(LinearMap.eqLocus (↑f) 1)), (orthogonalProjection (LinearMap.eqLocus f 1)) ↑x = x

Tactic:
exact orthogonalProjection_mem_subspace_eq_self (K := LinearMap.eqLocus f 1)

Result:
no goals