OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PlanarPartition.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A smooth square partition for finitely many disjoint planar cutoffs. The exterior function is smooth even on the regions where all site cutoffs vanish; no square root at a zero is used.

  1. def OAI.ContinuumCoulomb.planarTrigPartition line 15
  2. theorem OAI.ContinuumCoulomb.planarTrigPartition_C1 line 20
  3. theorem OAI.ContinuumCoulomb.disjoint_cutoff_vanish line 27
  4. theorem OAI.ContinuumCoulomb.planarTrigPartition_exterior_at line 37
  5. theorem OAI.ContinuumCoulomb.planarTrigPartition_square_sum line 51

    Source documentation

    The exterior and all site members have square sum exactly one.

    theorem planarTrigPartition_square_sum {ι : Type*} [Fintype ι]
    (χ : ι → PlanarPosition → ℝ)
    (hdisj : ∀ i j, i ≠ j → Disjoint (tsupport (χ i)) (tsupport (χ j)))
    (x : PlanarPosition) : ∑ i, planarTrigPartition χ i x ^ 2 = 1 := by
…

    Mentions: OAI.ContinuumCoulomb.PlanarPosition, OAI.ContinuumCoulomb.planarTrigPartition

  6. theorem OAI.ContinuumCoulomb.planarTrigPartition_partial_site line 74
  7. theorem OAI.ContinuumCoulomb.planarTrigPartition_partial_exterior line 83
  8. theorem OAI.ContinuumCoulomb.planarTrigPartition_gradient_square line 100

    Source documentation

    Disjoint supports prevent a factor equal to the number of wells in the localization error: the square gradient equals that of the active angle.

    theorem planarTrigPartition_gradient_square {ι : Type*} [Fintype ι]
    (χ : ι → PlanarPosition → ℝ) (hχ : ∀ i, ContDiff ℝ 1 (χ i))
    (hdisj : ∀ i j, i ≠ j → Disjoint (tsupport (χ i)) (tsupport (χ j)))
    (e x : PlanarPosition) :
    (∑ i, planarPartial (planarTrigPartition χ i) e x ^ 2) =
      ∑ i, planarPartial (χ i) e x ^ 2 := by
…

    Mentions: OAI.ContinuumCoulomb.PlanarPosition, OAI.ContinuumCoulomb.planarPartial, OAI.ContinuumCoulomb.planarTrigPartition

  9. theorem OAI.ContinuumCoulomb.planarTrigPartition_gradient_bound line 140