English
If I.distortion ≤ c, then diam(Icc I) ≤ c · (I.upper i − I.lower i) for any i.
Русский
Если I.distortion ≤ c, то diam(Icc I) ≤ c · (I.upper i − I.lower i) для любого i.
LaTeX
$$$$\forall I,i,c,\; (I.distortion \le c) \Rightarrow diam(Box.Icc I) \le c \cdot (I.upper i - I.lower i).$$$$
Lean4
/-- Auxiliary lemma for the divergence theorem. -/
theorem norm_volume_sub_integral_face_upper_sub_lower_smul_le {f : (Fin (n + 1) → ℝ) → E}
{f' : (Fin (n + 1) → ℝ) →L[ℝ] E} (hfc : ContinuousOn f (Box.Icc I)) {x : Fin (n + 1) → ℝ} (hxI : x ∈ (Box.Icc I))
{a : E} {ε : ℝ} (h0 : 0 < ε) (hε : ∀ y ∈ (Box.Icc I), ‖f y - a - f' (y - x)‖ ≤ ε * ‖y - x‖) {c : ℝ≥0}
(hc : I.distortion ≤ c) :
‖(∏ j, (I.upper j - I.lower j)) • f' (Pi.single i 1) -
(integral (I.face i) ⊥ (f ∘ i.insertNth (α := fun _ ↦ ℝ) (I.upper i)) BoxAdditiveMap.volume -
integral (I.face i) ⊥ (f ∘ i.insertNth (α := fun _ ↦ ℝ) (I.lower i)) BoxAdditiveMap.volume)‖ ≤
2 * ε * c * ∏ j, (I.upper j - I.lower j) :=
by
-- Porting note: Lean fails to find `α` in the next line
set e : ℝ → (Fin n → ℝ) → (Fin (n + 1) → ℝ) :=
i.insertNth (α := fun _ ↦ ℝ)
/- **Plan of the proof**. The difference of the integrals of the affine function
`fun y ↦ a + f' (y - x)` over the faces `x i = I.upper i` and `x i = I.lower i` is equal to the
volume of `I` multiplied by `f' (Pi.single i 1)`, so it suffices to show that the integral of
`f y - a - f' (y - x)` over each of these faces is less than or equal to `ε * c * vol I`. We
integrate a function of the norm `≤ ε * diam I.Icc` over a box of volume
`∏ j ≠ i, (I.upper j - I.lower j)`. Since `diam I.Icc ≤ c * (I.upper i - I.lower i)`, we get the
required estimate. -/
have Hl : I.lower i ∈ Icc (I.lower i) (I.upper i) := Set.left_mem_Icc.2 (I.lower_le_upper i)
have Hu : I.upper i ∈ Icc (I.lower i) (I.upper i) := Set.right_mem_Icc.2 (I.lower_le_upper i)
have Hi : ∀ x ∈ Icc (I.lower i) (I.upper i), Integrable.{0, u, u} (I.face i) ⊥ (f ∘ e x) BoxAdditiveMap.volume :=
fun x hx => integrable_of_continuousOn _ (Box.continuousOn_face_Icc hfc hx) volume
have :
∀ y ∈ Box.Icc (I.face i),
‖f' (Pi.single i (I.upper i - I.lower i)) - (f (e (I.upper i) y) - f (e (I.lower i) y))‖ ≤
2 * ε * diam (Box.Icc I) :=
fun y hy ↦ by
set g := fun y => f y - a - f' (y - x) with hg
change ∀ y ∈ (Box.Icc I), ‖g y‖ ≤ ε * ‖y - x‖ at hε
clear_value g; obtain rfl : f = fun y => a + f' (y - x) + g y := by simp [hg]
convert_to ‖g (e (I.lower i) y) - g (e (I.upper i) y)‖ ≤ _
· congr 1
have := Fin.insertNth_sub_same (α := fun _ ↦ ℝ) i (I.upper i) (I.lower i) y
simp only [← this, f'.map_sub]; abel
· have : ∀ z ∈ Icc (I.lower i) (I.upper i), e z y ∈ (Box.Icc I) := fun z hz => I.mapsTo_insertNth_face_Icc hz hy
replace hε : ∀ y ∈ (Box.Icc I), ‖g y‖ ≤ ε * diam (Box.Icc I) :=
by
intro y hy
refine (hε y hy).trans (mul_le_mul_of_nonneg_left ?_ h0.le)
rw [← dist_eq_norm]
exact dist_le_diam_of_mem I.isCompact_Icc.isBounded hy hxI
rw [two_mul, add_mul]
exact norm_sub_le_of_le (hε _ (this _ Hl)) (hε _ (this _ Hu))
calc
‖(∏ j, (I.upper j - I.lower j)) • f' (Pi.single i 1) -
(integral (I.face i) ⊥ (f ∘ e (I.upper i)) BoxAdditiveMap.volume -
integral (I.face i) ⊥ (f ∘ e (I.lower i)) BoxAdditiveMap.volume)‖ =
‖integral.{0, u, u} (I.face i) ⊥
(fun x : Fin n → ℝ =>
f' (Pi.single i (I.upper i - I.lower i)) - (f (e (I.upper i) x) - f (e (I.lower i) x)))
BoxAdditiveMap.volume‖ :=
by
rw [← integral_sub (Hi _ Hu) (Hi _ Hl), ← Box.volume_face_mul i, mul_smul, ← Box.volume_apply, ←
BoxAdditiveMap.toSMul_apply, ← integral_const, ← BoxAdditiveMap.volume, ←
integral_sub (integrable_const _) ((Hi _ Hu).sub (Hi _ Hl))]
simp only [(· ∘ ·), Pi.sub_def, ← f'.map_smul, ← Pi.single_smul', smul_eq_mul, mul_one]
_ ≤ (volume (I.face i : Set (Fin n → ℝ))).toReal * (2 * ε * c * (I.upper i - I.lower i)) := by
-- The hard part of the estimate was done above, here we just replace `diam I.Icc`
-- with `c * (I.upper i - I.lower i)`
refine norm_integral_le_of_le_const (fun y hy => (this y hy).trans ?_) volume
rw [mul_assoc (2 * ε)]
gcongr
exact I.diam_Icc_le_of_distortion_le i hc
_ = 2 * ε * c * ∏ j, (I.upper j - I.lower j) :=
by
rw [← measureReal_def, ← Measure.toBoxAdditive_apply, Box.volume_apply, ← I.volume_face_mul i]
ac_rfl
