English
A broad, elaborated induction principle for boxes: predicates on boxes are provable by iterating center splits with controlled subboxes and nhds-based conditions.
Русский
Обобщённый принцип индукции по подBoxes: утверждения о коробках доказываются усовершенствованием разбиений по центру с контролируемыми подBox и условиями в окрестностях.
LaTeX
$$$$\text{Let } p: Box ι \to Prop. \text{If appropriate induction and nhds hypotheses hold, then } p(I).$$$$
Lean4
/-- Let `p` be a predicate on `Box ι`, let `I` be a box. Suppose that the following two properties
hold true.
* `H_ind` : Consider a smaller box `J ≤ I`. The hyperplanes passing through the center of `J` split
it into `2 ^ n` boxes. If `p` holds true on each of these boxes, then it true on `J`.
* `H_nhds` : For each `z` in the closed box `I.Icc` there exists a neighborhood `U` of `z` within
`I.Icc` such that for every box `J ≤ I` such that `z ∈ J.Icc ⊆ U`, if `J` is homothetic to `I`
with a coefficient of the form `1 / 2 ^ m`, then `p` is true on `J`.
Then `p I` is true. See also `BoxIntegral.Box.subbox_induction_on` for a version using
`BoxIntegral.Prepartition.splitCenter` instead of `BoxIntegral.Box.splitCenterBox`.
The proof still works if we assume `H_ind` only for subboxes `J ≤ I` that are homothetic to `I` with
a coefficient of the form `2⁻ᵐ` but we do not need this generalization yet. -/
@[elab_as_elim]
theorem subbox_induction_on' {p : Box ι → Prop} (I : Box ι) (H_ind : ∀ J ≤ I, (∀ s, p (splitCenterBox J s)) → p J)
(H_nhds :
∀ z ∈ Box.Icc I,
∃ U ∈ 𝓝[Box.Icc I] z,
∀ J ≤ I,
∀ (m : ℕ),
z ∈ Box.Icc J → Box.Icc J ⊆ U → (∀ i, J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) → p J) :
p I := by
by_contra hpI
replace H_ind := fun J hJ ↦ not_imp_not.2 (H_ind J hJ)
simp only [not_forall] at H_ind
choose! s hs using H_ind
set J : ℕ → Box ι := fun m ↦ (fun J ↦ splitCenterBox J (s J))^[m] I
have J_succ : ∀ m, J (m + 1) = splitCenterBox (J m) (s <| J m) := fun m ↦
iterate_succ_apply' _ _
_
-- Now we prove some properties of `J`
have hJmono : Antitone J := antitone_nat_of_succ_le fun n ↦ by simpa [J_succ] using splitCenterBox_le _ _
have hJle (m) : J m ≤ I := hJmono (zero_le m)
have hJp (m) : ¬p (J m) := Nat.recOn m hpI fun m ↦ by simpa only [J_succ] using hs (J m) (hJle m)
have hJsub (m i) : (J m).upper i - (J m).lower i = (I.upper i - I.lower i) / 2 ^ m := by
induction m with
| zero => simp [J]
| succ m ihm => simp only [pow_succ, J_succ, upper_sub_lower_splitCenterBox, ihm, div_div]
have h0 : J 0 = I := rfl
clear_value J
clear hpI hs J_succ s
set z : ι → ℝ := ⨆ m, (J m).lower
have hzJ : ∀ m, z ∈ Box.Icc (J m) :=
mem_iInter.1
(ciSup_mem_iInter_Icc_of_antitone_Icc ((@Box.Icc ι).monotone.comp_antitone hJmono) fun m ↦ (J m).lower_le_upper)
have hJl_mem : ∀ m, (J m).lower ∈ Box.Icc I := fun m ↦ le_iff_Icc.1 (hJle m) (J m).lower_mem_Icc
have hJu_mem : ∀ m, (J m).upper ∈ Box.Icc I := fun m ↦ le_iff_Icc.1 (hJle m) (J m).upper_mem_Icc
have hJlz : Tendsto (fun m ↦ (J m).lower) atTop (𝓝 z) :=
tendsto_atTop_ciSup (antitone_lower.comp hJmono) ⟨I.upper, fun x ⟨m, hm⟩ ↦ hm ▸ (hJl_mem m).2⟩
have hJuz : Tendsto (fun m ↦ (J m).upper) atTop (𝓝 z) :=
by
suffices Tendsto (fun m ↦ (J m).upper - (J m).lower) atTop (𝓝 0) by simpa using hJlz.add this
refine tendsto_pi_nhds.2 fun i ↦ ?_
simpa [hJsub] using tendsto_const_nhds.div_atTop (tendsto_pow_atTop_atTop_of_one_lt _root_.one_lt_two)
replace hJlz : Tendsto (fun m ↦ (J m).lower) atTop (𝓝[Icc I.lower I.upper] z) :=
tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hJlz (Eventually.of_forall hJl_mem)
replace hJuz : Tendsto (fun m ↦ (J m).upper) atTop (𝓝[Icc I.lower I.upper] z) :=
tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hJuz (Eventually.of_forall hJu_mem)
rcases H_nhds z (h0 ▸ hzJ 0) with ⟨U, hUz, hU⟩
rcases (tendsto_lift'.1 (hJlz.Icc hJuz) U hUz).exists with ⟨m, hUm⟩
exact hJp m (hU (J m) (hJle m) m (hzJ m) hUm (hJsub m))
