OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/Perturbation.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Second-order block estimates

The finite reductions use the bottom-energy estimate from the binary manuscript's lem:second-order and the unit manuscript's lem:perturbation. Explicit positivity and operator norm bounds give vector and variational estimates for the penalty, inverse, coupling and high perturbation blocks.

Real inner products also express the real quadratic forms of complex spin Hilbert spaces by restriction of scalars.

  1. def OAI.ContinuumCoulomb.Perturbation.penaltyForm line 38
  2. def OAI.ContinuumCoulomb.Perturbation.inverseForm line 40
  3. def OAI.ContinuumCoulomb.Perturbation.blockEnergy line 44

    Source documentation

    Full block energy when the low-low perturbation block vanishes.

    def blockEnergy (A D : H →L[ℝ] H) (B : L →L[ℝ] H) (p : L) (q : H) : ℝ :=
…
  4. theorem OAI.ContinuumCoulomb.Perturbation.inverseForm_nonneg line 47
  5. theorem OAI.ContinuumCoulomb.Perturbation.penalty_square_identity line 54

    Source documentation

    The precise square-completion identity, before any estimates.

    theorem penalty_square_identity (A T : H →L[ℝ] H) (B : L →L[ℝ] H)
    (hAT : ∀ x, A (T x) = x)
    (hAsymm : ∀ x y, ⟪x, A y⟫_ℝ = ⟪A x, y⟫_ℝ)
    (p : L) (q : H) {σ : ℝ} (hσ : σ ≠ 0) :
    σ * penaltyForm A q + 2 * ⟪q, B p⟫_ℝ =
      σ * penaltyForm A (q + σ⁻¹ • T (B p)) - σ⁻¹ * inverseForm T B p := by
…

    Mentions: OAI.ContinuumCoulomb.Perturbation.penaltyForm, OAI.ContinuumCoulomb.Perturbation.inverseForm

  6. theorem OAI.ContinuumCoulomb.Perturbation.blockEnergy_trial_identity line 69

    Source documentation

    The trial vector used in the second-order variational upper bound.

    theorem blockEnergy_trial_identity (A T D : H →L[ℝ] H) (B : L →L[ℝ] H)
    (hAT : ∀ x, A (T x) = x) (p : L) :
    blockEnergy A D B p (-(T (B p))) =
      -inverseForm T B p + ⟪-(T (B p)), D (-(T (B p)))⟫_ℝ := by
…

    Mentions: OAI.ContinuumCoulomb.Perturbation.blockEnergy, OAI.ContinuumCoulomb.Perturbation.inverseForm

  7. theorem OAI.ContinuumCoulomb.Perturbation.inverse_coupling_norm_le line 78
  8. theorem OAI.ContinuumCoulomb.Perturbation.inverseForm_le line 90
  9. theorem OAI.ContinuumCoulomb.Perturbation.highPerturbation_abs_le line 103
  10. theorem OAI.ContinuumCoulomb.Perturbation.highPerturbation_relative_lower line 114
  11. theorem OAI.ContinuumCoulomb.Perturbation.blockEnergy_lower line 123

    Source documentation

    Completing a square lowers the full form by the inverse coupling form.

    theorem blockEnergy_lower (A T D : H →L[ℝ] H) (B : L →L[ℝ] H)
    {g ε : ℝ} (hε : 0 ≤ ε) (hε1 : ε < 1)
    (hAT : ∀ x, A (T x) = x)
    (hAsymm : ∀ x y, ⟪x, A y⟫_ℝ = ⟪A x, y⟫_ℝ)
    (hA : ∀ q, 0 ≤ penaltyForm A q)
    (hgap : ∀ q, g * ‖q‖ ^ 2 ≤ penaltyForm A q)
    (hD : ‖D‖ ≤ ε * g) (p : L) (q : H) :
    -inverseForm T B p / (1 - ε) ≤ blockEnergy A D B p q := by
