Documentation

LeanPool.ParameterFreeGradient.V7.Proofs.Stage5AboveTwoLowerS5AGlobalC2.Continuity

Continuity of the assembled kernel Hessian at all points.

source
noncomputable def V7.Stage5AboveTwoLower.S5AGlobalC2.pairingCLMLinear {d : ℕ} :
Point d →ₗ[ℝ] Point d →L[ℝ] ℝ

The linear map sending a vector to its continuous pairing functional.

Equations
Instances For
    source
    noncomputable def V7.Stage5AboveTwoLower.S5AGlobalC2.pairingCLMCLM {d : ℕ} :
    Point d →L[ℝ] Point d →L[ℝ] ℝ

    The continuous linear map sending a vector to its pairing functional.

    Equations
    Instances For
      source
      @[simp]
      theorem V7.Stage5AboveTwoLower.S5AGlobalC2.pairingCLMCLM_apply {d : ℕ} (g : Point d) :
      pairingCLMCLM g = S5ARepair.pairingCLM g
      source
      theorem V7.Stage5AboveTwoLower.S5AGlobalC2.continuous_powerDualityMap {r : ℝ} (hr : 2 < r) {d : ℕ} :
      Continuous (O3.powerDualityMap r)
      source
      theorem V7.Stage5AboveTwoLower.S5AGlobalC2.continuous_lpPowerFDeriv {r : ℝ} (hr : 2 < r) {d : ℕ} :
      Continuous (S5ARepair.lpPowerFDeriv r)
      source
      theorem V7.Stage5AboveTwoLower.S5AGlobalC2.continuous_lpPower {r : ℝ} (hr : 2 < r) {d : ℕ} :
      Continuous (O3.lpPower r)
      source
      theorem V7.Stage5AboveTwoLower.S5AGlobalC2.continuousAt_kernelHessianCoord_of_ne_zero {r theta : ℝ} (hr : 2 < r) {d : ℕ} (x : Point d) (hx : x ≠ 0) (i : Fin d) :
      ContinuousAt (fun (y : Point d) => S5ARepair.kernelHessianCoord r theta y i) x
      source
      noncomputable def V7.Stage5AboveTwoLower.S5AGlobalC2.assemblePiLinear {d : ℕ} :
      (Fin d → Point d →L[ℝ] ℝ) →ₗ[ℝ] Point d →L[ℝ] Point d

      The linear assembly of coordinate functionals into a vector-valued continuous linear map.

      Equations
      Instances For
        source
        noncomputable def V7.Stage5AboveTwoLower.S5AGlobalC2.assemblePiCLM {d : ℕ} :
        (Fin d → Point d →L[ℝ] ℝ) →L[ℝ] Point d →L[ℝ] Point d

        The continuous linear assembly of coordinate functionals into a vector-valued derivative.

        Equations
        Instances For
          source
          @[simp]
          theorem V7.Stage5AboveTwoLower.S5AGlobalC2.assemblePiCLM_apply {d : ℕ} (f : Fin d → Point d →L[ℝ] ℝ) :
          assemblePiCLM f = ContinuousLinearMap.pi f
          source
          theorem V7.Stage5AboveTwoLower.S5AGlobalC2.continuousAt_kernelHessian_of_ne_zero {r theta : ℝ} (hr : 2 < r) {d : ℕ} (x : Point d) (hx : x ≠ 0) :
          ContinuousAt (S5ARepair.kernelHessian r theta) x
          source
          theorem V7.Stage5AboveTwoLower.S5AGlobalC2.continuous_kernelHessian {r theta : ℝ} (hr : 2 < r) (htheta : 1 < theta) (htr : 2 * theta < r) {d : ℕ} :
          Continuous (S5ARepair.kernelHessian r theta)

          The exact concrete Hessian is globally continuous in CLM operator norm.