Stat.Nonparametric.Approximation.Holder

lemma volume_supBall {d : ℕ} (x0 : Fin d → ℝ) (r : ℝ) : volume (supBall x0 r) = ofReal (2 * r) ^ d := by rw [supBall_eq_pi, Set.pi_univ_Icc, Real.volume_Icc_pi] simp_rw [show ∀ i : Fin d, x0 i + r - (x0 i - r) = 2 * r from fun i => by ring] simp

theorem exists_holderBallStd_extension (d : ℕ) (β : ℝ) (hβ : 0 < β) : ∃ A : ℝ, 0 < A ∧ ∀ (u : (Fin d → ℝ) → ℝ) (L : ℝ), 0 ≤ L → CubeHolderBall d (⌈β⌉₊ - 1) (β - ((⌈β⌉₊ - 1 : ℕ) : ℝ)) L u → ∃ U : (Fin d → ℝ) → ℝ, EqOn U u (cube d) ∧ HolderBallStd U β (A * L) (cube d) := by have hceil : 1 ≤ ⌈β⌉₊ := Nat.one_le_ceil_iff.mpr hβ have hcast : ((⌈β⌉₊ - 1 : ℕ) : ℝ) = (⌈β⌉₊ : ℝ) - 1 := by rw [Nat.cast_sub hceil, Nat.cast_one] have hs : 0 < β - ((⌈β⌉₊ - 1 : ℕ) : ℝ) := by rw [hcast] linarith [Nat.ceil_lt_add_one hβ.le] have hs1 : β - ((⌈β⌉₊ - 1 : ℕ) : ℝ) ≤ 1 := by rw [hcast] linarith [Nat.le_ceil β] obtain ⟨A, hA, hExt⟩ := exists_global_holder_extension d (⌈β⌉₊ - 1) (β - ((⌈β⌉₊ - 1 : ℕ) : ℝ)) hs hs1 refine ⟨A, hA, ?_⟩ intro u L hL hu obtain ⟨U, hEq, hSmooth, hBounds, hMod⟩ := hExt u L hL hu refine ⟨U, hEq, ?_⟩ exact ⟨hSmooth.contDiffOn, (fun j hj x hx => hBounds j hj x), (fun x hx y hy => hMod x y)⟩