…

    Mentions: OAI.ContinuumCoulomb.Perturbation.penaltyForm, OAI.ContinuumCoulomb.Perturbation.inverseForm, OAI.ContinuumCoulomb.Perturbation.blockEnergy

  12. def OAI.ContinuumCoulomb.Perturbation.blockRayleigh line 139
  13. def OAI.ContinuumCoulomb.Perturbation.blockBottom line 142
  14. theorem OAI.ContinuumCoulomb.Perturbation.blockRayleigh_lower line 147

    Source documentation

    Pointwise inverse-form control gives the lower Rayleigh bound.

    theorem blockRayleigh_lower (A T D : H →L[ℝ] H) (B : L →L[ℝ] H)
    {g ε κ : ℝ} (hε : 0 ≤ ε) (hε1 : ε < 1) (hκ : 0 ≤ κ)
    (hAT : ∀ x, A (T x) = x)
    (hAsymm : ∀ x y, ⟪x, A y⟫_ℝ = ⟪A x, y⟫_ℝ)
    (hA : ∀ q, 0 ≤ penaltyForm A q)
    (hgap : ∀ q, g * ‖q‖ ^ 2 ≤ penaltyForm A q)
    (hD : ‖D‖ ≤ ε * g)
    (hK : ∀ p, inverseForm T B p ≤ κ * ‖p‖ ^ 2)
    (p : L) (q : H) (hnorm : 0 < ‖p‖ ^ 2 + ‖q‖ ^ 2) :
    -κ / (1 - ε) ≤ blockRayleigh A D B p q := by
…

    Mentions: OAI.ContinuumCoulomb.Perturbation.penaltyForm, OAI.ContinuumCoulomb.Perturbation.inverseForm, OAI.ContinuumCoulomb.Perturbation.blockRayleigh

  15. theorem OAI.ContinuumCoulomb.Perturbation.cubic_lower_error line 166
  16. theorem OAI.ContinuumCoulomb.Perturbation.blockRayleigh_trial_upper line 177

    Source documentation

    The explicit second-order trial vector gives a cubic upper error.

    theorem blockRayleigh_trial_upper (A T D : H →L[ℝ] H) (B : L →L[ℝ] H)
    {g ε κ : ℝ} (hg : 0 < g) (hε : 0 ≤ ε) (hεhalf : ε < 1 / 2)
    (hAT : ∀ x, A (T x) = x)
    (hT : ‖T‖ ≤ 1 / g) (hB : ‖B‖ ≤ ε * g) (hD : ‖D‖ ≤ ε * g)
    (hκ : κ ≤ g * ε ^ 2)
    (p : L) (hp : ‖p‖ = 1) (hattain : inverseForm T B p = κ) :
    blockRayleigh A D B p (-(T (B p))) ≤ -κ + 2 * g * ε ^ 3 := by
…

    Mentions: OAI.ContinuumCoulomb.Perturbation.inverseForm, OAI.ContinuumCoulomb.Perturbation.blockRayleigh

  17. theorem OAI.ContinuumCoulomb.Perturbation.blockBottom_second_order line 211

    Source documentation

    Supporting variational second-order estimate for the zero low-low block case. The effective positive inverse form is bounded by κ and attains it at the supplied unit vector, exactly as for the maximum eigenvector of the finite positive matrix PBA⁻¹BP in the manuscript.

    theorem blockBottom_second_order (A T D : H →L[ℝ] H) (B : L →L[ℝ] H)
    {g ε κ : ℝ} (hg : 0 < g) (hε : 0 ≤ ε) (hεhalf : ε < 1 / 2)
    (hAT : ∀ x, A (T x) = x)
    (hAsymm : ∀ x y, ⟪x, A y⟫_ℝ = ⟪A x, y⟫_ℝ)
    (hA : ∀ q, 0 ≤ penaltyForm A q)
    (hgap : ∀ q, g * ‖q‖ ^ 2 ≤ penaltyForm A q)
    (hT : ‖T‖ ≤ 1 / g) (hB : ‖B‖ ≤ ε * g) (hD : ‖D‖ ≤ ε * g)
    (hK : ∀ p, inverseForm T B p ≤ κ * ‖p‖ ^ 2)
    (p₀ : L) (hp₀ : ‖p₀‖ = 1) (hattain : inverseForm T B p₀ = κ) :
    |blockBottom A D B + κ| ≤ 2 * g * ε ^ 3 := by
…

    Mentions: OAI.ContinuumCoulomb.Perturbation.penaltyForm, OAI.ContinuumCoulomb.Perturbation.inverseForm, OAI.ContinuumCoulomb.Perturbation.blockBottom

  18. def OAI.ContinuumCoulomb.Perturbation.effectiveForm line 250

    Source documentation

    First-order low compression together with its second-order inverse term.

    def effectiveForm (C : L →L[ℝ] L) (T : H →L[ℝ] H) (B : L →L[ℝ] H)
    (p : L) : ℝ := ⟪p, C p⟫_ℝ - inverseForm T B p

    Mentions: OAI.ContinuumCoulomb.Perturbation.inverseForm

  19. theorem OAI.ContinuumCoulomb.Perturbation.effectiveForm_smul line 253
  20. theorem OAI.ContinuumCoulomb.Perturbation.effectiveForm_minimizer line 262

    Source documentation

    Finite dimensionality supplies the effective ground vector; this is not an additional simulation assumption.

    theorem effectiveForm_minimizer [FiniteDimensional ℝ L]
    (C : L →L[ℝ] L) (T : H →L[ℝ] H) (B : L →L[ℝ] H)
    (u : L) (hu : ‖u‖ = 1) :
    ∃ p : L, ‖p‖ = 1 ∧
      ∀ x : L, effectiveForm C T B p * ‖x‖ ^ 2 ≤ effectiveForm C T B x := by
