GramMetric.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Choosing the actual metric from the coordinate differentials

The Gram tensor is the sum of the rank-one coordinate tensors. Regularization makes it a positive definite metric, and the integral bound is for its actual inverse-matrix energy density.

def OAI.CircleDomainRigidity.FiniteTransfer.gramTensor line 23
theorem OAI.CircleDomainRigidity.FiniteTransfer.gramTensor_eq_sum line 27
theorem OAI.CircleDomainRigidity.FiniteTransfer.gramTensor_posSemidef line 33
theorem OAI.CircleDomainRigidity.FiniteTransfer.gramTensor_energy line 39

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_gramMetric_energy_lt line 49

Source documentation

Small pairwise wedge integrals give one positive definite metric with small total coordinate energy. All tensor and inverse formulas are derived.

theorem exists_gramMetric_energy_lt
    {X : Type*} [MeasurableSpace X] {μ : Measure X}
    (x y : ℕ → X → ℝ) (n : ℕ)
    (hx : ∀ i, Measurable (x i)) (hy : ∀ i, Measurable (y i))
    (htrace : Integrable (fun z => covectorTrace (fun i => x i z) (fun i => y i z) n) μ)
    (hwedge : Integrable (fun z => covectorWedges (fun i => x i z) (fun i => y i z) n) μ)
    {ε : ℝ} (hε : (∫ z, 2 * covectorWedges (fun i => x i z) (fun i => y i z) n ∂μ) < ε) :
    ∃ τ : ℝ, 0 < τ ∧
      (∀ z, (gramTensor (fun i => x i z) (fun i => y i z) n + τ • 1).PosDef) ∧
      (∫ z, Matrix.trace
        ((gramTensor (fun i => x i z) (fun i => y i z) n + τ • 1)⁻¹ *
          gramTensor (fun i => x i z) (fun i => y i z) n) *
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.covectorTrace, OAI.CircleDomainRigidity.FiniteTransfer.covectorWedges, OAI.CircleDomainRigidity.FiniteTransfer.gramTensor

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_smooth_gramMetric_on_bounded line 71

Source documentation

For smooth coordinate differentials on a bounded planar region, integrability is automatic and the chosen positive definite metric is itself smooth.

theorem exists_smooth_gramMetric_on_bounded
    (x y : ℕ → (ℝ × ℝ) → ℝ) (n : ℕ)
    (hx : ∀ i, ContDiff ℝ ∞ (x i)) (hy : ∀ i, ContDiff ℝ ∞ (y i))
    {S : Set (ℝ × ℝ)} (hS : Bornology.IsBounded S) {ε : ℝ}
    (hε : (∫ z in S, 2 * covectorWedges (fun i => x i z) (fun i => y i z) n) < ε) :
    ∃ τ : ℝ, 0 < τ ∧
      ContDiff ℝ ∞ (fun z => gramTensor (fun i => x i z) (fun i => y i z) n + τ • 1) ∧
      (∀ z, (gramTensor (fun i => x i z) (fun i => y i z) n + τ • 1).PosDef) ∧
      (∫ z in S, Matrix.trace
        ((gramTensor (fun i => x i z) (fun i => y i z) n + τ • 1)⁻¹ *
          gramTensor (fun i => x i z) (fun i => y i z) n) *
        Real.sqrt (gramTensor (fun i => x i z) (fun i => y i z) n + τ • 1).det) < ε := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.covectorWedges, OAI.CircleDomainRigidity.FiniteTransfer.gramTensor