lemma holder_line_taylor {d : ℕ} {γ M : ℝ} {g : (Fin d → ℝ) → ℝ} {S U : Set (Fin d → ℝ)} (hγ : 0 < γ) (hg : HolderBallStd g γ M S) (hU : IsOpen U) (hUS : U ⊆ S) (x0 y : Fin d → ℝ) (hseg : ∀ t ∈ Icc (0 : ℝ) 1, x0 + t • y ∈ U) : |g (x0 + y) - ∑ j ∈ range (⌈γ⌉₊ - 1 + 1), (1 / (Nat.factorial j : ℝ)) * iteratedFDeriv ℝ j g x0 (fun _ => y)| ≤ (M / (Nat.factorial (⌈γ⌉₊ - 1) : ℝ)) * ‖y‖ ^ γ := by have h0mem : x0 ∈ U := by have := hseg 0 (Set.left_mem_Icc.mpr zero_le_one); simpa using this have h1mem : x0 + y ∈ U := by have := hseg 1 (Set.right_mem_Icc.mpr zero_le_one); simpa using this have hx0S : x0 ∈ S := hUS h0mem have hx0yS : x0 + y ∈ S := hUS h1mem rcases Nat.eq_zero_or_pos (⌈γ⌉₊ - 1) with hm0 | hmpos · -- Case m = 0 (0 < γ ≤ 1): the sum is just `g x0`, no Taylor needed. have hb := holder_diag_diff_le hg (x0 + y) x0 hx0yS hx0S y rw [hm0] at hb ⊢ simp only [zero_add, Finset.sum_range_one, Nat.factorial_zero, Nat.cast_one, one_div, inv_one, one_mul, iteratedFDeriv_zero_apply, div_one, Nat.cast_zero, sub_zero, pow_zero, mul_one] at hb ⊢ rwa [add_sub_cancel_left] at hb · -- Case m ≥ 1 (γ > 1): Taylor with Lagrange remainder on the line. obtain ⟨n, hn⟩ : ∃ n, ⌈γ⌉₊ - 1 = n + 1 := ⟨⌈γ⌉₊ - 2, by omega⟩ have hM : 0 ≤ M := le_trans (norm_nonneg _) (hg.2.1 0 (zero_le _) x0 hx0S) have hfac : (0 : ℝ) < (Nat.factorial (n + 1) : ℝ) := by exact_mod_cast Nat.factorial_pos (n + 1) set K : Set (Fin d → ℝ) := (fun t : ℝ => x0 + t • y) '' Icc 0 1 with hKdef have hcontLine : Continuous (fun t : ℝ => x0 + t • y) := by fun_prop have hK : IsCompact K := isCompact_Icc.image hcontLine have hKU : K ⊆ U := by rintro _ ⟨t, ht, rfl⟩; exact hseg t ht have hx0K : x0 ∈ K := ⟨0, Set.left_mem_Icc.mpr zero_le_one, by simp⟩ have hx0yK : x0 + y ∈ K := ⟨1, Set.right_mem_Icc.mpr zero_le_one, by simp⟩ have hxξK : ∀ ξ : ℝ, ξ ∈ Ioo (0 : ℝ) 1 → x0 + ξ • y ∈ K := fun ξ hξ => ⟨ξ, ⟨hξ.1.le, hξ.2.le⟩, rfl⟩ obtain ⟨gt, hgt_cd, hgt_eq⟩ := exists_global_contDiff_of_contDiffOn (⌈γ⌉₊ - 1) hg.1 hU hUS hK hKU have htrans : ∀ (i : ℕ) (p : Fin d → ℝ), p ∈ K → iteratedFDeriv ℝ i gt p = iteratedFDeriv ℝ i g p := fun i p hp => ((hgt_eq p hp).iteratedFDeriv ℝ i).eq_of_nhds have hlineCD : ContDiff ℝ ((⌈γ⌉₊ - 1 : ℕ) : WithTop ℕ∞) (fun s : ℝ => x0 + s • y) := by fun_prop set φ : ℝ → ℝ := fun s => gt (x0 + s • y) with hφdef have hφCD : ContDiff ℝ ((⌈γ⌉₊ - 1 : ℕ) : WithTop ℕ∞) φ := by simpa [hφdef, Function.comp_def] using hgt_cd.comp hlineCD have hcoef : ∀ k : ℕ, k ≤ ⌈γ⌉₊ - 1 → iteratedDerivWithin k φ (Icc (0 : ℝ) 1) 0 = iteratedFDeriv ℝ k g x0 (fun _ => y) := by intro k hk have hCDk : ContDiff ℝ (k : WithTop ℕ∞) gt := hgt_cd.of_le (natCast_le_withTop hk) have hCDkφ : ContDiffAt ℝ (k : WithTop ℕ∞) φ 0 := (hφCD.of_le (natCast_le_withTop hk)).contDiffAt rw [iteratedDerivWithin_eq_iteratedDeriv uniqueDiffOn_Icc_zero_one hCDkφ (Set.left_mem_Icc.mpr zero_le_one), hφdef, line_iteratedDeriv gt k hCDk x0 y 0] simp only [zero_smul, add_zero] rw [htrans k x0 hx0K] have hCDgt : ContDiff ℝ ((n + 1 : ℕ) : WithTop ℕ∞) gt := hn ▸ hgt_cd have hφn : ContDiffOn ℝ (n : WithTop ℕ∞) φ (Icc (0 : ℝ) 1) := ((hn ▸ hφCD).of_le (natCast_le_withTop (le_succ n))).contDiffOn have hφn1 : ContDiffOn ℝ ((n + 1 : ℕ) : WithTop ℕ∞) φ (Icc (0 : ℝ) 1) := (hn ▸ hφCD).contDiffOn have hf' : DifferentiableOn ℝ (iteratedDerivWithin n φ (Icc (0 : ℝ) 1)) (Ioo 0 1) := (hφn1.differentiableOn_iteratedDerivWithin (natCast_lt_withTop (lt_succ_self n)) uniqueDiffOn_Icc_zero_one).mono Set.Ioo_subset_Icc_self have huIcc01 : uIcc (0 : ℝ) 1 = Icc (0 : ℝ) 1 := Set.uIcc_of_le zero_le_one have huIoo01 : Set.uIoo (0 : ℝ) 1 = Ioo (0 : ℝ) 1 := Set.uIoo_of_le zero_le_one obtain ⟨ξ, hξ, htay⟩ := taylor_mean_remainder_lagrange (f := φ) (x₀ := (0 : ℝ)) (x := (1 : ℝ)) (zero_ne_one) (by rw [huIcc01]; exact hφn) (by rw [huIcc01, huIoo01]; exact hf') rw [huIcc01] at htay rw [huIoo01] at hξ have hφ1 : φ 1 = g (x0 + y) := by have := (hgt_eq (x0 + y) hx0yK).eq_of_nhds; simpa [hφdef, one_smul] using this have hsum : taylorWithinEval φ n (Icc (0 : ℝ) 1) 0 1 = ∑ k ∈ range (n + 1), 1 / (Nat.factorial k : ℝ) * iteratedFDeriv ℝ k g x0 (fun _ => y) := by rw [taylor_within_apply] apply Finset.sum_congr rfl intro k hk simp only [Finset.mem_range] at hk rw [hcoef k (by rw [hn]; omega)] simp only [sub_zero, one_pow, mul_one, smul_eq_mul, one_div] have hR : iteratedDerivWithin (n + 1) φ (Icc (0 : ℝ) 1) ξ = iteratedFDeriv ℝ (n + 1) g (x0 + ξ • y) (fun _ => y) := by have hCDξ : ContDiffAt ℝ ((n + 1 : ℕ) : WithTop ℕ∞) φ ξ := (hn ▸ hφCD).contDiffAt rw [iteratedDerivWithin_eq_iteratedDeriv uniqueDiffOn_Icc_zero_one hCDξ (Set.Ioo_subset_Icc_self hξ), hφdef, line_iteratedDeriv gt (n + 1) hCDgt x0 y ξ, htrans (n + 1) (x0 + ξ • y) (hxξK ξ hξ)] have eq1 : g (x0 + y) - ∑ k ∈ range (n + 1), 1 / (Nat.factorial k : ℝ) * iteratedFDeriv ℝ k g x0 (fun _ => y) = iteratedFDeriv ℝ (n + 1) g (x0 + ξ • y) (fun _ => y) / (Nat.factorial (n + 1) : ℝ) := by rw [hφ1, hsum, hR] at htay; simpa using htay have hxξS : x0 + ξ • y ∈ S := hUS (hKU (hxξK ξ hξ)) have hbound := holder_diag_diff_le hg (x0 + ξ • y) x0 hxξS hx0S y rw [hn] at hbound rw [add_sub_cancel_left, norm_smul, Real.norm_eq_abs, abs_of_pos hξ.1] at hbound have hlt : ((n + 1 : ℕ) : ℝ) < γ := by have := Nat.lt_ceil.mp (show ⌈γ⌉₊ - 1 < ⌈γ⌉₊ by omega); rw [hn] at this; exact this have he_nonneg : 0 ≤ γ - ((n + 1 : ℕ) : ℝ) := by linarith have hem : (γ - ((n + 1 : ℕ) : ℝ)) + ((n + 1 : ℕ) : ℝ) = γ := by ring have hcombine : ‖y‖ ^ (γ - ((n + 1 : ℕ) : ℝ)) * ‖y‖ ^ (n + 1) = ‖y‖ ^ γ := by rw [← Real.rpow_natCast (‖y‖) (n + 1), ← Real.rpow_add' (norm_nonneg y) (by rw [hem]; exact ne_of_gt hγ), hem] have key : (ξ * ‖y‖) ^ (γ - ((n + 1 : ℕ) : ℝ)) * ‖y‖ ^ (n + 1) ≤ ‖y‖ ^ γ := by rw [Real.mul_rpow hξ.1.le (norm_nonneg y), mul_assoc, hcombine] calc ξ ^ (γ - ((n + 1 : ℕ) : ℝ)) * ‖y‖ ^ γ ≤ 1 * ‖y‖ ^ γ := mul_le_mul_of_nonneg_right (Real.rpow_le_one hξ.1.le hξ.2.le he_nonneg) (Real.rpow_nonneg (norm_nonneg y) γ) _ = ‖y‖ ^ γ := one_mul _ have hmid : M * (ξ * ‖y‖) ^ (γ - ((n + 1 : ℕ) : ℝ)) * ‖y‖ ^ (n + 1) ≤ M * ‖y‖ ^ γ := by rw [mul_assoc]; exact mul_le_mul_of_nonneg_left key hM have hgoal_eq : g (x0 + y) - ∑ j ∈ range (n + 1 + 1), 1 / (Nat.factorial j : ℝ) * iteratedFDeriv ℝ j g x0 (fun _ => y) = 1 / (Nat.factorial (n + 1) : ℝ) * (iteratedFDeriv ℝ (n + 1) g (x0 + ξ • y) (fun _ => y) - iteratedFDeriv ℝ (n + 1) g x0 (fun _ => y)) := by rw [Finset.sum_range_succ]; linear_combination eq1 rw [hn, hgoal_eq, abs_mul, abs_of_pos (div_pos one_pos hfac)] calc 1 / (Nat.factorial (n + 1) : ℝ) * |iteratedFDeriv ℝ (n + 1) g (x0 + ξ • y) (fun _ => y) - iteratedFDeriv ℝ (n + 1) g x0 (fun _ => y)| ≤ 1 / (Nat.factorial (n + 1) : ℝ) * (M * (ξ * ‖y‖) ^ (γ - ((n + 1 : ℕ) : ℝ)) * ‖y‖ ^ (n + 1)) := mul_le_mul_of_nonneg_left hbound (div_pos one_pos hfac).le _ ≤ 1 / (Nat.factorial (n + 1) : ℝ) * (M * ‖y‖ ^ γ) := mul_le_mul_of_nonneg_left hmid (div_pos one_pos hfac).le _ = M / (Nat.factorial (n + 1) : ℝ) * ‖y‖ ^ γ := by ring

theorem holder_point_l1_interpolation {d : ℕ} {γ M r : ℝ} {x0 : Fin d → ℝ} {S : Set (Fin d → ℝ)} (hγ : 0 < γ) (hM : 0 < M) (hr : 0 < r) (hS : supBall x0 r ⊆ S) : ∃ cH : ℝ, 0 < cH ∧ ∀ g : (Fin d → ℝ) → ℝ, HolderBallStd g γ M S → cH * |g x0| ^ (1 + (d : ℝ) / γ) ≤ ∫ x in supBall x0 r, |g x| := by classical -- Construct the moment-cancelling 1-D kernel and tensorize it as `K = prodKernel k d`. obtain ⟨k, hk_cont, hk_supp, hk_mass, hk_mom⟩ := exists_moment_cancelling_kernel_1d (⌈γ⌉₊ - 1) -- `k` is bounded (continuous with support in `[-1,1]`). have hcs : HasCompactSupport k := by apply HasCompactSupport.intro (isCompact_Icc (a := (-1 : ℝ)) (b := 1)) intro x hx apply hk_supp rw [Set.mem_Icc, not_and_or] at hx rcases hx with hx | hx · rw [not_le] at hx; rw [lt_abs]; right; linarith · rw [not_le] at hx; rw [lt_abs]; left; linarith obtain ⟨C0, hC0⟩ := hk_cont.bounded_above_of_compact_support hcs set B := max C0 0 with hBdef have hB : ∀ u, |k u| ≤ B := fun u => le_trans (by simpa [Real.norm_eq_abs] using hC0 u) (le_max_left _ _) have hB0 : 0 ≤ B := le_max_right _ _ -- `B > 0`: else `k ≡ 0`, contradicting unit mass. have hBpos : 0 < B := by rcases hB0.lt_or_eq with h | h · exact h · exfalso have hk0 : ∀ u, k u = 0 := by intro u have hle : |k u| ≤ 0 := by rw [h]; exact hB u exact abs_eq_zero.mp (le_antisymm hle (abs_nonneg _)) rw [MeasureTheory.setIntegral_congr_fun measurableSet_Icc (fun u _ => hk0 u)] at hk_mass simp at hk_mass have hBd : 0 < B ^ d := pow_pos hBpos d -- Obtain the uniform bias constant `C`. obtain ⟨C, hC0nn, hCbias⟩ := holder_taylor_bias hγ hM hS hk_cont hk_supp hk_mass hk_mom hB hB0 -- Choose the bandwidth constant `cstar`. have hMrpow_pos : 0 < M ^ ((1 : ℝ) / γ) := Real.rpow_pos_of_pos hM _ have hC1 : (0 : ℝ) < C + 1 := by positivity have hden_pos : (0 : ℝ) < 4 * (C + 1) * M := by positivity have hb_pos : 0 < (1 / (4 * (C + 1) * M)) ^ ((1 : ℝ) / γ) := Real.rpow_pos_of_pos (by positivity) _ set cstar := min (r / M ^ ((1 : ℝ) / γ)) ((1 / (4 * (C + 1) * M)) ^ ((1 : ℝ) / γ)) with hcstar_def have hcstar_pos : 0 < cstar := lt_min (div_pos hr hMrpow_pos) hb_pos refine ⟨(3 / (4 * B ^ d)) * cstar ^ d, ?_, ?_⟩ · exact mul_pos (div_pos (by norm_num) (mul_pos (by norm_num) hBd)) (pow_pos hcstar_pos d) · intro g hg set Δ := |g x0| with hΔdef have hΔnn : 0 ≤ Δ := by rw [hΔdef]; exact abs_nonneg _ rcases hΔnn.lt_or_eq with hΔpos | hΔ0 swap · -- `Δ = 0`: RHS ≥ 0. rw [← hΔ0, Real.zero_rpow (by positivity : (1 : ℝ) + (d : ℝ) / γ ≠ 0), mul_zero] exact MeasureTheory.setIntegral_nonneg (measurableSet_supBall x0 r) (fun x _ => abs_nonneg _) · -- `Δ > 0`. have hx0S : x0 ∈ S := hS (mem_supBall_self x0 hr.le) have hΔM : Δ ≤ M := by have h0 := hg.2.1 0 (zero_le _) x0 hx0S rw [norm_iteratedFDeriv_zero, Real.norm_eq_abs] at h0 rw [hΔdef]; exact h0 set h := cstar * Δ ^ ((1 : ℝ) / γ) with hh_def have hh_pos : 0 < h := mul_pos hcstar_pos (Real.rpow_pos_of_pos hΔpos _) -- `h ≤ r`. have hh_le_r : h ≤ r := by rw [hh_def] have hΔle : Δ ^ ((1 : ℝ) / γ) ≤ M ^ ((1 : ℝ) / γ) := Real.rpow_le_rpow hΔnn hΔM (one_div_nonneg.mpr hγ.le) have hne := hMrpow_pos.ne' calc cstar * Δ ^ ((1 : ℝ) / γ) ≤ cstar * M ^ ((1 : ℝ) / γ) := mul_le_mul_of_nonneg_left hΔle hcstar_pos.le _ ≤ (r / M ^ ((1 : ℝ) / γ)) * M ^ ((1 : ℝ) / γ) := mul_le_mul_of_nonneg_right (min_le_left _ _) hMrpow_pos.le _ = r := by field_simp -- Remainder `C·M·hᵞ ≤ Δ/4`. have hpow : (Δ ^ ((1 : ℝ) / γ)) ^ γ = Δ := by rw [← Real.rpow_mul hΔnn, one_div_mul_cancel hγ.ne', Real.rpow_one] have hhg : h ^ γ = cstar ^ γ * Δ := by rw [hh_def, Real.mul_rpow hcstar_pos.le (Real.rpow_nonneg hΔnn _), hpow] have hcstar_g : cstar ^ γ ≤ 1 / (4 * (C + 1) * M) := by have h2 : cstar ^ γ ≤ ((1 / (4 * (C + 1) * M)) ^ ((1 : ℝ) / γ)) ^ γ := Real.rpow_le_rpow hcstar_pos.le (min_le_right _ _) hγ.le rwa [← Real.rpow_mul (by positivity), one_div_mul_cancel hγ.ne', Real.rpow_one] at h2 have hrem : C * M * h ^ γ ≤ Δ / 4 := by have hge : C * M * cstar ^ γ ≤ C * M * (1 / (4 * (C + 1) * M)) := mul_le_mul_of_nonneg_left hcstar_g (by positivity) have heq : C * M * (1 / (4 * (C + 1) * M)) = C / (4 * (C + 1)) := by field_simp rw [heq] at hge have hle14 : C / (4 * (C + 1)) ≤ 1 / 4 := by rw [div_le_iff₀ (by positivity : (0:ℝ) < 4 * (C + 1))]; nlinarith [hC0nn] have hCMc : C * M * cstar ^ γ ≤ 1 / 4 := le_trans hge hle14 rw [hhg] calc C * M * (cstar ^ γ * Δ) = (C * M * cstar ^ γ) * Δ := by ring _ ≤ (1 / 4) * Δ := mul_le_mul_of_nonneg_right hCMc hΔnn _ = Δ / 4 := by ring -- Bias and change-of-variables combine into the `l1` hypothesis. have hbias := hCbias g hg h hh_pos hh_le_r have hbias' : |g x0 - ∫ u in supBall (0 : Fin d → ℝ) 1, prodKernel k d u * g (x0 + h • u)| ≤ Δ / 4 := le_trans hbias hrem have hVlow : 3 * Δ / 4 ≤ |∫ u in supBall (0 : Fin d → ℝ) 1, prodKernel k d u * g (x0 + h • u)| := by have h1 := abs_sub_abs_le_abs_sub (g x0) (∫ u in supBall (0 : Fin d → ℝ) 1, prodKernel k d u * g (x0 + h • u)) rw [← hΔdef] at h1 linarith [le_trans h1 hbias'] have hsm := smoothed_abs_le hS (prodKernel_abs_le hB) g hg h hh_pos hh_le_r have hbound : 3 * Δ / 4 ≤ B ^ d * h⁻¹ ^ d * ∫ x in supBall x0 r, |g x| := le_trans hVlow hsm have hfin := l1_lower_of_bias_bound hBd hΔpos hcstar_pos hh_def hbound rw [hΔdef] exact hfin

theorem exists_moment_cancelling_kernel_1d (m : ℕ) : ∃ k : ℝ → ℝ, Continuous k ∧ (∀ u : ℝ, 1 < |u| → k u = 0) ∧ (∫ u in Icc (-1 : ℝ) 1, k u) = 1 ∧ (∀ j : ℕ, 1 ≤ j → j ≤ m → (∫ u in Icc (-1 : ℝ) 1, u ^ j * k u) = 0) := by -- Solve the Gram system `G c = e₀` by injectivity ⟹ surjectivity of a -- finite-dimensional endomorphism. have hsurj : Surjective ((hpkGram m).mulVecLin) := by rw [← LinearMap.injective_iff_surjective, ← LinearMap.ker_eq_bot, Matrix.ker_mulVecLin_eq_bot_iff] exact fun v hv => hpkInjective m v hv obtain ⟨c, hc⟩ := hsurj (single 0 1) rw [Matrix.mulVecLin_apply] at hc -- The moment integrals of `k = max(1-u²,0) · p(u)` over `[-1,1]` equal the Gram rows. have hmom : ∀ J : Fin (m + 1), (∫ u in Icc (-1 : ℝ) 1, u ^ (J : ℕ) * (max (1 - u ^ 2) 0 * hpkPoly m c u)) = (hpkGram m).mulVec c J := by intro J rw [MeasureTheory.setIntegral_congr_fun measurableSet_Icc (f := fun u => u ^ (J : ℕ) * (max (1 - u ^ 2) 0 * hpkPoly m c u)) (g := fun u => u ^ (J : ℕ) * ((1 - u ^ 2) * hpkPoly m c u)) (fun u hu => by dsimp only rw [max_eq_left (by nlinarith [hu.1, hu.2] : (0 : ℝ) ≤ 1 - u ^ 2)])] exact hpkExpand m c J refine ⟨fun u => max (1 - u ^ 2) 0 * hpkPoly m c u, ?_, ?_, ?_, ?_⟩ · exact ((continuous_const.sub (continuous_pow 2)).max continuous_const).mul (hpkPoly_continuous m c) · intro u hu have h1 : (1 : ℝ) < u ^ 2 := by nlinarith [hu, sq_abs u, abs_nonneg u] dsimp only rw [max_eq_right (by linarith : (1 : ℝ) - u ^ 2 ≤ 0), zero_mul] · have h0 := hmom 0 rw [hc, Pi.single_eq_same] at h0 simp only [Fin.val_zero, pow_zero, one_mul] at h0 simpa using h0 · intro j hj1 hjm have hJ : j < m + 1 := by omega have h0 := hmom ⟨j, hJ⟩ rw [hc, Pi.single_apply, if_neg (by intro h; rw [Fin.ext_iff] at h; simp at h; omega)] at h0 simpa using h0