OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PlanarIMS.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

IMS localization for the actual planar kinetic and potential integrals. The partition functions need not have compact support; the test function does. In particular the exterior member of a multiwell partition is allowed.

  1. theorem OAI.ContinuumCoulomb.planarPartial_finsetSum line 14
  2. theorem OAI.ContinuumCoulomb.planar_partition_cross line 22
  3. theorem OAI.ContinuumCoulomb.planar_partition_gradient_identity line 37
  4. theorem OAI.ContinuumCoulomb.planar_partition_potential_identity line 55
  5. theorem OAI.ContinuumCoulomb.planar_partition_direction_integral line 67
  6. theorem OAI.ContinuumCoulomb.planar_potential_test_integrable line 90
  7. theorem OAI.ContinuumCoulomb.planar_IMS line 99

    Source documentation

    Exact IMS formula, with the localization cost expressed through the actual classical directional derivatives of the partition.

    theorem planar_IMS {ι : Type*} [Fintype ι]
    (θ : ι → PlanarPosition → ℝ) (hθ : ∀ i, ContDiff ℝ 1 (θ i))
    (hpart : ∀ x, ∑ i, θ i x ^ 2 = 1)
    (W u : PlanarPosition → ℝ) (hW : Continuous W)
    (hu : ContDiff ℝ 1 u) (hc : HasCompactSupport u) :
    (∑ i, planarTestForm W (fun x => θ i x * u x)) =
      planarTestForm W u + (1/2 : ℝ) *
        ∑ a : Fin 2, ∫ x, (∑ i, planarPartial (θ i) (planarAxis a) x ^ 2) * u x ^ 2 := by
…

    Mentions: OAI.ContinuumCoulomb.PlanarPosition, OAI.ContinuumCoulomb.planarTestForm, OAI.ContinuumCoulomb.planarPartial, OAI.ContinuumCoulomb.planarAxis