…

    Mentions: OAI.ContinuumCoulomb.Perturbation.effectiveForm

  21. def OAI.ContinuumCoulomb.Perturbation.effectiveBottom line 289
  22. theorem OAI.ContinuumCoulomb.Perturbation.effectiveBottom_eq line 292
  23. def OAI.ContinuumCoulomb.Perturbation.lowBlockEnergy line 303
  24. def OAI.ContinuumCoulomb.Perturbation.lowBlockRayleigh line 307
  25. def OAI.ContinuumCoulomb.Perturbation.lowBlockBottom line 311
  26. theorem OAI.ContinuumCoulomb.Perturbation.effectiveForm_bounds line 316
  27. theorem OAI.ContinuumCoulomb.Perturbation.first_order_inverse_cubic_loss line 329
  28. theorem OAI.ContinuumCoulomb.Perturbation.lowBlockEnergy_shift_lower line 347

    Source documentation

    A shifted square gives the lower bound even when the first-order compression is nonzero. The effective form is only assumed bounded below pointwise; the full-energy conclusion is proved here.

    theorem lowBlockEnergy_shift_lower (C : L →L[ℝ] L) (A T D : H →L[ℝ] H)
    (B : L →L[ℝ] H) {g ε μ : ℝ}
    (hg : 0 < g) (hε : 0 ≤ ε) (hεquarter : ε ≤ 1 / 4)
    (hAT : ∀ x, A (T x) = x)
    (hAsymm : ∀ x y, ⟪x, A y⟫_ℝ = ⟪A x, y⟫_ℝ)
    (hA : ∀ q, 0 ≤ penaltyForm A q)
    (hgap : ∀ q, g * ‖q‖ ^ 2 ≤ penaltyForm A q)
    (hT : ‖T‖ ≤ 1 / g) (hB : ‖B‖ ≤ ε * g) (hD : ‖D‖ ≤ ε * g)
    (hμupper : μ ≤ ε * g)
    (hmin : ∀ p, μ * ‖p‖ ^ 2 ≤ effectiveForm C T B p)
    (p : L) (q : H) :
    -4 * g * ε ^ 3 * ‖p‖ ^ 2 ≤
…

    Mentions: OAI.ContinuumCoulomb.Perturbation.penaltyForm, OAI.ContinuumCoulomb.Perturbation.effectiveForm

  29. theorem OAI.ContinuumCoulomb.Perturbation.lowBlockRayleigh_lower line 373
  30. theorem OAI.ContinuumCoulomb.Perturbation.lowBlockRayleigh_trial_upper line 394

    Source documentation

    The same inverse-coupling trial vector works with the unreplaced low-block terms retained.

    theorem lowBlockRayleigh_trial_upper (C : L →L[ℝ] L) (A T D : H →L[ℝ] H)
    (B : L →L[ℝ] H) {g ε μ : ℝ}
    (hg : 0 < g) (hε : 0 ≤ ε)
    (hAT : ∀ x, A (T x) = x)
    (hT : ‖T‖ ≤ 1 / g) (hB : ‖B‖ ≤ ε * g) (hD : ‖D‖ ≤ ε * g)
    (hμlower : -2 * ε * g ≤ μ)
    (p : L) (hp : ‖p‖ = 1) (hattain : effectiveForm C T B p = μ) :
    lowBlockRayleigh C A D B p (-(T (B p))) ≤ μ + 3 * g * ε ^ 3 := by
