MetricIntegral.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Integrating the finite-transfer metric limit

The original trace bounds the regularized energy density uniformly. Dominated convergence therefore turns the scalar eigenvalue limit into the small-energy choice used in Step 5 of finite transfer. The eigenvalues need only be measurable with integrable trace; smooth compact pieces satisfy these hypotheses.

theorem OAI.CircleDomainRigidity.FiniteTransfer.measurable_metricEnergy line 22
Source documentation
Measurability of the regularized metric energy.
```
theorem measurable_metricEnergy {X : Type*} [MeasurableSpace X]
    {a b : X → ℝ} (ha : Measurable a) (hb : Measurable b) (τ : ℝ) :
    Measurable (fun x => metricEnergy (a x) (b x) τ) := by
…
```
Mentions: OAI.CircleDomainRigidity.FiniteTransfer.metricEnergy

theorem OAI.CircleDomainRigidity.FiniteTransfer.tendsto_integral_metricEnergy line 31

Source documentation

Dominated convergence for the optimized metric: the limiting total energy is twice the integral of the square root of the determinant.

theorem tendsto_integral_metricEnergy {X : Type*} [MeasurableSpace X]
    {μ : Measure X} {a b : X → ℝ} (ha : Measurable a) (hb : Measurable b)
    (ha0 : ∀ x, 0 ≤ a x) (hb0 : ∀ x, 0 ≤ b x)
    (htrace : Integrable (fun x => a x + b x) μ) :
    Tendsto (fun τ : ℝ => ∫ x, metricEnergy (a x) (b x) τ ∂μ) (𝓝[>] 0)
      (𝓝 (∫ x, 2 * Real.sqrt (a x * b x) ∂μ)) := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.metricEnergy

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_metricEnergy_integral_lt line 55

Source documentation

A sufficiently small positive regularization attains any strict upper bound for the limiting determinant integral.

theorem exists_metricEnergy_integral_lt {X : Type*} [MeasurableSpace X]
    {μ : Measure X} {a b : X → ℝ} (ha : Measurable a) (hb : Measurable b)
    (ha0 : ∀ x, 0 ≤ a x) (hb0 : ∀ x, 0 ≤ b x)
    (htrace : Integrable (fun x => a x + b x) μ) {ε : ℝ}
    (hε : (∫ x, 2 * Real.sqrt (a x * b x) ∂μ) < ε) :
    ∃ τ : ℝ, 0 < τ ∧ (∫ x, metricEnergy (a x) (b x) τ ∂μ) < ε := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.metricEnergy

theorem OAI.CircleDomainRigidity.FiniteTransfer.tendsto_integral_metricEnergy_rank_one line 67

Source documentation

On a rank-at-most-one piece, the total regularized energy tends to zero.

theorem tendsto_integral_metricEnergy_rank_one {X : Type*} [MeasurableSpace X]
    {μ : Measure X} {a b : X → ℝ} (ha : Measurable a) (hb : Measurable b)
    (ha0 : ∀ x, 0 ≤ a x) (hb0 : ∀ x, 0 ≤ b x)
    (htrace : Integrable (fun x => a x + b x) μ) (hrank : ∀ x, a x * b x = 0) :
    Tendsto (fun τ : ℝ => ∫ x, metricEnergy (a x) (b x) τ ∂μ) (𝓝[>] 0) (𝓝 0) := by
…

Mentions: OAI.CircleDomainRigidity.FiniteTransfer.metricEnergy