LinePayment.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Energy paid by a line crossing a barrier

A barrier that is zero at an end of [-L, L] and equals one somewhere on the segment has squared derivative integral at least 1 / (2 * L). This follows from the fundamental theorem of calculus and the integral Cauchy–Schwarz inequality.

Both absolutely continuous and C¹ restrictions satisfy this estimate. Fubini's theorem gives the rectangular energy lower bound when horizontal slices are almost everywhere absolutely continuous.

theorem OAI.CircleDomainRigidity.integral_sq_le_length_mul_integral_sq line 28

Source documentation

Cauchy–Schwarz against the constant function on a finite interval, written without square roots.

theorem integral_sq_le_length_mul_integral_sq {g : ℝ → ℝ} {a b : ℝ}
    (hab : a ≤ b) (hg : IntervalIntegrable g volume a b)
    (hg2 : IntervalIntegrable (fun x => g x ^ 2) volume a b) :
    (∫ x in a..b, g x) ^ 2 ≤ (b - a) * (∫ x in a..b, g x ^ 2) := by
…

theorem OAI.CircleDomainRigidity.line_payment_of_hasDerivAt line 56

Source documentation

A continuous restriction with endpoint value zero and an interior or endpoint value one pays at least reciprocal interval length in squared derivative energy. The derivative need only exist in the open interval, and both integrability assumptions are ordinary FTC hypotheses.

theorem line_payment_of_hasDerivAt {f d : ℝ → ℝ} {a b c : ℝ}
    (hc : c ∈ Icc a b) (hf : ContinuousOn f (Icc a b))
    (hd : ∀ x ∈ Ioo a b, HasDerivAt f (d x) x)
    (hi : IntervalIntegrable d volume a b)
    (hi2 : IntervalIntegrable (fun x => d x ^ 2) volume a b)
    (ha : f a = 0) (hcone : f c = 1) :
    1 ≤ (b - a) * (∫ x in a..b, d x ^ 2) := by
…

theorem OAI.CircleDomainRigidity.line_payment_of_contDiff line 89
Source documentation
The smooth-barrier specialization needs no separate integrability hypotheses: continuity of the derivative on a compact interval supplies them.
```
theorem line_payment_of_contDiff {f : ℝ → ℝ} {a b c : ℝ}
    (hf : ContDiff ℝ 1 f) (hc : c ∈ Icc a b)
    (ha : f a = 0) (hcone : f c = 1) :
    1 ≤ (b - a) * (∫ x in a..b, deriv f x ^ 2) := by
…
```

theorem OAI.CircleDomainRigidity.line_payment_on_symmetric_interval line 100

Source documentation

The 1 / (2L) payment of a smooth barrier on a horizontal segment in the supporting square [-L,L]². Only the left endpoint value is needed.

theorem line_payment_on_symmetric_interval {f : ℝ → ℝ} {L c : ℝ}
    (hL : 0 < L) (hf : ContDiff ℝ 1 f) (hc : c ∈ Icc (-L) L)
    (ha : f (-L) = 0) (hcone : f c = 1) :
    1 / (2 * L) ≤ ∫ x in (-L)..L, deriv f x ^ 2 := by
…

theorem OAI.CircleDomainRigidity.line_payment_of_absolutelyContinuous line 111
Source documentation
The actual absolutely continuous case of the line-payment estimate. Absolute continuity supplies the integrable derivative and its fundamental theorem of calculus; only square-integrability is an extra energy hypothesis.
```
theorem line_payment_of_absolutelyContinuous {f : ℝ → ℝ} {a b c : ℝ}
    (hf : AbsolutelyContinuousOnInterval f a b) (hc : c ∈ Icc a b)
    (hi2 : IntervalIntegrable (fun x => deriv f x ^ 2) volume a b)
    (ha : f a = 0) (hcone : f c = 1) :
    1 ≤ (b - a) * (∫ x in a..b, deriv f x ^ 2) := by
…
```

theorem OAI.CircleDomainRigidity.line_payment_on_symmetric_interval_of_absolutelyContinuous line 138

Source documentation

The sharp form needed on each absolutely continuous horizontal slice of a Sobolev barrier supported in the square [-L,L]².

theorem line_payment_on_symmetric_interval_of_absolutelyContinuous
    {f : ℝ → ℝ} {L c : ℝ} (hL : 0 < L)
    (hf : AbsolutelyContinuousOnInterval f (-L) L) (hc : c ∈ Icc (-L) L)
    (hi2 : IntervalIntegrable (fun x => deriv f x ^ 2) volume (-L) L)
    (ha : f (-L) = 0) (hcone : f c = 1) :
    1 / (2 * L) ≤ ∫ x in (-L)..L, deriv f x ^ 2 := by
…

theorem OAI.CircleDomainRigidity.integrated_line_payment_of_absolutelyContinuous line 153

Source documentation

Integrating line payment over a transverse interval gives the energy lower bound (b-a)/(2L). The hypotheses are the actual ACL slice conditions and integrability of the squared horizontal derivative on the rectangle. Fubini supplies square-integrability on almost every slice and integrability of the resulting slice energies. Coordinates are written (y,x).

theorem integrated_line_payment_of_absolutelyContinuous
    {v : ℝ → ℝ → ℝ} {L a b : ℝ} (hL : 0 < L) (hab : a ≤ b)
    (hEnergy : Integrable (fun p : ℝ × ℝ => deriv (v p.1) p.2 ^ 2)
      ((volume.restrict (Ioc a b)).prod (volume.restrict (Ioc (-L) L))))
    (hSlices : ∀ᵐ y ∂volume.restrict (Ioc a b),
      AbsolutelyContinuousOnInterval (v y) (-L) L ∧ v y (-L) = 0 ∧
        ∃ c ∈ Icc (-L) L, v y c = 1) :
    (b - a) / (2 * L) ≤
      ∫ p : ℝ × ℝ, deriv (v p.1) p.2 ^ 2
        ∂((volume.restrict (Ioc a b)).prod (volume.restrict (Ioc (-L) L))) := by
…