…

    Mentions: OAI.ContinuumCoulomb.Perturbation.effectiveForm, OAI.ContinuumCoulomb.Perturbation.lowBlockRayleigh

  31. theorem OAI.ContinuumCoulomb.Perturbation.lowBlockBottom_second_order line 421

    Source documentation

    Quantitative version of the unit manuscript's lem:perturbation, retaining the nonzero first-order compression. μ is the attained variational minimum of C - B* T B; the full variational bottom is proved within 4 g ε³ of it.

    theorem lowBlockBottom_second_order (C : L →L[ℝ] L) (A T D : H →L[ℝ] H)
    (B : L →L[ℝ] H) {g ε μ : ℝ}
    (hg : 0 < g) (hε : 0 ≤ ε) (hεquarter : ε ≤ 1 / 4)
    (hAT : ∀ x, A (T x) = x)
    (hAsymm : ∀ x y, ⟪x, A y⟫_ℝ = ⟪A x, y⟫_ℝ)
    (hA : ∀ q, 0 ≤ penaltyForm A q)
    (hgap : ∀ q, g * ‖q‖ ^ 2 ≤ penaltyForm A q)
    (hT : ‖T‖ ≤ 1 / g) (hB : ‖B‖ ≤ ε * g)
    (hC : ‖C‖ ≤ ε * g) (hD : ‖D‖ ≤ ε * g)
    (hmin : ∀ p, μ * ‖p‖ ^ 2 ≤ effectiveForm C T B p)
    (p₀ : L) (hp₀ : ‖p₀‖ = 1) (hattain : effectiveForm C T B p₀ = μ) :
    |lowBlockBottom C A D B - μ| ≤ 4 * g * ε ^ 3 := by
…

    Mentions: OAI.ContinuumCoulomb.Perturbation.penaltyForm, OAI.ContinuumCoulomb.Perturbation.effectiveForm, OAI.ContinuumCoulomb.Perturbation.lowBlockBottom

  32. theorem OAI.ContinuumCoulomb.Perturbation.finite_lowBlockBottom_second_order line 464

    Source documentation

    The finite-dimensional, nonzero-low-block perturbation estimate compares the two actual variational infima.

    theorem finite_lowBlockBottom_second_order [FiniteDimensional ℝ L]
    (C : L →L[ℝ] L) (A T D : H →L[ℝ] H) (B : L →L[ℝ] H)
    {g ε : ℝ} (hg : 0 < g) (hε : 0 ≤ ε) (hεquarter : ε ≤ 1 / 4)
    (hAT : ∀ x, A (T x) = x)
    (hAsymm : ∀ x y, ⟪x, A y⟫_ℝ = ⟪A x, y⟫_ℝ)
    (hA : ∀ q, 0 ≤ penaltyForm A q)
    (hgap : ∀ q, g * ‖q‖ ^ 2 ≤ penaltyForm A q)
    (hT : ‖T‖ ≤ 1 / g) (hB : ‖B‖ ≤ ε * g)
    (hC : ‖C‖ ≤ ε * g) (hD : ‖D‖ ≤ ε * g)
    (u : L) (hu : ‖u‖ = 1) :
    |lowBlockBottom C A D B - effectiveBottom C T B| ≤ 4 * g * ε ^ 3 := by
…

    Mentions: OAI.ContinuumCoulomb.Perturbation.penaltyForm, OAI.ContinuumCoulomb.Perturbation.lowBlockBottom, OAI.ContinuumCoulomb.Perturbation.effectiveBottom

  33. theorem OAI.ContinuumCoulomb.Perturbation.finite_blockBottom_second_order line 482

    Source documentation

    The sharper zero-low-block estimate also compares actual variational infima without a separately supplied effective maximizing vector.

    theorem finite_blockBottom_second_order [FiniteDimensional ℝ L]
    (A T D : H →L[ℝ] H) (B : L →L[ℝ] H)
    {g ε : ℝ} (hg : 0 < g) (hε : 0 ≤ ε) (hεhalf : ε < 1 / 2)
    (hAT : ∀ x, A (T x) = x)
    (hAsymm : ∀ x y, ⟪x, A y⟫_ℝ = ⟪A x, y⟫_ℝ)
    (hA : ∀ q, 0 ≤ penaltyForm A q)
    (hgap : ∀ q, g * ‖q‖ ^ 2 ≤ penaltyForm A q)
    (hT : ‖T‖ ≤ 1 / g) (hB : ‖B‖ ≤ ε * g) (hD : ‖D‖ ≤ ε * g)
    (u : L) (hu : ‖u‖ = 1) :
    |blockBottom A D B - effectiveBottom (0 : L →L[ℝ] L) T B| ≤ 2 * g * ε ^ 3 := by
…

    Mentions: OAI.ContinuumCoulomb.Perturbation.penaltyForm, OAI.ContinuumCoulomb.Perturbation.blockBottom, OAI.ContinuumCoulomb.Perturbation.effectiveBottom