English
For any i, nndist I.lower I.upper ≤ I.distortion · nndist(I.lower i) (I.upper i).
Русский
Для любой координаты i имеет место неравенство nndist(I.lower, I.upper) ≤ I.distortion · nndist(I.lower i, I.upper i).
LaTeX
$$$$\forall I,i,\; nndist(I.lower,I.upper) \le I.distortion \cdot nndist(I.lower(i),I.upper(i)).$$$$
Lean4
/-- If `f : ℝⁿ⁺¹ → E` is differentiable on a closed rectangular box `I` with derivative `f'`, then
the partial derivative `fun x ↦ f' x (Pi.single i 1)` is Henstock-Kurzweil integrable with integral
equal to the difference of integrals of `f` over the faces `x i = I.upper i` and `x i = I.lower i`.
More precisely, we use a non-standard generalization of the Henstock-Kurzweil integral and
we allow `f` to be non-differentiable (but still continuous) at a countable set of points.
TODO: If `n > 0`, then the condition at `x ∈ s` can be replaced by a much weaker estimate but this
requires either better integrability theorems, or usage of a filter depending on the countable set
`s` (we need to ensure that none of the faces of a partition contain a point from `s`). -/
theorem hasIntegral_GP_pderiv (f : (Fin (n + 1) → ℝ) → E) (f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E)
(s : Set (Fin (n + 1) → ℝ)) (hs : s.Countable) (Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x)
(Hd : ∀ x ∈ (Box.Icc I) \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x) (i : Fin (n + 1)) :
HasIntegral.{0, u, u} I GP (fun x => f' x (Pi.single i 1)) BoxAdditiveMap.volume
(integral.{0, u, u} (I.face i) GP (fun x => f (i.insertNth (I.upper i) x)) BoxAdditiveMap.volume -
integral.{0, u, u} (I.face i) GP (fun x => f (i.insertNth (I.lower i) x)) BoxAdditiveMap.volume) :=
by
/- Note that `f` is continuous on `I.Icc`, hence it is integrable on the faces of all boxes
`J ≤ I`, thus the difference of integrals over `x i = J.upper i` and `x i = J.lower i` is a
box-additive function of `J ≤ I`. -/
have Hc : ContinuousOn f (Box.Icc I) := fun x hx ↦
by
by_cases hxs : x ∈ s
exacts [Hs x hxs, (Hd x ⟨hx, hxs⟩).continuousWithinAt]
set fI : ℝ → Box (Fin n) → E := fun y J =>
integral.{0, u, u} J GP (fun x => f (i.insertNth y x)) BoxAdditiveMap.volume
set fb : Icc (I.lower i) (I.upper i) → Fin n →ᵇᵃ[↑(I.face i)] E := fun x =>
(integrable_of_continuousOn GP (Box.continuousOn_face_Icc Hc x.2) volume).toBoxAdditive
set F : Fin (n + 1) →ᵇᵃ[I] E := BoxAdditiveMap.upperSubLower I i fI fb fun x _ J => rfl
change HasIntegral I GP (fun x => f' x (Pi.single i 1)) _ (F I)
refine HasIntegral.of_le_Henstock_of_forall_isLittleO gp_le ?_ ?_ _ s hs ?_ ?_
· -- We use the volume as an upper estimate.
exact (volume : Measure (Fin (n + 1) → ℝ)).toBoxAdditive.restrict _ le_top
· exact fun J => ENNReal.toReal_nonneg
· intro c x hx ε ε0
have :
∀ᶠ δ in 𝓝[>] (0 : ℝ),
δ ∈ Ioc (0 : ℝ) (1 / 2) ∧
(∀ᵉ (y₁ ∈ closedBall x δ ∩ (Box.Icc I)) (y₂ ∈ closedBall x δ ∩ (Box.Icc I)), ‖f y₁ - f y₂‖ ≤ ε / 2) ∧
(2 * δ) ^ (n + 1) * ‖f' x (Pi.single i 1)‖ ≤ ε / 2 :=
by
refine .and (Ioc_mem_nhdsGT one_half_pos) (.and ?_ ?_)
· rcases
((nhdsWithin_hasBasis nhds_basis_closedBall _).tendsto_iff nhds_basis_closedBall).1 (Hs x hx.2) _
(half_pos <| half_pos ε0) with
⟨δ₁, δ₁0, hδ₁⟩
filter_upwards [Ioc_mem_nhdsGT δ₁0] with δ hδ y₁ hy₁ y₂ hy₂
have : closedBall x δ ∩ (Box.Icc I) ⊆ closedBall x δ₁ ∩ (Box.Icc I) := by gcongr; exact hδ.2
rw [← dist_eq_norm]
calc
dist (f y₁) (f y₂) ≤ dist (f y₁) (f x) + dist (f y₂) (f x) := dist_triangle_right _ _ _
_ ≤ ε / 2 / 2 + ε / 2 / 2 := (add_le_add (hδ₁ _ <| this hy₁) (hδ₁ _ <| this hy₂))
_ = ε / 2 := add_halves _
· have : ContinuousWithinAt (fun δ : ℝ => (2 * δ) ^ (n + 1) * ‖f' x (Pi.single i 1)‖) (Ioi 0) 0 :=
((continuousWithinAt_id.const_mul _).pow _).mul_const _
refine this.eventually (ge_mem_nhds ?_)
simpa using half_pos ε0
rcases this.exists with ⟨δ, ⟨hδ0, hδ12⟩, hdfδ, hδ⟩
refine ⟨δ, hδ0, fun J hJI hJδ _ _ => add_halves ε ▸ ?_⟩
have Hl : J.lower i ∈ Icc (J.lower i) (J.upper i) := Set.left_mem_Icc.2 (J.lower_le_upper i)
have Hu : J.upper i ∈ Icc (J.lower i) (J.upper i) := Set.right_mem_Icc.2 (J.lower_le_upper i)
have Hi :
∀ x ∈ Icc (J.lower i) (J.upper i),
Integrable.{0, u, u} (J.face i) GP (fun y => f (i.insertNth x y)) BoxAdditiveMap.volume :=
fun x hx => integrable_of_continuousOn _ (Box.continuousOn_face_Icc (Hc.mono <| Box.le_iff_Icc.1 hJI) hx) volume
have hJδ' : Box.Icc J ⊆ closedBall x δ ∩ (Box.Icc I) := subset_inter hJδ (Box.le_iff_Icc.1 hJI)
have Hmaps :
∀ z ∈ Icc (J.lower i) (J.upper i), MapsTo (i.insertNth z) (Box.Icc (J.face i)) (closedBall x δ ∩ (Box.Icc I)) :=
fun z hz => (J.mapsTo_insertNth_face_Icc hz).mono Subset.rfl hJδ'
simp only [dist_eq_norm]; dsimp [F]
rw [← integral_sub (Hi _ Hu) (Hi _ Hl)]
refine (norm_sub_le _ _).trans (add_le_add ?_ ?_)
· simp_rw [BoxAdditiveMap.volume_apply, norm_smul, Real.norm_eq_abs, abs_prod]
refine (mul_le_mul_of_nonneg_right ?_ <| norm_nonneg _).trans hδ
have : ∀ j, |J.upper j - J.lower j| ≤ 2 * δ := fun j ↦
calc
dist (J.upper j) (J.lower j) ≤ dist J.upper J.lower := dist_le_pi_dist _ _ _
_ ≤ dist J.upper x + dist J.lower x := (dist_triangle_right _ _ _)
_ ≤ δ + δ := (add_le_add (hJδ J.upper_mem_Icc) (hJδ J.lower_mem_Icc))
_ = 2 * δ := (two_mul δ).symm
calc
∏ j, |J.upper j - J.lower j| ≤ ∏ j : Fin (n + 1), 2 * δ :=
prod_le_prod (fun _ _ => abs_nonneg _) fun j _ => this j
_ = (2 * δ) ^ (n + 1) := by simp
· refine (norm_integral_le_of_le_const (fun y hy => hdfδ _ (Hmaps _ Hu hy) _ (Hmaps _ Hl hy)) volume).trans ?_
refine (mul_le_mul_of_nonneg_right ?_ (half_pos ε0).le).trans_eq (one_mul _)
rw [Box.coe_eq_pi, measureReal_def, Real.volume_pi_Ioc_toReal (Box.lower_le_upper _)]
refine prod_le_one (fun _ _ => sub_nonneg.2 <| Box.lower_le_upper _ _) fun j _ => ?_
calc
J.upper (i.succAbove j) - J.lower (i.succAbove j) ≤ dist (J.upper (i.succAbove j)) (J.lower (i.succAbove j)) :=
le_abs_self _
_ ≤ dist J.upper J.lower := (dist_le_pi_dist J.upper J.lower (i.succAbove j))
_ ≤ dist J.upper x + dist J.lower x := (dist_triangle_right _ _ _)
_ ≤ δ + δ := (add_le_add (hJδ J.upper_mem_Icc) (hJδ J.lower_mem_Icc))
_ ≤ 1 / 2 + 1 / 2 := by gcongr
_ = 1 := add_halves 1
· intro c x hx ε ε0
rcases exists_pos_mul_lt ε0 (2 * c) with ⟨ε', ε'0, hlt⟩
rcases (nhdsWithin_hasBasis nhds_basis_closedBall _).mem_iff.1 ((Hd x hx).isLittleO.def ε'0) with ⟨δ, δ0, Hδ⟩
refine ⟨δ, δ0, fun J hle hJδ hxJ hJc => ?_⟩
simp only [BoxAdditiveMap.volume_apply, dist_eq_norm]
refine
(norm_volume_sub_integral_face_upper_sub_lower_smul_le _ (Hc.mono <| Box.le_iff_Icc.1 hle) hxJ ε'0
(fun y hy => Hδ ?_) (hJc rfl)).trans
?_
· exact ⟨hJδ hy, Box.le_iff_Icc.1 hle hy⟩
· rw [mul_right_comm (2 : ℝ), ← Box.volume_apply]
exact mul_le_mul_of_nonneg_right hlt.le ENNReal.toReal_nonneg
