Theillière's corrugation operation

This files introduces the fundamental calculus tool of convex integration. The version of convex integration that we formalize is Theillière's corrugation-based convex integration. It improves a map f : E → F by adding to it some corrugation map fun x ↦ (1/N) • ∫ t in 0..(N*π x), (γ x t - (γ x).average) where γ is a family of loops in F parametrized by E and N is some (very large) real number.

Under the assumption that ∀ x, (γ x).average = D f x p.v for some dual pair p, this improved map will have a derivative which is almost a value of γ x in direction p.v and almost the derivative of f in direction ker p.π. More precisely, its derivative will be almost p.update (D f x) (γ x (N*p.π x)). In addition the improved map will be very close to f in C⁰ topology. All those "almost" and "very close" refer to the asymptotic behavior when N is very large.

The main definition is corrugation. The main results are:

• fderiv_corrugated_map computing the difference between D (f + corrugation p.π N γ) x and p.update (D f x) (γ x (N*p.π x)) + corrugation.remainder p.π N γ x
• remainder_c0_small_on saying this difference is very small
• corrugation.c0_small_on saying that corrugations are C⁰-small

noncomputable def corrugation {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (π : E →L[ℝ] ℝ) (N : ℝ) (γ : E → Loop F) : E → F

Theillière's corrugations.

Equations

• corrugation π N γ x = (1 / N) • ∫ (t : ℝ) in 0..N * π x, ↑(γ x) t - (γ x).average

theorem per_corrugation {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] (γ : Loop F) (hγ : ∀ (s t : ℝ), IntervalIntegrable (↑γ) MeasureTheory.volume s t) : OnePeriodic fun (s : ℝ) => ∫ (t : ℝ) in 0..s, ↑γ t - γ.average

The integral appearing in corrugations is periodic.

@[simp]

theorem corrugation_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {π : E →L[ℝ] ℝ} (N : ℝ) (γ : E → Loop F) {x : E} (h : (γ x).IsConst) : corrugation π N γ x = 0

theorem corrugation.support {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] (π : E →L[ℝ] ℝ) (N : ℝ) (γ : E → Loop F) : Function.support (corrugation π N γ) ⊆ Loop.support γ

theorem corrugation_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] (π : E →L[ℝ] ℝ) (N : ℝ) (γ : E → Loop F) (x : E) (H : x ∉ Loop.support γ) : corrugation π N γ x = 0

theorem corrugation.c0_small_on {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] (π : E →L[ℝ] ℝ) {γ : ℝ → E → Loop F} {K : Set E} (hK : IsCompact K) (h_le : ∀ (x : E), ∀ t ≤ 0, γ t x = γ 0 x) (h_ge : ∀ (x : E), ∀ t ≥ 1, γ t x = γ 1 x) (hγ_cont : Continuous ↿γ) {ε : ℝ} (ε_pos : 0 < ε) : ∀ᶠ (N : ℝ) in Filter.atTop, ∀ x ∈ K, ∀ (t : ℝ), ‖corrugation π N (γ t) x‖ < ε

theorem corrugation.contDiff' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {H : Type u_4} [NormedAddCommGroup H] [NormedSpace ℝ H] [FiniteDimensional ℝ H] (π : E →L[ℝ] ℝ) (N : ℝ) {n : ℕ∞} {γ : G → E → Loop F} (hγ_diff : 𝒞 ↑n ↿γ) {x : H → E} (hx : 𝒞 (↑n) x) {g : H → G} (hg : 𝒞 (↑n) g) : 𝒞 ↑n fun (h : H) => corrugation π N (γ (g h)) (x h)

theorem corrugation.contDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] (π : E →L[ℝ] ℝ) (N : ℝ) {γ : E → Loop F} [FiniteDimensional ℝ E] {n : ℕ∞} (hγ_diff : 𝒞 ↑n ↿γ) : 𝒞 (↑n) (corrugation π N γ)

def «term∂₁» : Lean.ParserDescr

Equations

