AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.ClosedGraphResolvent

- Orthogonal projection onto the scaled closed graph constructs the unique weak solution. Norms of domain elements below are their ambient H norms; the explicit bounds depend on epsilon and do not persist uniformly as it approaches zero.

theorem weak_resolvent {H K : Type*}
    [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
    [NormedAddCommGroup K] [InnerProductSpace ℝ K] [CompleteSpace K]
    (A : H →ₗ.[ℝ] K) (hA : A.IsClosed) (ε : ℝ) (hε : 0 < ε) (f : H) :
    ∃ u : A.domain,
      (∀ v : A.domain, ε * ⟪(u : H), (v : H)⟫ + ⟪A u, A v⟫ = ⟪f, (v : H)⟫) ∧
      ε * ‖(u : H)‖^2 + ‖A u‖^2 = ⟪f, (u : H)⟫ ∧
      ‖(u : H)‖ ≤ ε⁻¹ * ‖f‖ ∧
      ε * ‖(u : H)‖^2 + ‖A u‖^2 ≤ ε⁻¹ * ‖f‖^2 ∧
      ∀ w : A.domain,
        (∀ v : A.domain, ε * ⟪(w : H), (v : H)⟫ + ⟪A w, A v⟫ = ⟪f, (v : H)⟫) → w = u := by
  have hex : ∃ u : A.domain, ∀ v : A.domain,
      ε * ⟪(u : H), (v : H)⟫ + ⟪A u, A v⟫ = ⟪f, (v : H)⟫ := by
    let s := Real.sqrt ε
    have hs : 0 < s := Real.sqrt_pos.2 hε
    have hs0 : s ≠ 0 := ne_of_gt hs
    have hss : s * s = ε := Real.mul_self_sqrt hε.le
    let T : WithLp 2 (H × K) →L[ℝ] H × K :=
      (s⁻¹ • (WithLp.fstL 2 ℝ H K)).prod (WithLp.sndL 2 ℝ H K)
    let G : Submodule ℝ (WithLp 2 (H × K)) := A.graph.comap T.toLinearMap
    have hG : IsClosed (G : Set (WithLp 2 (H × K))) := hA.preimage T.continuous
    let : CompleteSpace G := hG.completeSpace_coe
    let z : WithLp 2 (H × K) := WithLp.toLp 2 (s⁻¹ • f, 0)
    let p := G.starProjection z
    have hp : T p ∈ A.graph := G.starProjection_apply_mem z
    obtain ⟨u,hu,hAu⟩ := A.mem_graph_iff.mp hp
    have hu' : s • (u : H) = p.fst := by
      rw [hu]
      change s • (s⁻¹ • p.fst) = p.fst
      simp [smul_smul, hs0]
    refine ⟨u, ?_⟩
    intro v
    let w : WithLp 2 (H × K) := WithLp.toLp 2 (s • (v : H), A v)
    have hw : w ∈ G := by
      change T w ∈ A.graph
      apply A.mem_graph_iff.mpr
      refine ⟨v, ?_, ?_⟩
      · change (v : H) = s⁻¹ • (s • (v : H))
        simp [smul_smul, hs0]
      · rfl
    have ho := G.starProjection_inner_eq_zero z w hw
    change ⟪s⁻¹ • f - p.fst, s • (v : H)⟫ + ⟪(0 : K) - p.snd, A v⟫ = 0 at ho
    have hAu' : A u = p.snd := hAu
    rw [← hu', ← hAu'] at ho
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/ClosedGraphResolvent.lean:24published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.