OAI/Topology/CoarseAssembly/LatticeHat.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Piecewise linear hat functions of the triangular lattice

The nodal function at a lattice vertex is max (0, 1 - ρ(p-v)), where ρ(x,y) = max(|x|, |y|, |x+y|). These are the barycentric coordinate functions for the filled triangular lattice. Their partition of unity maps the filled hexagons into Rips space.

  1. def OAI.CoarseAssembly.realLatticeRadius line 21
  2. theorem OAI.CoarseAssembly.realLatticeRadius_le_iff line 23
  3. theorem OAI.CoarseAssembly.realLatticeRadius_lt_iff line 27
  4. theorem OAI.CoarseAssembly.realLatticeRadius_continuous line 31
  5. def OAI.CoarseAssembly.hatKernel line 35
  6. def OAI.CoarseAssembly.latticeHat line 37
  7. theorem OAI.CoarseAssembly.latticeHat_nonneg line 40
  8. theorem OAI.CoarseAssembly.latticeHat_continuous line 43
  9. theorem OAI.CoarseAssembly.latticeHat_pos_iff line 47
  10. theorem OAI.CoarseAssembly.hatKernel_partition line 54

    Source documentation

    The four cell functions sum to one; at most three of them are positive.

    theorem hatKernel_partition {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t)
    (hs₁ : s ≤ 1) (ht₁ : t ≤ 1) :
    hatKernel s t + hatKernel (s - 1) t + hatKernel s (t - 1) +
      hatKernel (s - 1) (t - 1) = 1 := by
…

    Mentions: OAI.CoarseAssembly.hatKernel

  11. def OAI.CoarseAssembly.latticeCell line 105
  12. theorem OAI.CoarseAssembly.latticeHat_support_cell line 108
  13. def OAI.CoarseAssembly.latticeHatWeights line 121
  14. theorem OAI.CoarseAssembly.latticeHatWeights_apply line 124
  15. theorem OAI.CoarseAssembly.latticeHatWeights_total line 127
  16. theorem OAI.CoarseAssembly.latticeHat_adjacent line 143
  17. theorem OAI.CoarseAssembly.latticeHat_in_disc line 168