English
Define a box-additive map on a higher-dimensional box by looking at differences on the upper and lower faces of a fixed coordinate.
Русский
Определение box-additive map на более высокой коробке через разности по лицам верхней и нижней граней по фиксированной координате.
LaTeX
$$$\text{upperSubLower} : \dots$$$
Lean4
/-- Given a box `I₀` in `ℝⁿ⁺¹`, `f x : Box (Fin n) → G` is a family of functions indexed by a real
`x` and for `x ∈ [I₀.lower i, I₀.upper i]`, `f x` is box-additive on subboxes of the `i`-th face of
`I₀`, then `fun J ↦ f (J.upper i) (J.face i) - f (J.lower i) (J.face i)` is box-additive on subboxes
of `I₀`. -/
@[simps!]
def upperSubLower.{u} {G : Type u} [AddCommGroup G] (I₀ : Box (Fin (n + 1))) (i : Fin (n + 1)) (f : ℝ → Box (Fin n) → G)
(fb : Icc (I₀.lower i) (I₀.upper i) → Fin n →ᵇᵃ[I₀.face i] G)
(hf : ∀ (x) (hx : x ∈ Icc (I₀.lower i) (I₀.upper i)) (J), f x J = fb ⟨x, hx⟩ J) : Fin (n + 1) →ᵇᵃ[I₀] G :=
ofMapSplitAdd (fun J : Box (Fin (n + 1)) => f (J.upper i) (J.face i) - f (J.lower i) (J.face i)) I₀
(by
intro J hJ j x
rw [WithTop.coe_le_coe] at hJ
refine i.succAboveCases (fun hx => ?_) (fun j hx => ?_) j
· simp only [Box.splitLower_def hx, Box.splitUpper_def hx, update_self, ← WithBot.some_eq_coe, Option.elim',
Box.face, Function.comp_def, update_of_ne (Fin.succAbove_ne _ _)]
abel
· have : (J.face i : WithTop (Box (Fin n))) ≤ I₀.face i := WithTop.coe_le_coe.2 (face_mono hJ i)
rw [le_iff_Icc, @Box.Icc_eq_pi _ I₀] at hJ
simp only
rw [hf _ (hJ J.upper_mem_Icc _ trivial), hf _ (hJ J.lower_mem_Icc _ trivial), ← (fb _).map_split_add this j x, ←
(fb _).map_split_add this j x]
have hx' : x ∈ Ioo ((J.face i).lower j) ((J.face i).upper j) := hx
simp only [Box.splitLower_def hx, Box.splitUpper_def hx, Box.splitLower_def hx', Box.splitUpper_def hx',
← WithBot.some_eq_coe, Option.elim', Box.face_mk, update_of_ne (Fin.succAbove_ne _ _).symm, sub_add_sub_comm,
update_comp_eq_of_injective _ (Fin.strictMono_succAbove i).injective j x, ← hf]
simp only [Box.face])