• «term∂₁» = Lean.ParserDescr.node `«term∂₁» 1024 (Lean.ParserDescr.symbol "∂₁")

noncomputable def corrugation.remainder {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (π : E → ℝ) (N : ℝ) (γ : E → Loop F) : E → E →L[ℝ] F

The remainder appearing when differentiating a corrugation.

Equations

• corrugation.remainder π N γ x = (1 / N) • ∫ (t : ℝ) in 0..N * π x, ∂₁ (fun (x : E) (t : ℝ) => ↑(γ x).normalize t) x t

theorem remainder_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] (π : E →L[ℝ] ℝ) [FiniteDimensional ℝ E] (N : ℝ) {γ : E → Loop F} (h : 𝒞 1 ↿γ) : corrugation.remainder (⇑π) N γ = fun (x : E) => (1 / N) • ∫ (t : ℝ) in 0..N * π x, ↑(Loop.diff γ x).normalize t

theorem remainder_eq_corrugation {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] (π : E →L[ℝ] ℝ) [FiniteDimensional ℝ E] (N : ℝ) {γ : E → Loop F} (h : 𝒞 1 ↿γ) : corrugation.remainder (⇑π) N γ = corrugation π N fun (x : E) => Loop.diff γ x

@[simp]

theorem remainder_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] (π : E →L[ℝ] ℝ) [FiniteDimensional ℝ E] (N : ℝ) {γ : E → Loop F} (h : 𝒞 1 ↿γ) {x : E} (hx : x ∉ Loop.support γ) : corrugation.remainder (⇑π) N γ x = 0

theorem corrugation.fderiv_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] (π : E →L[ℝ] ℝ) {γ : E → Loop F} [FiniteDimensional ℝ E] {N : ℝ} (hN : N ≠ 0) (hγ_diff : 𝒞 1 ↿γ) : D (corrugation π N γ) = fun (x : E) => ((↑(γ x) (N * π x) - (γ x).average) ⬝ π) + remainder (⇑π) N γ x

theorem corrugation.fderiv_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] (π : E →L[ℝ] ℝ) (N : ℝ) {γ : E → Loop F} [FiniteDimensional ℝ E] (hN : N ≠ 0) (hγ_diff : 𝒞 1 ↿γ) (x v : E) : (D (corrugation π N γ) x) v = π v • (↑(γ x) (N * π x) - (γ x).average) + (remainder (⇑π) N γ x) v

theorem fderiv_corrugated_map {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] (N : ℝ) {γ : E → Loop F} [FiniteDimensional ℝ E] (hN : N ≠ 0) (hγ_diff : 𝒞 1 ↿γ) {f : E → F} (hf : 𝒞 1 f) (p : DualPair E) {x : E} (hfγ : (γ x).average = (D f x) p.v) : D (f + corrugation p.π N γ) x = p.update (D f x) (↑(γ x) (N * p.π x)) + corrugation.remainder (⇑p.π) N γ x

theorem Remainder.smooth {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {H : Type u_4} [NormedAddCommGroup H] [NormedSpace ℝ H] [FiniteDimensional ℝ H] (π : E →L[ℝ] ℝ) (N : ℝ) [FiniteDimensional ℝ E] {γ : G → E → Loop F} (hγ_diff : 𝒞 ↑⊤ ↿γ) {x : H → E} (hx : 𝒞 (↑⊤) x) {g : H → G} (hg : 𝒞 (↑⊤) g) : 𝒞 ↑⊤ fun (h : H) => corrugation.remainder (⇑π) N (γ (g h)) (x h)

theorem remainder_c0_small_on {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] (π : E →L[ℝ] ℝ) {γ : E → Loop F} [FiniteDimensional ℝ E] {K : Set E} (hK : IsCompact K) (hγ_diff : 𝒞 1 ↿γ) {ε : ℝ} (ε_pos : 0 < ε) : ∀ᶠ (N : ℝ) in Filter.atTop, ∀ x ∈ K, ‖corrugation.remainder (⇑π) N γ x‖ < ε