OAI/Geometry/ProjectionBodies/Support.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PettyProjection.support line 13

    Source documentation

    The actual support function of a compact body, not a surrogate gauge.

    def support {n : ℕ} (K : Set (Space n)) (u : Space n) : ℝ :=
…

    Mentions: OAI.PettyProjection.Space

  2. lemma OAI.PettyProjection.support_attained line 16
  3. lemma OAI.PettyProjection.inner_le_support line 20
  4. lemma OAI.PettyProjection.support_le_iff line 24
  5. lemma OAI.PettyProjection.support_continuous line 32
  6. lemma OAI.PettyProjection.support_lipschitz line 36
  7. lemma OAI.PettyProjection.support_smul line 51
  8. lemma OAI.PettyProjection.support_add_le line 62
  9. lemma OAI.PettyProjection.support_nonneg line 69
  10. lemma OAI.PettyProjection.support_minkowski line 73
  11. lemma OAI.PettyProjection.support_linear_image line 86
  12. lemma OAI.PettyProjection.mem_iff_inner_le_support line 98
  13. lemma OAI.PettyProjection.support_eq_iff line 115
  14. lemma OAI.PettyProjection.Spherical.harmonicSpace_isHilbertSum line 133
  15. lemma OAI.PettyProjection.Spherical.polynomialL2_X_mul_X line 145
  16. lemma OAI.PettyProjection.Spherical.polynomialL2_X_mul_mem_lowSpace line 152
  17. lemma OAI.PettyProjection.Spherical.homogeneous_two_mem_lowSpace line 170
  18. lemma OAI.PettyProjection.Spherical.harmonicSpace_two_le_lowSpace line 179
  19. lemma OAI.PettyProjection.hilbertSum_component line 195
  20. lemma OAI.PettyProjection.hilbertSum_hasSum_projection line 207
  21. lemma OAI.PettyProjection.hilbertSum_hasSum_projection_norm_sq line 213