OAI/Geometry/ProjectionBodies/AffinePosition.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PettyProjection.measurePair line 14

   Source documentation

   The genuine unpolarized cosine pairing of two (not necessarily even) measures.

   def measurePair {n : ℕ} (μ ν : Measure (Space n)) : ℝ :=
   …

   Mentions: OAI.PettyProjection.Space

2. def OAI.PettyProjection.Represents line 17
3. lemma OAI.PettyProjection.represents_pair line 22
4. lemma OAI.PettyProjection.RelativeGauge.scaled_represents line 50
5. lemma OAI.PettyProjection.Position.compact_inward line 76
6. lemma OAI.PettyProjection.Position.inward_perturbation line 105
7. theorem OAI.PettyProjection.Position.traceOne_field_zero line 140

   Source documentation

   The topological mechanism. The field is genuine and continuous; its negativity on every null direction forces an interior zero.

   theorem traceOne_field_zero {n : ℕ} [NeZero n] (F : {A : Mat n // A∈domain n} → Mat n)
       (hFc : Continuous F) (hFs : ∀ A,Symmetric (F A)) (hFt : ∀ A,tr (F A)=0)
       (hFk : ∀ A (e : Sphere n),op A.val e=0 → quad (F A) e<0) :
       ∃ A : {A : Mat n // A∈domain n},F A=0 ∧ Function.Injective (op A.val) := by
   …

   Mentions: OAI.PettyProjection.Position.Mat, OAI.PettyProjection.Position.domain, OAI.PettyProjection.Position.Symmetric, OAI.PettyProjection.Position.tr, OAI.PettyProjection.Position.op, OAI.PettyProjection.Position.quad

8. abbrev OAI.PettyProjection.Position.Domain line 187
9. instance OAI.PettyProjection.Position.domain_compactSpace line 188
10. def OAI.PettyProjection.Position.domainMap line 190
11. lemma OAI.PettyProjection.Position.domainMap_continuous line 192
12. lemma OAI.PettyProjection.Position.optimizer_kernel line 195
13. lemma OAI.PettyProjection.Position.optimizer_joint_continuous line 212
14. def OAI.PettyProjection.Position.positionField line 217
15. lemma OAI.PettyProjection.Position.positionField_continuous line 221
16. theorem OAI.PettyProjection.Position.exists_optimizer_position line 244

    Source documentation

    A genuine nonsingular affine position for the variational optimizer. The trace-one representative is used here; determinant normalization is a scalar change and is performed in the global assembly.

    theorem exists_optimizer_position (hμ : Integrable (fun x : Space n => ‖x‖) μ)
        (hq : ∀ x : Space n,x≠0 → 0<cosineSeminorm μ hμ x) (b : Bool) {k : ℕ} (hk : 0<k) :
        ∃ A : Domain n,Function.Injective (op A.val) ∧
          momentField (optimizer hμ hq b (domainMap A)).toSeminorm k=0 := by
    …

    Mentions: OAI.PettyProjection.Space, OAI.PettyProjection.cosineSeminorm, OAI.PettyProjection.Position.Domain, OAI.PettyProjection.Position.op, OAI.PettyProjection.Position.momentField, OAI.PettyProjection.Position.domainMap

17. lemma OAI.PettyProjection.volumeReal_linearEquiv line 264
18. lemma OAI.PettyProjection.linearEquiv_body line 269
19. lemma OAI.PettyProjection.linearEquiv_det_ne_zero line 276
20. def OAI.PettyProjection.volumeFactor line 279
21. lemma OAI.PettyProjection.volumeFactor_pos line 280
22. lemma OAI.PettyProjection.normalizedVolume_linearEquiv line 283
23. lemma OAI.PettyProjection.volumeFactor_symm line 290
24. lemma OAI.PettyProjection.symmetric_equiv_symm line 295
25. lemma OAI.PettyProjection.functional_map_symmetric line 303
26. lemma OAI.PettyProjection.measurePair_cosine line 314
27. lemma OAI.PettyProjection.measurePair_map_symmetric line 323
28. lemma OAI.PettyProjection.Position.mean_inner_sq line 346
29. lemma OAI.PettyProjection.Position.symmetric_eq_zero_of_quad line 361
30. lemma OAI.PettyProjection.Position.constantMomentField_zero line 371
31. lemma OAI.PettyProjection.Position.coordinateProduct_mean line 380
32. lemma OAI.PettyProjection.Position.field_zero_harmonic line 389

    Source documentation

    The matrix isotropy condition gives precisely the actual H₂ projection, not a replacement cancellation condition.

    lemma field_zero_harmonic {n : ℕ} (hn : 2≤n) [NeZero n] (g : Seminorm ℝ (Space n))
        (hg : g≠0) (k : ℕ) (hF : momentField g k=0) :
        (harmonicSpace n 2).starProjection (toH n
          (restrictContinuous (fun x => g x^k) ((seminorm_continuous n g).pow k)))=0 := by
    …

    Mentions: OAI.PettyProjection.Space, OAI.PettyProjection.Position.momentField

33. def OAI.PettyProjection.RelativeGauge.IsMinimizer line 446
34. lemma OAI.PettyProjection.RelativeGauge.copy_minimizer line 452
35. theorem OAI.PettyProjection.RelativeGauge.exists_symmetric_position line 463

    Source documentation

    Actual full-dimensional position of the logarithmic/linear optimizer, with no determinant normalization needed in the later weighted assembly.

    theorem exists_symmetric_position {μ : Measure (Space n)}
        (hμ : Integrable (fun x : Space n => ‖x‖) μ)
        (hq : ∀ x : Space n,x≠0 → 0 < cosineSeminorm μ hμ x) :
        ∃ T : Space n ≃L[ℝ] Space n,T.toLinearMap.IsSymmetric ∧
          ∃ g : RelativeGauge (⊤ : Submodule ℝ (Space n)),IsMinimizer (μ.map T) (regime n) g ∧
            Position.momentField g.toSeminorm (Scalar.exponent n)=0 := by
    …

    Mentions: OAI.PettyProjection.Space, OAI.PettyProjection.cosineSeminorm, OAI.PettyProjection.RelativeGauge, OAI.PettyProjection.RelativeGauge.IsMinimizer, OAI.PettyProjection.regime, OAI.PettyProjection.Position.momentField, OAI.PettyProjection.Scalar.exponent

36. lemma OAI.PettyProjection.RelativeGauge.exists_full_minimizer line 482